Library Sec5_TamarinReduction
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
3B: 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 Sec4_Groundterms.
"reduceWithRule r f1 l f2" means that the rule "r" can match the
facts "f1" and produce the facts "f2" with the label "label"
Inductive reduceWithGroundRule : rule -> facts -> label -> facts -> Prop :=
| R_match : forall r s1, (subList (premiseFacts r) s1) ->
reduceWithGroundRule r s1 (labelR r)
(appendAny (conclFacts r) (removeFacts (premiseFacts r) s1)).
Definition reduceWithRule (r1:rule) (f:facts) (l:label) (f2:facts) : Prop :=
exists r2, (ginst r2 r1) /\ reduceWithGroundRule r2 f l f2.
Definition reduceWithRules (rs:ruleList) (f:facts) (l:label) (f2:facts) : Prop :=
exists r2, (ginsts r2 rs) /\ reduceWithGroundRule r2 f l f2.
"reduceWithRuleSigma r f1 l f2" means that the rule "r" can match the
facts "f1" and produce the facts "f2" with the label "label"
Definition reduceWithRuleSigma (r1:rule) (sigma:substitution) (f:facts) (l:label) (f2:facts) : Prop :=
exists r2, (ginstWithSigma r2 sigma r1) /\ reduceWithGroundRule r2 f l f2.
Definition reduceWithRulesSigma (rs:ruleList) (sigma:substitution) (f:facts) (l:label) (f2:facts) : Prop :=
exists r2, (ginstsWithSigma r2 sigma rs) /\ reduceWithGroundRule r2 f l f2.
Definition freshRuleS (n:freshNameSetup) : rule := (RuleSetup [] emptyLabel [FR_P (Name (Fresh_S n))]).
Definition freshRuleP (n:freshNameProto) : rule := (RuleProto [] emptyLabel [FR_P (Name (Fresh_P n))]).
Inductive run : ruleList -> facts -> trace -> facts -> Prop :=
| Run_Stop : forall rl f1, run rl f1 [] f1
| Run_Step : forall rl f1 t f2 f3 l, (reduceWithRules rl f1 l f2)
-> (run rl f2 t f3) -> run rl f1 (l::t) f3
| Run_Step_Silent : forall rl f1 t f2 f3, (reduceWithRules rl f1 emptyLabel f2)
-> (run rl f2 t f3) -> run rl f1 t f3
| Run_FreshStepP : forall rl f1 t f2 f3 fn, (reduceWithRule (freshRuleP fn) f1 emptyLabel f2)
-> (run rl f2 t f3) -> run rl f1 t f3.
Inductive runSigma : ruleList -> substitutions -> facts -> trace -> facts -> Prop :=
| SigmaRun_Stop : forall rl f1, runSigma rl [] f1 [] f1
| SigmaRun_Step : forall rl sigmaPrev f1 t f2 f3 l sigmaNow, (reduceWithRulesSigma rl sigmaNow f1 l f2)
-> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 (l::t) f3
| SigmaRun_Step_Silent : forall rl sigmaPrev f1 t f2 f3 sigmaNow, (reduceWithRulesSigma rl sigmaNow f1 emptyLabel f2)
-> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 t f3
| SigmaRun_FreshStepP : forall rl f1 t f2 f3 fn sigmaPrev sigmaNow, (reduceWithRuleSigma (freshRuleP fn) sigmaNow f1 emptyLabel f2)
-> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 t f3.
Some useful Lemmas about traces
Lemma reduceWithFirstRule : forall r rl f1 f2 l, reduceWithRule r f1 l f2 -> reduceWithRules (r::rl) f1 l f2.
Lemma reduceWithSecondRule : forall r1 r2 rl f1 f2 l, reduceWithRule r2 f1 l f2 -> reduceWithRules (r1::r2::rl) f1 l f2.
Lemma FreshRulePIsAGroundRule : forall fn, groundRule (freshRuleP fn).
Lemma ProtoFreshNameStep (fn:freshNameProto) :
forall fs, reduceWithRule (freshRuleP fn) fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Lemma FreshRuleSIsAGroundRule : forall fn, groundRule (freshRuleS fn).
Lemma SetupFreshNameStep (fn:freshNameSetup) :
forall fs, reduceWithRule (freshRuleP fn) fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Lemma ProtoFreshNameStepEmpty (fn:freshNameProto) :
reduceWithRule (freshRuleP fn) [] emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Lemma SetupFreshNameStepEmpty (fn:freshNameSetup) :
reduceWithRule (freshRuleP fn) [] emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Lemma reduceRulesLessImpliesMore : forall r rl f1 l f2, reduceWithRules rl f1 l f2 -> reduceWithRules (r::rl) f1 l f2.
Lemma runRulesLessImpliesMore : forall r rl f1 t f2, run rl f1 t f2 -> run (r::rl) f1 t f2.
Lemma runTransitive : forall rl s1 s2 s3 l1 l2,
run rl s1 l1 s2 /\ run rl s2 l2 s3 -> run rl s1 (appendAny l1 l2) s3.
The same Lemmas with substitution
Lemma reduceWithFirstRuleSigma : forall r rl f1 f2 l sigma, reduceWithRuleSigma r sigma f1 l f2
-> reduceWithRulesSigma (r::rl) sigma f1 l f2.
Lemma reduceWithSecondRuleSigma : forall r1 r2 rl f1 f2 l sigma, reduceWithRuleSigma r2 sigma f1 l f2
-> reduceWithRulesSigma (r1::r2::rl) sigma f1 l f2.
Lemma ProtoFreshNameStepSigma (fn:freshNameProto) :
forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Lemma SetupFreshNameStepSigma (fn:freshNameSetup) :
forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Lemma ProtoFreshNameStepEmptySigma (fn:freshNameProto) :
reduceWithRuleSigma (freshRuleP fn) subs_empty [] emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Lemma SetupFreshNameStepEmptySigma (fn:freshNameSetup) :
reduceWithRuleSigma (freshRuleP fn) subs_empty [] emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Lemma reduceRulesLessImpliesMoreSigma : forall r rl f1 l f2 sigma, reduceWithRulesSigma rl sigma f1 l f2
-> reduceWithRulesSigma (r::rl) sigma f1 l f2.
Lemma runRulesLessImpliesMoreSigma : forall r rl f1 t f2 sigmas, runSigma rl sigmas f1 t f2
-> runSigma (r::rl) sigmas f1 t f2.
Lemma runTransitiveSigma : forall rl f1 f2 f3 l1 l2 sigmas1 sigmas2,
runSigma rl sigmas1 f1 l1 f2 /\ runSigma rl sigmas2 f2 l2 f3 -> runSigma rl (appendAny sigmas1 sigmas2) f1 (appendAny l1 l2) f3.
-> reduceWithRulesSigma (r::rl) sigma f1 l f2.
Lemma reduceWithSecondRuleSigma : forall r1 r2 rl f1 f2 l sigma, reduceWithRuleSigma r2 sigma f1 l f2
-> reduceWithRulesSigma (r1::r2::rl) sigma f1 l f2.
Lemma ProtoFreshNameStepSigma (fn:freshNameProto) :
forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Lemma SetupFreshNameStepSigma (fn:freshNameSetup) :
forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Lemma ProtoFreshNameStepEmptySigma (fn:freshNameProto) :
reduceWithRuleSigma (freshRuleP fn) subs_empty [] emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Lemma SetupFreshNameStepEmptySigma (fn:freshNameSetup) :
reduceWithRuleSigma (freshRuleP fn) subs_empty [] emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Lemma reduceRulesLessImpliesMoreSigma : forall r rl f1 l f2 sigma, reduceWithRulesSigma rl sigma f1 l f2
-> reduceWithRulesSigma (r::rl) sigma f1 l f2.
Lemma runRulesLessImpliesMoreSigma : forall r rl f1 t f2 sigmas, runSigma rl sigmas f1 t f2
-> runSigma (r::rl) sigmas f1 t f2.
Lemma runTransitiveSigma : forall rl f1 f2 f3 l1 l2 sigmas1 sigmas2,
runSigma rl sigmas1 f1 l1 f2 /\ runSigma rl sigmas2 f2 l2 f3 -> runSigma rl (appendAny sigmas1 sigmas2) f1 (appendAny l1 l2) f3.
| 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
Sec5_TamarinReduction [library]Library Index
S
Sec5_TamarinReduction| 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