50 | b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2" |
50 | b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2" |
51 | b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]" |
51 | b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]" |
52 |
52 |
53 equivariance beta |
53 equivariance beta |
54 |
54 |
55 (* HERE 1 *) |
|
56 nominal_inductive beta |
55 nominal_inductive beta |
57 avoids b3: x |
56 avoids b3: x |
|
57 | b4: x |
58 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
58 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
59 |
59 |
60 (* This also works, but we cannot have them together: *) |
60 |
61 (*nominal_inductive beta |
|
62 avoids b4: x |
|
63 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)*) |
|
64 |
|
65 (* But I need a combination, possibly with an 'and' syntax: |
|
66 nominal_inductive beta |
|
67 avoids b3: x and b4: x |
|
68 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
|
69 *) |
|
70 |
61 |
71 (* The combination should look like this: *) |
62 (* The combination should look like this: *) |
72 lemma beta_strong_induct: |
|
73 assumes "x1 \<longrightarrow>b x2" |
|
74 and "\<And>t1 t2 s c. \<lbrakk> t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (App t1 s) (App t2 s)" |
|
75 and "\<And>s1 s2 t c. \<lbrakk> s1 \<longrightarrow>b s2; \<And>c. P c s1 s2\<rbrakk> \<Longrightarrow> P c (App t s1) (App t s2)" |
|
76 and "\<And>t1 t2 x c. \<lbrakk>{atom x} \<sharp>* c; t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (Lam [x]. t1) (Lam [x]. t2)" |
|
77 and "\<And>x s t c. \<lbrakk>{atom x} \<sharp>* c; atom x \<sharp> s\<rbrakk> \<Longrightarrow> P c (App (Lam [x]. t) s) (t [x ::= s])" |
|
78 shows "P (c\<Colon>'a\<Colon>fs) x1 x2" |
|
79 sorry |
|
80 |
63 |
81 inductive |
64 inductive |
82 beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80) |
65 beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80) |
83 where |
66 where |
84 bs1[intro, simp]: "M \<longrightarrow>b* M" |
67 bs1[intro, simp]: "M \<longrightarrow>b* M" |
199 (auto simp add: fresh_fact forget) |
182 (auto simp add: fresh_fact forget) |
200 |
183 |
201 lemma beta_subst2_pre: |
184 lemma beta_subst2_pre: |
202 assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]" |
185 assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]" |
203 using assms |
186 using assms |
204 (* HERE 3: nominal_induct doesn't work - leaves the assumption *) |
187 apply (nominal_induct avoiding: x C rule: beta.strong_induct) |
205 (* apply (nominal_induct avoiding: x C rule: beta_strong_induct)*) |
|
206 apply - |
|
207 apply (erule beta_strong_induct[of A B "\<lambda>c A B. A [(fst c) ::= (snd c)] \<longrightarrow>b* B [(fst c) ::= (snd c)]" "(x, C)", simplified]) |
|
208 apply (auto simp add: App_beta fresh_star_def fresh_Pair Lam_beta)[3] |
188 apply (auto simp add: App_beta fresh_star_def fresh_Pair Lam_beta)[3] |
209 apply (subst substitution_lemma) |
189 apply (subst substitution_lemma) |
210 apply (auto simp add: fresh_star_def fresh_Pair fresh_at_base)[2] |
190 apply (auto simp add: fresh_star_def fresh_Pair fresh_at_base)[2] |
211 apply (auto simp add: fresh_star_def fresh_Pair) |
191 apply (auto simp add: fresh_star_def fresh_Pair) |
212 apply (rule beta_star.intros) |
192 apply (rule beta_star.intros) |