Library Sec4_Groundterms
Contents :
0: General House Keeping
1: Syntax definitions
2: Equality, membership and extraction functions for the syntax
2A: Equality functions
2B: Membership functions
2C: Extraction of submembers functions
3: Substitution
4: Ground terms and rules instances
5: Tamarin Reduction
6: Example
7: Definitions from Chapter 5 of the thesis
8: Tests and Definitions for Well formedness
8A: Functions to test no or One Input / Output in facts
8B: Definitions on Variables and Terms for Equivalence proof
8C: Well formedness definitions
9: Some useful lemmas on well formedness
10: Definitions from Chapter 6 of the thesis
10A: Types of Facts allowed in the system
11: Props and Theorems from Chapter 6
Load Sec3_SubstitutionDefs.
===================================
4: Ground terms and rule instances
===================================
Ground Defs, these might be better as Props, rather than bools
I'm not sure at this point, we can always change these to Props later
Fixpoint groundBaseTerm (ts:baseTerm) : Prop :=
match ts with
| Var v => False
| _ => True
end.
Definition groundBaseTerms : baseTerms -> Prop := trueForAll groundBaseTerm.
Fixpoint groundTerm (t:term) : Prop :=
match t with
| Func f ts => groundBaseTerms ts
| Bterm (Name (Pub n)) => True
| Bterm (Name (Fresh_S n)) => True
| Bterm (Name (Fresh_P n)) => True
| _ => False
end.
Fixpoint groundTerms (ts:terms) : Prop :=
match ts with
| t::ts => groundTerm t /\ groundTerms ts
| [] => True
end.
Fixpoint groundFact (f:fact) : Prop :=
match f with
| IN ts => groundTerms ts
| OUT ts => groundTerms ts
| K ts => groundTerms ts
| STATE n ts => groundTerms ts
| FR_P fn => True
end.
Fixpoint groundFacts (fs:facts) : Prop :=
match fs with
| f::fs => groundFact f /\ groundFacts fs
| [] => True
end.
Definition groundActionLabel (al:actionLabel) : Prop :=
match al with
| ActLabel n ts => groundTerms ts
end.
Fixpoint groundBasicLabel (lb:list actionLabel) : Prop :=
match lb with
| al::als => groundActionLabel al /\ groundBasicLabel als
| [] => True
end.
Definition groundLoggedLabel (lg:actionLabel) (lb:list actionLabel) : Prop :=
groundActionLabel lg /\ groundBasicLabel lb.
Definition groundLoggedSIDLabel (t:baseTerm) (lg:actionLabel) (lb:list actionLabel) : Prop :=
groundBaseTerm t /\ groundActionLabel lg /\ groundBasicLabel lb.
Definition groundLabel (lb:label) : Prop :=
match lb with
| BasicLabel ls => groundBasicLabel ls
| LoggedLabel lg ls => groundLoggedLabel lg ls
| LoggedSIDLabel t lg ls => groundLoggedSIDLabel t lg ls
end.
Definition groundRule (r:rule) : Prop :=
match r with
| RuleProto f1 l f2 => groundFacts f1 /\ groundFacts f2 /\ groundLabel l
| RuleSetup f1 l f2 => groundFacts f1 /\ groundFacts f2 /\ groundLabel l
end.
Inductive ginst : rule -> rule -> Prop :=
| Ginst : forall r1 r2, (exists sigma, (applySubRule sigma r2) = r1) /\ (groundRule r1) -> ginst r1 r2.
Inductive ginsts : rule -> ruleList -> Prop :=
| GinstHead : forall r1 r2 rs, (ginst r1 r2) -> ginsts r1 (r2::rs)
| GinstTail : forall r1 r2 rs, (ginsts r1 rs) -> ginsts r1 (r2::rs).
Inductive ginstWithSigma : rule -> substitution -> rule -> Prop :=
| GinstSigma : forall r1 r2 sigma, (applySubRule sigma r2) = r1 /\ groundRule r1 -> ginstWithSigma r1 sigma r2.
Inductive ginstsWithSigma : rule -> substitution -> ruleList -> Prop :=
| GinstHeadSigma : forall r1 r2 rs sigma,
(ginstWithSigma r1 sigma r2) -> ginstsWithSigma r1 sigma (r2::rs)
| GinstTailSigma : forall r1 r2 rs sigma,
(ginstsWithSigma r1 sigma rs) -> ginstsWithSigma r1 sigma (r2::rs).
Lemma composeSubstBaseTerm : forall bt (sigma1:substitution) (sigma2:substitution),
groundBaseTerm (applySubBaseTerm sigma1 bt)
-> groundBaseTerm (applySubBaseTerm (compose sigma1 sigma2) bt).
Lemma composeSubstBaseTerms : forall bt (sigma1:substitution) (sigma2:substitution),
groundBaseTerms (applySubBaseTerms sigma1 bt)
-> groundBaseTerms (applySubBaseTerms (compose sigma1 sigma2) bt).
Lemma composeSubstGroundTerm : forall tm (sigma1:substitution) (sigma2:substitution),
groundTerm (applySubTerm sigma1 tm)
-> groundTerm (applySubTerm (compose sigma1 sigma2) tm).
Lemma composeSubstGroundTerms : forall tms (sigma1:substitution) (sigma2:substitution),
groundTerms (applySubTerms sigma1 tms)
-> groundTerms (applySubTerms (compose sigma1 sigma2) tms).
Lemma composeSubstGroundAL : forall al (sigma1:substitution) (sigma2:substitution),
groundActionLabel (applySubActionLabel sigma1 al)
-> groundActionLabel (applySubActionLabel (compose sigma1 sigma2) al).
Lemma composeSubstGroundBasicLabel : forall l (sigma1:substitution) (sigma2:substitution),
groundBasicLabel (map ( applySubActionLabel sigma1) l)
-> groundBasicLabel (map (applySubActionLabel (compose sigma1 sigma2)) l).
Lemma composeSubstGroundLoggedLabel : forall al ls (sigma1:substitution) (sigma2:substitution),
groundLoggedLabel
(applySubActionLabel sigma1 al)
(map (applySubActionLabel sigma1) ls)
-> groundLoggedLabel
(applySubActionLabel (compose sigma1 sigma2) al)
(map (applySubActionLabel (compose sigma1 sigma2)) ls).
Lemma composeSubstGroundLoggedSIDLabel : forall al ls t (sigma1:substitution) (sigma2:substitution),
groundLoggedSIDLabel
(applySubBaseTerm sigma1 t)
(applySubActionLabel sigma1 al)
(map (applySubActionLabel sigma1) ls)
-> groundLoggedSIDLabel
(applySubBaseTerm (compose sigma1 sigma2) t)
(applySubActionLabel (compose sigma1 sigma2) al)
(map (applySubActionLabel (compose sigma1 sigma2)) ls).
Lemma composeSubstGroundLabel : forall l (sigma1:substitution) (sigma2:substitution),
groundLabel (applySubLabel sigma1 l)
-> groundLabel (applySubLabel (compose sigma1 sigma2) l).
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
S
Sec4_Groundterms [library]Library Index
S
Sec4_Groundterms| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
This page has been generated by coqdoc