equal
deleted
inserted
replaced
15 bn |
15 bn |
16 where |
16 where |
17 "bn ANil = []" |
17 "bn ANil = []" |
18 | "bn (ACons x t as) = (atom x) # (bn as)" |
18 | "bn (ACons x t as) = (atom x) # (bn as)" |
19 |
19 |
20 nominal_primrec substrec where |
20 nominal_function substrec where |
21 "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))" |
21 "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))" |
22 | "substrec fa fl fd y z (App l r) = fa l r" |
22 | "substrec fa fl fd y z (App l r) = fa l r" |
23 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow> |
23 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow> |
24 substrec fa fl fd y z (Let as t) = fl as t" |
24 substrec fa fl fd y z (Let as t) = fl as t" |
25 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> \<not>(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow> |
25 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> \<not>(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow> |
53 apply clarify |
53 apply clarify |
54 apply metis |
54 apply metis |
55 done |
55 done |
56 termination (eqvt) by lexicographic_order |
56 termination (eqvt) by lexicographic_order |
57 |
57 |
58 nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where |
58 nominal_function substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where |
59 "substarec fac ANil = ANil" |
59 "substarec fac ANil = ANil" |
60 | "substarec fac (ACons x t as) = fac x t as" |
60 | "substarec fac (ACons x t as) = fac x t as" |
61 unfolding eqvt_def substarec_graph_def |
61 unfolding eqvt_def substarec_graph_def |
62 apply (rule, perm_simp, rule, rule) |
62 apply (rule, perm_simp, rule, rule) |
63 apply (case_tac x) |
63 apply (case_tac x) |