82 assume "\<And>xa. x = Var xa \<Longrightarrow> P" "\<And>M N. x = M \<cdot> N \<Longrightarrow> P" "\<And>xa M. x = \<integral> xa. M \<Longrightarrow> P" |
82 assume "\<And>xa. x = Var xa \<Longrightarrow> P" "\<And>M N. x = M \<cdot> N \<Longrightarrow> P" "\<And>xa M. x = \<integral> xa. M \<Longrightarrow> P" |
83 then show "P" |
83 then show "P" |
84 by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust) |
84 by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust) |
85 (auto simp add: Abs1_eq_iff fresh_star_def)[3] |
85 (auto simp add: Abs1_eq_iff fresh_star_def)[3] |
86 next |
86 next |
87 fix x :: var and M and xa :: var and Ma |
87 fix x :: name and M and xa :: name and Ma |
88 assume "[[atom x]]lst. M = [[atom xa]]lst. Ma" |
88 assume "[[atom x]]lst. M = [[atom xa]]lst. Ma" |
89 "eqvt_at Numeral_sumC M" |
89 "eqvt_at Numeral_sumC M" |
90 then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma" |
90 then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma" |
91 apply - |
91 apply - |
92 apply (erule Abs_lst1_fcb) |
92 apply (erule Abs_lst1_fcb) |
108 |
108 |
109 lemma fresh_numeral[simp]: |
109 lemma fresh_numeral[simp]: |
110 "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y" |
110 "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y" |
111 unfolding fresh_def by simp |
111 unfolding fresh_def by simp |
112 |
112 |
113 fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where |
113 fun app_lst :: "name \<Rightarrow> lam list \<Rightarrow> lam" where |
114 "app_lst n [] = Var n" |
114 "app_lst n [] = Var n" |
115 | "app_lst n (h # t) = (app_lst n t) \<cdot> h" |
115 | "app_lst n (h # t) = (app_lst n t) \<cdot> h" |
116 |
116 |
117 lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)" |
117 lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)" |
118 by (induct ts arbitrary: t p) (simp_all add: eqvts) |
118 by (induct ts arbitrary: t p) (simp_all add: eqvts) |
132 Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000) |
132 Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000) |
133 where |
133 where |
134 [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))" |
134 [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))" |
135 unfolding eqvt_def Ltgt_graph_def |
135 unfolding eqvt_def Ltgt_graph_def |
136 apply (rule, perm_simp, rule, rule) |
136 apply (rule, perm_simp, rule, rule) |
137 apply (rule_tac x="x" and ?'a="var" in obtain_fresh) |
137 apply (rule_tac x="x" and ?'a="name" in obtain_fresh) |
138 apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base) |
138 apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base) |
139 apply (simp add: eqvts swap_fresh_fresh) |
139 apply (simp add: eqvts swap_fresh_fresh) |
140 apply (case_tac "x = xa") |
140 apply (case_tac "x = xa") |
141 apply simp_all |
141 apply simp_all |
142 apply (subgoal_tac "eqvt app_lst") |
142 apply (subgoal_tac "eqvt app_lst") |
147 termination (eqvt) by lexicographic_order |
147 termination (eqvt) by lexicographic_order |
148 |
148 |
149 lemma ltgt_eq_iff[simp]: |
149 lemma ltgt_eq_iff[simp]: |
150 "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N" |
150 "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N" |
151 proof auto |
151 proof auto |
152 obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
152 obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
153 then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all |
153 then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all |
154 then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps) |
154 then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps) |
155 qed |
155 qed |
156 |
156 |
157 lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M" |
157 lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M" |
158 proof - |
158 proof - |
159 obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
159 obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
160 then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all |
160 then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all |
161 then show ?thesis |
161 then show ?thesis |
162 apply (subst Ltgt.simps) |
162 apply (subst Ltgt.simps) |
163 apply (simp add: fresh_Cons fresh_Nil) |
163 apply (simp add: fresh_Cons fresh_Nil) |
164 apply (rule b3, rule bI, simp add: b1) |
164 apply (rule b3, rule bI, simp add: b1) |
165 done |
165 done |
166 qed |
166 qed |
167 |
167 |
168 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P" |
168 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P" |
169 proof - |
169 proof - |
170 obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto |
170 obtain x :: name where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto |
171 then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all |
171 then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all |
172 then have s: "Var x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp |
172 then have s: "Var x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp |
173 show ?thesis using * |
173 show ?thesis using * |
174 apply (subst Ltgt.simps) |
174 apply (subst Ltgt.simps) |
175 apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim) |
175 apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim) |
179 qed |
179 qed |
180 |
180 |
181 lemma supp_ltgt[simp]: |
181 lemma supp_ltgt[simp]: |
182 "supp \<guillemotleft>t\<guillemotright> = supp t" |
182 "supp \<guillemotleft>t\<guillemotright> = supp t" |
183 proof - |
183 proof - |
184 obtain x :: var where *:"atom x \<sharp> t" using obtain_fresh by auto |
184 obtain x :: name where *:"atom x \<sharp> t" using obtain_fresh by auto |
185 show ?thesis using * |
185 show ?thesis using * |
186 by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def) |
186 by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def) |
187 qed |
187 qed |
188 |
188 |
189 lemma fresh_ltgt[simp]: |
189 lemma fresh_ltgt[simp]: |
192 by (simp_all add: fresh_def supp_Cons supp_Nil supp_Pair) |
192 by (simp_all add: fresh_def supp_Cons supp_Nil supp_Pair) |
193 |
193 |
194 lemma Ltgt1_subst[simp]: |
194 lemma Ltgt1_subst[simp]: |
195 "\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>" |
195 "\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>" |
196 proof - |
196 proof - |
197 obtain x :: var where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast |
197 obtain x :: name where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast |
198 have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp |
198 have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp |
199 then show ?thesis |
199 then show ?thesis |
200 apply (subst Ltgt.simps) |
200 apply (subst Ltgt.simps) |
201 using a apply (simp add: fresh_Nil fresh_Cons fresh_Pair_elim) |
201 using a apply (simp add: fresh_Nil fresh_Cons fresh_Pair_elim) |
202 apply (subst Ltgt.simps) |
202 apply (subst Ltgt.simps) |
240 |
240 |
241 lemma F3_app: |
241 lemma F3_app: |
242 assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *) |
242 assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *) |
243 shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))" |
243 shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))" |
244 proof - |
244 proof - |
245 obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast |
245 obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast |
246 obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast |
246 obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast |
247 have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z" |
247 have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z" |
248 using b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
248 using b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
249 have **: |
249 have **: |
250 "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
250 "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
251 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
251 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |