36 height :: "lam \<Rightarrow> int" |
36 height :: "lam \<Rightarrow> int" |
37 where |
37 where |
38 "height (Var x) = 1" |
38 "height (Var x) = 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
40 | "height (Lam [x].t) = height t + 1" |
40 | "height (Lam [x].t) = height t + 1" |
41 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
41 apply(simp add: eqvt_def height_graph_def) |
42 unfolding eqvt_def |
42 apply (rule, perm_simp, rule) |
43 apply(rule allI) |
43 apply(rule TrueI) |
44 apply(simp add: permute_fun_def) |
|
45 apply(rule ext) |
|
46 apply(rule ext) |
|
47 apply(simp add: permute_bool_def) |
|
48 apply(rule iffI) |
|
49 apply(drule_tac x="p" in meta_spec) |
|
50 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
51 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
52 apply(simp) |
|
53 apply(drule_tac x="-p" in meta_spec) |
|
54 apply(drule_tac x="x" in meta_spec) |
|
55 apply(drule_tac x="xa" in meta_spec) |
|
56 apply(simp) |
|
57 apply(erule height_graph.induct) |
|
58 apply(perm_simp) |
|
59 apply(rule height_graph.intros) |
|
60 apply(perm_simp) |
|
61 apply(rule height_graph.intros) |
|
62 apply(assumption) |
|
63 apply(assumption) |
|
64 apply(perm_simp) |
|
65 apply(rule height_graph.intros) |
|
66 apply(assumption) |
|
67 apply(rule_tac y="x" in lam.exhaust) |
44 apply(rule_tac y="x" in lam.exhaust) |
68 apply(auto simp add: lam.distinct lam.eq_iff) |
45 apply(auto) |
69 apply(simp add: Abs_eq_iff alphas) |
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
70 apply(clarify) |
47 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
71 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
|
72 apply(simp add: pure_supp fresh_star_def) |
|
73 apply(simp add: eqvt_at_def) |
|
74 done |
48 done |
75 |
49 |
76 termination |
50 termination (eqvt) |
77 by (relation "measure size") (simp_all add: lam.size) |
51 by lexicographic_order |
78 |
52 |
79 |
53 |
80 subsection {* Capture-Avoiding Substitution *} |
54 subsection {* Capture-Avoiding Substitution *} |
81 |
55 |
82 nominal_primrec |
56 nominal_primrec |
83 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
84 where |
58 where |
85 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
86 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
87 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
88 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
62 unfolding eqvt_def subst_graph_def |
89 unfolding eqvt_def |
63 apply(rule, perm_simp, rule) |
90 apply(rule allI) |
64 apply(rule TrueI) |
91 apply(simp add: permute_fun_def) |
65 apply(auto) |
92 apply(rule ext) |
66 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
93 apply(rule ext) |
67 apply(blast)+ |
94 apply(simp add: permute_bool_def) |
68 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
95 apply(rule iffI) |
69 apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
96 apply(drule_tac x="p" in meta_spec) |
70 apply(simp_all add: Abs_fresh_iff) |
97 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
71 apply(simp add: fresh_star_def fresh_Pair) |
98 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
72 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
99 apply(simp) |
73 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
100 apply(drule_tac x="-p" in meta_spec) |
|
101 apply(drule_tac x="x" in meta_spec) |
|
102 apply(drule_tac x="xa" in meta_spec) |
|
103 apply(simp) |
|
104 apply(erule subst_graph.induct) |
|
105 apply(perm_simp) |
|
106 apply(rule subst_graph.intros) |
|
107 apply(perm_simp) |
|
108 apply(rule subst_graph.intros) |
|
109 apply(assumption) |
|
110 apply(assumption) |
|
111 apply(perm_simp) |
|
112 apply(rule subst_graph.intros) |
|
113 apply(simp add: fresh_Pair) |
|
114 apply(assumption) |
|
115 apply(auto simp add: lam.distinct lam.eq_iff) |
|
116 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
117 apply(blast)+ |
|
118 apply(simp add: fresh_star_def) |
|
119 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
|
120 apply(subst (asm) Abs_eq_iff2) |
|
121 apply(simp add: alphas atom_eqvt) |
|
122 apply(clarify) |
|
123 apply(rule trans) |
|
124 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
125 apply(rule fresh_star_supp_conv) |
|
126 apply(drule fresh_star_perm_set_conv) |
|
127 apply(simp add: finite_supp) |
|
128 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))") |
|
129 apply(auto simp add: fresh_star_def)[1] |
|
130 apply(simp (no_asm) add: fresh_star_def) |
|
131 apply(rule conjI) |
|
132 apply(simp (no_asm) add: Abs_fresh_iff) |
|
133 apply(clarify) |
|
134 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
135 apply(simp add: finite_supp) |
|
136 apply(simp (no_asm_use) add: fresh_Pair) |
|
137 apply(simp add: Abs_fresh_iff) |
|
138 apply(simp) |
|
139 apply(simp add: Abs_fresh_iff) |
|
140 apply(subgoal_tac "p \<bullet> ya = ya") |
|
141 apply(subgoal_tac "p \<bullet> sa = sa") |
|
142 apply(simp add: atom_eqvt eqvt_at_def) |
|
143 apply(rule perm_supp_eq) |
|
144 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
145 apply(rule perm_supp_eq) |
|
146 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
147 apply(rule conjI) |
|
148 apply(simp add: Abs_fresh_iff) |
|
149 apply(drule sym) |
|
150 apply(simp add: Abs_fresh_iff) |
|
151 done |
74 done |
152 |
75 |
153 termination |
76 termination (eqvt) |
154 by (relation "measure (\<lambda>(t, _, _). size t)") |
77 by lexicographic_order |
155 (simp_all add: lam.size) |
|
156 |
|
157 lemma subst_eqvt[eqvt]: |
|
158 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
|
159 by (induct t x s rule: subst.induct) (simp_all) |
|
160 |
78 |
161 lemma fresh_fact: |
79 lemma fresh_fact: |
162 assumes a: "atom z \<sharp> s" |
80 assumes a: "atom z \<sharp> s" |
163 and b: "z = y \<or> atom z \<sharp> t" |
81 and b: "z = y \<or> atom z \<sharp> t" |
164 shows "atom z \<sharp> t[y ::= s]" |
82 shows "atom z \<sharp> t[y ::= s]" |