(** 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 Sec1_SyntaxDefs. (** =================================== *** 2: Equality, membership and extraction functions for the syntax =================================== **) (** =================================== 2A: Equality functions =================================== **) (** We have defined two versions for the same definitions anything starting with "b" returns a bool otherwise Prop *) Inductive b2p : bool -> Prop := | b2pt : True -> b2p true. (** "beq_string s1 s2 "checks whether two strings are equal *) Definition beq_string (s1:string) (s2:string) : bool := if (string_dec s1 s2) then true else false. Lemma beq_string_EQ : forall s1 s2, beq_string s1 s2 = true -> s1 = s2. Proof. intros. unfold beq_string in H. destruct (string_dec s1 s2) eqn:D. assumption. inversion H. Qed. (* This is probably defined in one of the standard libs *) Fixpoint beq_A_list (A:Type) (beq_A: A->A->bool) (s1:list A) (s2:list A) : bool := match s1,s2 with | [],[] => true | h1::ts1, h2::ts2 => andb (beq_A h1 h2) (beq_A_list beq_A ts1 ts2) | _, _ => false end. (* This is probably defined in one of the standard libs *) Fixpoint eq_A_list (A:Type) (eq_A: A->A->Prop) (s1:list A) (s2:list A) : Prop := match s1,s2 with | [],[] => True | h1::ts1, h2::ts2 => (eq_A h1 h2) /\ (eq_A_list eq_A ts1 ts2) | _, _ => False end. (** "beq_string_list s1 s2 "checks whether two lists of strings are equal *) Definition beq_string_list : (list string) -> (list string) -> bool := beq_A_list beq_string. Definition eq_string (s1:string) (s2:string) : Prop := b2p (beq_string s1 s2). Definition eq_string_list (s1: list string) (s2:list string) : Prop := b2p (beq_string_list s1 s2). (** "eq_base_term t1 t2 "checks whether two baseterms are equal *) Fixpoint beq_name (n1:name) (n2:name) : bool := match n1,n2 with | Fresh_P s1 , Fresh_P s2 => beq_string s1 s2 | Fresh_S s1 , Fresh_S s2 => beq_string s1 s2 | Pub s1, Pub s2 => beq_string s1 s2 | _, _ => false end. Definition eq_name (n1:name) (n2:name) : Prop := b2p (beq_name n1 n2). Definition beq_names : (list name) -> (list name) -> bool := beq_A_list beq_name. Lemma beq_name_EQ : forall n1 n2, beq_name n1 n2 = true -> n1 = n2. Proof. intros. destruct n1; destruct n2; inversion H; apply beq_string_EQ in H1; subst; reflexivity. Qed. Definition name_dec : forall b1 b2 : name, {b1 = b2} + {b1 <> b2}. decide equality;apply string_dec. Defined. Fixpoint beq_baseTerm (t1:baseTerm) (t2:baseTerm) : bool := match t1,t2 with | Var x,Var y => beq_string x y | Name n1, Name n2 => beq_name n1 n2 | _, _ => false end. Fixpoint eq_baseTerm (t1:baseTerm) (t2:baseTerm) : Prop := match t1,t2 with | Var x,Var y => eq_string x y | Name n1, Name n2 => eq_name n1 n2 | _, _ => False end. Definition baseTerm_dec : forall b1 b2 : baseTerm, {b1 = b2} + {b1 <> b2}. decide equality. + apply string_dec. + destruct n0; destruct n1. - decide equality; apply string_dec. - decide equality; apply string_dec. - right. unfold not. intro. inversion H. - right. unfold not. intro. inversion H. - decide equality; apply string_dec. - right. unfold not. intro. inversion H. - right. unfold not. intro. inversion H. - right. unfold not. intro. inversion H. - decide equality; apply string_dec. Defined. Definition beq_baseTerms : (list baseTerm) -> (list baseTerm) -> bool := beq_A_list beq_baseTerm. Definition eq_baseTerms : (list baseTerm) -> (list baseTerm) -> Prop := eq_A_list eq_baseTerm. Definition baseTerms_dec : forall bl1 bl2 : (list baseTerm), {bl1 = bl2} + {bl1 <> bl2}. decide equality. apply baseTerm_dec. Defined. Definition beq_term (t1:term) (t2:term) : bool := match t1,t2 with | (Bterm b1), (Bterm b2) => beq_baseTerm b1 b2 | (Func f1 l1), (Func f2 l2) => andb (beq_string f1 f2) (beq_baseTerms l1 l2) | _, _ => false end. Definition beq_terms : (list term) -> (list term) -> bool := beq_A_list beq_term. Definition eq_term (t1:term) (t2:term) : Prop := match t1,t2 with | (Bterm b1), (Bterm b2) => eq_baseTerm b1 b2 | (Func f1 l1), (Func f2 l2) => (eq_string f1 f2) /\ (eq_baseTerms l1 l2) | _, _ => False end. Definition eq_termFuncName (t1:term) (t2:term) : Prop := match t1,t2 with | (Func f1 l1), (Func f2 l2) => (eq_string f1 f2) | _, _ => False end. Definition eq_terms : (list term) -> (list term) -> Prop := eq_A_list eq_term. Definition term_dec : forall t1 t2 : term, {t1 = t2} + {t1 <> t2}. decide equality. + apply baseTerms_dec. + apply string_dec. + apply baseTerm_dec. Defined. Definition terms_dec : forall ts1 ts2 : terms, {ts1 = ts2} + {ts1 <> ts2}. decide equality. apply term_dec. Defined. Fixpoint beq_fact (f1:fact) (f2:fact) : bool := match f1,f2 with | IN ts1, IN ts2 => beq_terms ts1 ts2 | OUT ts1, OUT ts2 => beq_terms ts1 ts2 | K ts1, K ts2 => beq_terms ts1 ts2 | STATE n1 ts1, STATE n2 ts2 => andb (beq_name n1 n2) (beq_terms ts1 ts2) | FR_P bt1, FR_P bt2 => beq_baseTerm bt1 bt2 | _, _ => false end. Fixpoint eq_fact (f1:fact) (f2:fact) : Prop := match f1,f2 with | IN ts1, IN ts2 => eq_terms ts1 ts2 | OUT ts1, OUT ts2 => eq_terms ts1 ts2 | K ts1, K ts2 => eq_terms ts1 ts2 | STATE n1 ts1, STATE n2 ts2 => eq_name n1 n2 /\ eq_terms ts1 ts2 | FR_P bt1, FR_P bt2 => eq_baseTerm bt1 bt2 | _, _ => False end. Definition eq_facts : (list fact) -> (list fact) -> Prop := eq_A_list eq_fact. Definition beq_facts : (list fact) -> (list fact) -> bool := beq_A_list beq_fact. Definition fact_dec : forall f1 f2 : fact, {f1 = f2} + {f1 <> f2}. decide equality; try apply terms_dec. + apply name_dec. + apply baseTerm_dec. Defined. Definition facts_dec : forall fs1 fs2 : facts, {fs1 = fs2} + {fs1 <> fs2}. decide equality. apply fact_dec. Defined. Definition tpair_dec : forall tp1 tp2 : tpair, {tp1 = tp2} + {tp1 <> tp2}. decide equality; try apply terms_dec. + apply term_dec. + apply term_dec. Defined. Definition tpairs_dec : forall ts1 ts2 : tpairs, {ts1 = ts2} + {ts1 <> ts2}. decide equality. apply tpair_dec. Defined. Definition beq_var (v1:variable) (v2:variable) : bool := beq_string v1 v2. Definition beq_vars_list : (list variable) -> (list variable) -> bool := beq_A_list beq_var. Definition beq_actionLabel (a1:actionLabel) (a2:actionLabel) : bool := match a1, a2 with | ActLabel n1 ts1, ActLabel n2 ts2 => andb (beq_name n1 n2) (beq_terms ts1 ts2) end. Definition beq_actionLabels : (list actionLabel) -> (list actionLabel) -> bool := beq_A_list beq_actionLabel. Definition actionLabel_dec : forall t1 t2 : actionLabel, {t1 = t2} + {t1 <> t2}. decide equality. + apply terms_dec. + apply name_dec. Defined. Definition actionLabels_dec : forall t1 t2 : list actionLabel, {t1 = t2} + {t1 <> t2}. decide equality. apply actionLabel_dec. Defined. Definition eq_actionLabel (a1:actionLabel) (a2:actionLabel) : Prop := b2p (beq_actionLabel a1 a2). Definition eq_actionLabels (al1:list actionLabel) (al2:list actionLabel) : Prop := b2p (beq_actionLabels al1 al2). Definition label_dec : forall l1 l2 : label, {l1 = l2} + {l1 <> l2}. decide equality. apply actionLabels_dec. apply actionLabels_dec. apply actionLabel_dec. apply actionLabels_dec. apply actionLabel_dec. apply baseTerm_dec. Defined. Definition beq_label (l1:label) (l2:label) : bool := match l1, l2 with | BasicLabel ll1 , BasicLabel ll2 => beq_actionLabels ll1 ll2 | LoggedLabel al1 ll1 , LoggedLabel al2 ll2 => andb (beq_actionLabel al1 al2) (beq_actionLabels ll1 ll2) | _, _ => false end. Definition eq_label (l1:label) (l2:label) : Prop := match l1, l2 with | BasicLabel ll1 , BasicLabel ll2 => eq_A_list eq_actionLabel ll1 ll2 | LoggedLabel lg1 ll1 , LoggedLabel lg2 ll2 => eq_A_list eq_actionLabel ll1 ll2 /\ eq_actionLabel lg1 lg2 | _, _ => False end. Definition beq_trace : trace -> trace -> bool := beq_A_list beq_label. Definition eq_trace : trace -> trace -> Prop := eq_A_list eq_label. Definition rule_dec : forall r1 r2 : rule, {r1 = r2} + {r1 <> r2}. decide equality; try apply facts_dec; try apply label_dec. Defined. Definition rules_dec : forall r1 r2 : ruleList, {r1 = r2} + {r1 <> r2}. decide equality. apply rule_dec. Defined. (** ============================================== 2B: Membership functions : MEMBERSHIP TESTS ==================================================**) Fixpoint member {A:Type} (r:A) (rl:list A) : Prop := match rl with | [] => False | r1::rs => r=r1 \/ (member r rs) end. Fixpoint memberWith {A:Type} (x : A) (l : list A) (beq_test : A->A->bool) : bool := match l with | [] => false | h :: ts => orb (beq_test x h) (memberWith x ts beq_test) end. Fixpoint memberOnce {A:Type} (a : A) (ls : list A) : Prop := match ls with | [] => False | h::ts => a = h /\ NotIn a ts end. (* This removes the first matching fact in a list, if any *) Definition removeFact : fact -> facts -> facts := removeElement fact_dec. Fixpoint removeFacts (facts1:facts) (facts2:facts) : facts := match facts1 with | [] => facts2 | h::ts => removeFact h (removeFacts ts facts2) end. Fixpoint subList (l1:list fact) (l2:list fact) : Prop := match l1,l2 with | [],_ => True | _,[] => False | h1::t,l2 => (In h1 l2) /\ (subList t (removeFact h1 l2)) end. Definition b_inLabel (al:actionLabel) (lb:label) : bool := match lb with | BasicLabel ll1 => memberWith al ll1 beq_actionLabel | LoggedLabel lg1 ll1 => orb (beq_actionLabel al lg1) (memberWith al ll1 beq_actionLabel) | LoggedSIDLabel t lg1 ll1 => orb (beq_actionLabel al lg1) (memberWith al ll1 beq_actionLabel) end. (** "inLabel al lb" verifies whether the action label "al" is in the label "lb" or not **) Fixpoint inLabel (al:actionLabel) (lb:label) : Prop := match lb with | BasicLabel ll => member al ll | LoggedLabel lg ll => ( eq_actionLabel lg al) \/ member al ll | LoggedSIDLabel t lg ll => ( eq_actionLabel lg al) \/ member al ll end. (** "inLoggedSIDLabel al lb" verifies whether the action label "al" is in the LoggedSIDLabel "lb" or not **) Fixpoint inLoggedSIDLabel (al:actionLabel) (lb:label) : Prop := match lb with | BasicLabel ll => False | LoggedLabel lg ll => False | LoggedSIDLabel t lg ll => ( eq_actionLabel lg al) end. (** "al_in_Trace al tr" verifies whether the action label "al" is in the trace "tr" or not **) Fixpoint al_in_Trace (al:actionLabel) (tr:trace) : Prop := match tr with | [] => False | lbl1 :: lbs => inLabel al lbl1 \/ (al_in_Trace al lbs) end. (** "LoggedAL_in_Trace al tr" verifies whether the action label "al" is in the trace "tr" or not **) Fixpoint LoggedAL_in_Trace (al:actionLabel) (tr:trace) : Prop := match tr with | [] => False | lbl1 :: lbs => inLoggedSIDLabel al lbl1 \/ (LoggedAL_in_Trace al lbs) end. (** "LoggedLbl_in_Trace al tr" verifies whether the Label "lbl" is in the trace "tr" or not **) Fixpoint LoggedLbl_in_Trace (lbl:label) (tr:trace) : Prop := match tr with | [] => False | lbl1 :: lbs => (eq_label lbl lbl1) \/ (LoggedLbl_in_Trace lbl lbs) end. (** "b_lbl_inTrace lb tr" verifies whether label "lb" is in trace "tr" or not **) (** "lb" is either the first member of "tr" or somehere before the end of trace**) Definition b_label_in_Trace (lb:label) (tr:trace) : bool := memberWith lb tr beq_label. Definition b_labelS_in_Trace (lb:label) (tr:trace) : bool := memberWith lb tr beq_label. Definition beq_trace_in_Traces (tr:trace) (trlist:list trace) : bool := memberWith tr trlist beq_trace. (* MEMBERSHIP TESTS for template *) (** "beq_actionLabelName a1 a2 "checks whether two action labels in template have the same name *) Definition beq_actionLabelName (a1:actionLabel) (a2:actionLabel) : bool := match a1, a2 with | ActLabel n1 ts1, ActLabel n2 ts2 => (beq_name n1 n2) end. Definition eq_actionLabelName (a1:actionLabel) (a2:actionLabel) : Prop := b2p (beq_actionLabelName a1 a2). (** "inLabelName al lb" verifies whether the action label "al" is in the label "lb" or not **) Definition b_inLabelwithName (al:actionLabel) (lb:label) : bool := match lb with | BasicLabel ll1 => memberWith al ll1 beq_actionLabelName | LoggedLabel lg1 ll1 => orb (beq_actionLabelName al lg1) (memberWith al ll1 beq_actionLabelName) | LoggedSIDLabel t lg1 ll1 => orb (beq_actionLabelName al lg1) (memberWith al ll1 beq_actionLabelName) end. Fixpoint memberName (al:actionLabel) (lb:list actionLabel) : Prop := match lb with | [] => False | l1::ls => (eq_actionLabelName al l1) \/ (memberName al ls) end. Fixpoint inLabelwithName (al:actionLabel) (lb:label) : Prop := match lb with | BasicLabel ll => memberName al ll | LoggedLabel lg ll => ( eq_actionLabelName lg al) \/ memberName al ll | LoggedSIDLabel t lg ll => ( eq_actionLabelName lg al) \/ memberName al ll end. Fixpoint b_ALinTemplatewithName (al:actionLabel) (tm:trace) : bool := match tm with | [] => false | tm1::tms => orb (b_inLabelwithName al tm1) (b_ALinTemplatewithName al tms) end. Fixpoint b_ALinStdTemplateswithName (al:actionLabel) (StdTemps:list trace) : bool := match StdTemps with | [] => false | tm1::tms => orb (b_ALinTemplatewithName al tm1) (b_ALinStdTemplateswithName al tms) end. Definition ALinTemplatewithName (al:actionLabel) (tm:trace) : Prop := b2p (b_ALinTemplatewithName al tm). Definition ALinStdTemplateswithName (al:actionLabel) (tms:list trace) : Prop := b2p (b_ALinStdTemplateswithName al tms). Fixpoint InList (tm : term) (tmlist : terms) : bool := match tmlist with | [] => false | ml1::mls => orb (beq_term tm ml1) (InList tm mls) end. Fixpoint commonTerms (v1:terms) (v2:terms): terms := match v1 with | [] => [] | v11 :: v1s => if InList v11 v2 then (v11::(commonTerms v1s v2)) else commonTerms v1s v2 end. Fixpoint InFreshList (tm : freshNameProto) (tmlist : list freshNameProto) : bool := match tmlist with | [] => false | ml1::mls => orb (beq_term (Bterm (Name (Fresh_P tm))) (Bterm (Name (Fresh_P ml1)))) (InFreshList tm mls) end. Fixpoint commonTermsAL (alp1:actionLabel) (alp2:actionLabel): terms := match alp1, alp2 with | ActLabel nm1 vars1, ActLabel nm2 vars2 => commonTerms vars1 vars2 end. (* For Definition SelectName *) Fixpoint hasFunction (tm:terms) : Prop := match tm with | tm1::tms => match tm1 with | Func _ _ => True | _ => hasFunction tms end | [] => False end. Fixpoint hasPubNameInBaseTerms (btm:baseTerms) : Prop := match btm with | btm1::btms => match btm1 with | (Var _) => hasPubNameInBaseTerms btms | (Name nm) => match nm with | Pub _ => True | _ => hasPubNameInBaseTerms btms end end | [] => False end. Fixpoint b_hasPubNameInBaseTerms (btm:baseTerms) : bool := match btm with | btm1::btms => match btm1 with | (Var _) => b_hasPubNameInBaseTerms btms | (Name nm) => match nm with | Pub _ => true | _ => b_hasPubNameInBaseTerms btms end end | [] => false end. Fixpoint hasPubName (tm:terms) : Prop := match tm with | tm1::tms => match tm1 with | Func f bts => hasPubNameInBaseTerms bts | Bterm bt => match bt with | (Var _) => hasPubName tms | (Name nm) => match nm with | Pub _ => True | _ => hasPubName tms end end end | [] => False end. Fixpoint getPubNameInBaseTerms (t:term) (btm:baseTerms) : term := match btm with | btm1::btms => match btm1 with | (Var _) => getPubNameInBaseTerms t btms | (Name nm) => match nm with | Pub pn => Bterm (Name (Pub pn)) | _ => getPubNameInBaseTerms t btms end end | [] => t end. Fixpoint getPubName (t:term) (tm:terms) : term := match tm with | tm1::tms => match tm1 with | Func f bts => getPubNameInBaseTerms t bts | Bterm bt => match bt with | (Var _) => getPubName t tms | (Name nm) => match nm with | Pub pn => Bterm (Name (Pub pn)) | _ => getPubName t tms end end end | [] => t end. Fixpoint b_hasPubName (tm:terms) : bool := match tm with | tm1::tms => match tm1 with | Func f bts => b_hasPubNameInBaseTerms bts | Bterm bt => match bt with | (Var _) => b_hasPubName tms | (Name nm) => match nm with | Pub _ => true | _ => b_hasPubName tms end end end | [] => false end. Fixpoint b_hasFunction (tm:terms) : bool := match tm with | tm1::tms => match tm1 with | Func _ _ => true | _ => b_hasFunction tms end | [] => false end. Fixpoint selectFunctions (tm: terms) : terms := match tm with | Func f bt1::tms => (Func f bt1)::(selectFunctions tms) | _ ::tms => (selectFunctions tms) | [] => [] end. (** ================================================================================ 2C: Extraction of submembers : Functions to extract facts/logs etc. from rules =================================================================================*) Fixpoint premiseFacts (r:rule) : facts := match r with | RuleSetup f1 l f2 => f1 | RuleProto f1 l f2 => f1 end. Fixpoint conclFacts (r:rule) : facts := match r with | RuleSetup f1 l f2 => f2 | RuleProto f1 l f2 => f2 end. Fixpoint allPremiseFacts (rs:(list rule)) : facts := match rs with | [] => [] | r::rst => appendAny (premiseFacts r) (allPremiseFacts rst) end. Fixpoint allConclFacts (rs:(list rule)) : facts := match rs with | [] => [] | r::rst => appendAny (conclFacts r) (allConclFacts rst) end. Fixpoint allFactsRL (rs:(list rule)) : facts := appendAny (allPremiseFacts rs) (allConclFacts rs). Fixpoint labelR (r:rule) : label := match r with | RuleSetup f1 l f2 => l | RuleProto f1 l f2 => l end. Fixpoint getInFactPremise (fp:facts) : facts := match fp with | f1::fs => match f1 with | IN _ => appendAny [f1](getInFactPremise fs) | OUT _ => (getInFactPremise fs) | K _ => (getInFactPremise fs) | STATE _ _ => (getInFactPremise fs) | FR_P _ => (getInFactPremise fs) end | [] => [] end. Fixpoint getFrFactPremise (fp:facts) : facts := match fp with | f1::fs => match f1 with | IN _ => (getFrFactPremise fs) | OUT _ => (getFrFactPremise fs) | K _ => (getFrFactPremise fs) | STATE _ _ => (getFrFactPremise fs) | FR_P _ => appendAny [f1](getFrFactPremise fs) end | [] => [] end. Fixpoint getOutFactConclusion (fp:facts) : facts := match fp with | f1::fs => match f1 with | IN _ => (getOutFactConclusion fs) | OUT _ => appendAny [f1] (getOutFactConclusion fs) | K _ => (getOutFactConclusion fs) | STATE _ _ => (getOutFactConclusion fs) | FR_P _ => (getOutFactConclusion fs) end | [] => [] end. Fixpoint getOutFactProtoRule (rl:rule) : facts := match rl with | (RuleProto fp1 lp fp2) => getOutFactConclusion fp2 | (RuleSetup fp1 lp fp2) => [] end. Fixpoint getInFactProtoRule (rl:rule) : facts := match rl with | (RuleProto fp1 lp fp2) => getInFactPremise fp1 | (RuleSetup fp1 lp fp2) => [] end. Fixpoint getFrFactProtoRule (rl:rule) : facts := match rl with | (RuleProto fp1 lp fp2) => getFrFactPremise fp1 | (RuleSetup fp1 lp fp2) => [] end. Fixpoint getFrFactSetupRule (rl:rule) : facts := match rl with | (RuleProto fp1 lp fp2) => [] | (RuleSetup fp1 lp fp2) => getFrFactPremise fp1 end. Fixpoint removeOutInfromFactList (fs: facts) : facts := match fs with | [] => [] | fs1::fss => match fs1 with | IN _ => (removeOutInfromFactList fss) | OUT _ => (removeOutInfromFactList fss) | K _ => appendAny [fs1] (removeOutInfromFactList fss) | STATE _ _ => appendAny [fs1] (removeOutInfromFactList fss) | FR_P _ => appendAny [fs1] (removeOutInfromFactList fss) end end. (* For Tamarin Reduction *) Fixpoint getStateFacts (fp:facts) : facts := match fp with | f1::fs => match f1 with | IN _ => (getStateFacts fs) | OUT _ => (getStateFacts fs) | K _ => (getStateFacts fs) | STATE _ _ => appendAny [f1](getStateFacts fs) | FR_P _ => (getStateFacts fs) end | [] => [] end. Fixpoint getLogRL (rl: ruleList) : trace := match rl with | [] => [] | rl1::rls => match labelR rl1 with | LoggedLabel lg lb1 => (LoggedLabel lg [])::(getLogRL rls) | _ => getLogRL rls end end. Fixpoint onlyBasicLogsInRL (rl: ruleList) : Prop := match rl with | [] => True | rl1::rls => match labelR rl1 with | BasicLabel lb1 => True /\ (onlyBasicLogsInRL rls) | _ => False end end. Fixpoint getTermsAL (al:actionLabel) : terms := match al with | ActLabel NM TRMS => TRMS end. Fixpoint getTermsLoggedLabel (l1:label) : terms := match l1 with | (LoggedSIDLabel t al lb) => (Bterm t):: (getTermsAL al) | (LoggedLabel al lb) => [] | (BasicLabel als) => [] end. (* Fixpoint getTermsLabel (l1:label) : terms := match l1 with | (LoggedSIDLabel t al lb) => (Bterm t):: (getTermsAL al) | (LoggedLabel al lb) => [] | (BasicLabel als) => [] end. *) Fixpoint getFreshProtoNamesinAL (al: list actionLabel) : list freshNameProto := match al with | al1::als => match al1 with | ActLabel (Fresh_P fp) t => fp ::(getFreshProtoNamesinAL als) | _ => getFreshProtoNamesinAL als end | [] => [] end. Fixpoint getFreshProtoNamesinLabel (lb: label) : list freshNameProto := match lb with | LoggedSIDLabel t al als => match al with | ActLabel (Fresh_P fp) t => fp :: (getFreshProtoNamesinAL als) | _ => getFreshProtoNamesinAL als end | BasicLabel al => [] | LoggedLabel al als => [] (*We assume that there will not be any label of this type after annotating the rules with SID*) end. (* "getSID lbl SID" holds if "SID" used in the label "lbl". *) Inductive getSID : label -> baseTerm -> Prop := | validSID : forall t al als, getSID (LoggedSIDLabel t al als) t. Inductive getParsFromLog : label -> terms -> Prop := | validTerms : forall t alname alterms als, getParsFromLog (LoggedSIDLabel t (alname alterms) als) alterms. Fixpoint getLogTrace (t:trace) : trace := match t with | [] => [] | h::ts => match h with | LoggedLabel lg lb1 => (LoggedLabel lg [])::(getLogTrace ts) | _ => getLogTrace ts end end. (**===================================== constants and variables in term ========================================*) Definition constantsInBaseTerm (bt:baseTerm) : variables := match bt with | Name (Pub v) => [v] | _ => [] end. Definition constantsInBaseTerms : (list baseTerm) -> variables := mapListFunction constantsInBaseTerm. Definition constantsInTerm (t:term) : variables := match t with | Func fn bts => constantsInBaseTerms bts | Bterm bt => constantsInBaseTerm bt end. Definition constantsInTerms : (list term) -> variables := mapListFunction constantsInTerm. (* Some general functions for working with the syntax *) Definition variablesInBaseTerm (bt:baseTerm) : variables := match bt with | Var v => [v] | _ => [] end. Definition variablesInBaseTerms : (list baseTerm) -> variables := mapListFunction variablesInBaseTerm. Definition variablesInTerm (t:term) : variables := match t with | Func fn bts => variablesInBaseTerms bts | Bterm bt => variablesInBaseTerm bt end. Definition variablesInTerms : (list term) -> variables := mapListFunction variablesInTerm. Definition variablesInFact (f:fact) : variables := match f with | IN ts => variablesInTerms ts | OUT ts => variablesInTerms ts | K ts => variablesInTerms ts | STATE n ts => variablesInTerms ts | FR_P bt => variablesInBaseTerm bt end. Definition variablesInRule (r:rule) : variables := match r with | RuleSetup f1 l f2 => mapListFunction variablesInFact f1 | RuleProto f1 l f2 => mapListFunction variablesInFact f1 end. (** Some general functions for working with the syntax *) Definition freshNameInBaseTerm (bt:baseTerm) : list freshNameProto := match bt with | Name nm => match nm with | Fresh_P fp => [fp] | _ => [] end | _ => [] end. Definition freshNamesInBaseTerms : (list baseTerm) -> list freshNameProto := mapListFunction freshNameInBaseTerm. Definition freshNamesInTerm (t:term) : list freshNameProto := match t with | Func fn bts => freshNamesInBaseTerms bts | Bterm bt => freshNameInBaseTerm bt end. Definition freshNamesInTerms : (list term) -> list freshNameProto := mapListFunction freshNamesInTerm. Fixpoint getFreshProtoNamesinLoggedSIDTrace (tr: trace) : list freshNameProto := match tr with | [] => [] | h::ts => match h with | LoggedSIDLabel t al als => match al with | ActLabel nm t => appendAny (freshNamesInTerms t) (getFreshProtoNamesinLoggedSIDTrace ts) end | BasicLabel al => (getFreshProtoNamesinLoggedSIDTrace ts) | LoggedLabel al lb => (getFreshProtoNamesinLoggedSIDTrace ts) end end. Fixpoint getFreshProtoNamesinTrace (tr: trace) : list freshNameProto := match tr with | [] => [] | h::ts => match h with | LoggedLabel al als => match al with | ActLabel nm t => appendAny (freshNamesInTerms t) (getFreshProtoNamesinTrace ts) end | BasicLabel al => (getFreshProtoNamesinTrace ts) | LoggedSIDLabel t al lb => (getFreshProtoNamesinTrace ts) end end. Definition getFreshProtoNamesList : (list trace) -> list freshNameProto := mapListFunction getFreshProtoNamesinTrace. Fixpoint getFrNamesPremiseProto (fp:facts) : list freshNameProto := match fp with | f1::fs => match f1 with | IN _ => (getFrNamesPremiseProto fs) | OUT _ => (getFrNamesPremiseProto fs) | K _ => (getFrNamesPremiseProto fs) | STATE _ _ => (getFrNamesPremiseProto fs) | FR_P fp1 => match fp1 with | (Var _) => getFrNamesPremiseProto fs | (Name nm) => match nm with | Fresh_S _ => (getFrNamesPremiseProto fs) | Fresh_P fn => fn::(getFrNamesPremiseProto fs) | Pub _ => (getFrNamesPremiseProto fs) end end end | [] => [] end. Fixpoint getFrNamesPremiseSetup (fp:facts) : list freshNameSetup := match fp with | f1::fs => match f1 with | IN _ => (getFrNamesPremiseSetup fs) | OUT _ => (getFrNamesPremiseSetup fs) | K _ => (getFrNamesPremiseSetup fs) | STATE _ _ => (getFrNamesPremiseSetup fs) | FR_P fp1 => match fp1 with | (Var _) => getFrNamesPremiseSetup fs | (Name nm) => match nm with | Fresh_S fss => (fss::getFrNamesPremiseSetup fs) | Fresh_P _ => (getFrNamesPremiseSetup fs) | Pub _ => (getFrNamesPremiseSetup fs) end end end | [] => [] end. Fixpoint InFresh (fr : freshNameProto) (frlist : list freshNameProto) : bool := match (member fr frlist) with | True => true end. Fixpoint commonFreshNames (f1:list freshNameProto) (f2:list freshNameProto): list freshNameProto := match f1 with | [] => [] | f11 :: f1s => if InFreshList f11 f2 then (f11::(commonFreshNames f1s f2)) else commonFreshNames f1s f2 end. Fixpoint getVarsInTemplate (tr:trace) : list variable := match tr with | [] => [] | h::ts => match h with | LoggedSIDLabel t al als => match al with | ActLabel nm t => appendAny (variablesInTerms t) (getVarsInTemplate ts) end | BasicLabel al => (getVarsInTemplate ts) | LoggedLabel al lb => (getVarsInTemplate ts) end end.