1 theory BetaCR |
1 theory BetaCR |
2 imports |
2 imports CR |
3 "../Nominal2" |
|
4 begin |
3 begin |
5 |
4 |
6 atom_decl name |
5 (* TODO1: Does not work:*) |
7 |
|
8 nominal_datatype lam = |
|
9 Var "name" |
|
10 | App "lam" "lam" |
|
11 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
12 |
|
13 nominal_primrec |
|
14 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
15 where |
|
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
19 unfolding eqvt_def subst_graph_def |
|
20 apply (rule, perm_simp, rule) |
|
21 apply(rule TrueI) |
|
22 apply(auto simp add: lam.distinct lam.eq_iff) |
|
23 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
24 apply(blast)+ |
|
25 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
|
26 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
27 apply(simp_all add: Abs_fresh_iff) |
|
28 apply(simp add: fresh_star_def fresh_Pair) |
|
29 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
30 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
31 done |
|
32 |
|
33 termination (eqvt) |
|
34 by lexicographic_order |
|
35 |
|
36 lemma fresh_fact: |
|
37 fixes z::"name" |
|
38 assumes a: "atom z \<sharp> s" |
|
39 and b: "z = y \<or> atom z \<sharp> t" |
|
40 shows "atom z \<sharp> t[y ::= s]" |
|
41 using a b |
|
42 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
|
43 (auto simp add: lam.fresh fresh_at_base) |
|
44 |
|
45 inductive |
|
46 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
|
47 where |
|
48 b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s" |
|
49 | b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2" |
|
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]" |
|
52 |
|
53 equivariance beta |
|
54 |
|
55 nominal_inductive beta |
|
56 avoids b3: x |
|
57 | b4: x |
|
58 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
|
59 |
|
60 |
|
61 |
|
62 (* The combination should look like this: *) |
|
63 |
|
64 inductive |
|
65 beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80) |
|
66 where |
|
67 bs1[intro, simp]: "M \<longrightarrow>b* M" |
|
68 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3" |
|
69 |
|
70 lemma beta_star_trans: |
|
71 assumes "A \<longrightarrow>b* B" |
|
72 and "B \<longrightarrow>b* C" |
|
73 shows "A \<longrightarrow>b* C" |
|
74 using assms(2) assms(1) |
|
75 by induct auto |
|
76 |
|
77 (* HERE 2: Does not work:*) |
|
78 |
6 |
79 (* equivariance beta_star *) |
7 (* equivariance beta_star *) |
80 |
8 |
81 (* proved manually below. *) |
9 (* proved manually below. *) |
82 |
10 |
83 lemma eqvt_helper: "x1 \<longrightarrow>b* x2 \<Longrightarrow> (p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2)" |
11 lemma eqvt_helper: "x1 \<longrightarrow>b* x2 \<Longrightarrow> (p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2)" |
84 apply (erule beta_star.induct) |
12 by (erule beta_star.induct) |
85 apply auto |
13 (metis beta.eqvt bs2 bs1)+ |
86 using eqvt(1) bs2 |
|
87 by blast |
|
88 |
14 |
89 lemma [eqvt]: "p \<bullet> (x1 \<longrightarrow>b* x2) = ((p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2))" |
15 lemma [eqvt]: "p \<bullet> (x1 \<longrightarrow>b* x2) = ((p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2))" |
90 apply rule |
16 apply rule |
91 apply (drule permute_boolE) |
17 apply (drule permute_boolE) |
92 apply (erule eqvt_helper) |
18 apply (erule eqvt_helper) |
107 assumes "t \<approx> s" |
33 assumes "t \<approx> s" |
108 shows "s \<approx> t" |
34 shows "s \<approx> t" |
109 using assms unfolding equ_def |
35 using assms unfolding equ_def |
110 by auto |
36 by auto |
111 |
37 |
112 (* can be ported from nominal1 *) |
|
113 lemma cr: |
|
114 assumes "t \<longrightarrow>b* t1" and "t \<longrightarrow>b* t2" shows "\<exists>t3. t1 \<longrightarrow>b* t3 \<and> t2 \<longrightarrow>b* t3" |
|
115 sorry |
|
116 |
|
117 lemma equ_trans: |
38 lemma equ_trans: |
118 assumes "A \<approx> B" "B \<approx> C" |
39 assumes "A \<approx> B" "B \<approx> C" |
119 shows "A \<approx> C" |
40 shows "A \<approx> C" |
120 using assms unfolding equ_def |
41 using assms unfolding equ_def |
121 proof (elim exE conjE) |
42 proof (elim exE conjE) |
122 fix D E |
43 fix D E |
123 assume a: "A \<longrightarrow>b* D" "B \<longrightarrow>b* D" "B \<longrightarrow>b* E" "C \<longrightarrow>b* E" |
44 assume a: "A \<longrightarrow>b* D" "B \<longrightarrow>b* D" "B \<longrightarrow>b* E" "C \<longrightarrow>b* E" |
124 then obtain F where "D \<longrightarrow>b* F" "E \<longrightarrow>b* F" using cr by blast |
45 then obtain F where "D \<longrightarrow>b* F" "E \<longrightarrow>b* F" using CR_for_Beta_star by blast |
125 then have "A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" using a beta_star_trans by blast |
46 then have "A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" using a bs3 by blast |
126 then show "\<exists>F. A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" by blast |
47 then show "\<exists>F. A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" by blast |
127 qed |
48 qed |
128 |
49 |
129 lemma App_beta: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> App A C \<longrightarrow>b* App B D" |
50 lemma App_beta: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> App A C \<longrightarrow>b* App B D" |
130 apply (erule beta_star.induct) |
51 apply (erule beta_star.induct) |
144 done |
65 done |
145 |
66 |
146 lemma [quot_respect]: |
67 lemma [quot_respect]: |
147 shows "(op = ===> equ) Var Var" |
68 shows "(op = ===> equ) Var Var" |
148 and "(equ ===> equ ===> equ) App App" |
69 and "(equ ===> equ ===> equ) App App" |
149 and "(op = ===> equ ===> equ) BetaCR.Lam BetaCR.Lam" |
70 and "(op = ===> equ ===> equ) CR.Lam CR.Lam" |
150 unfolding fun_rel_def equ_def |
71 unfolding fun_rel_def equ_def |
151 apply auto |
72 apply auto |
152 apply (rule_tac x="App r ra" in exI) |
73 apply (rule_tac x="App r ra" in exI) |
153 apply (auto simp add: App_beta) |
74 apply (auto simp add: App_beta) |
154 apply (rule_tac x="Lam [x]. r" in exI) |
75 apply (rule_tac x="Lam [x]. r" in exI) |
162 lemma beta_subst1: "B \<longrightarrow>b* C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]" |
83 lemma beta_subst1: "B \<longrightarrow>b* C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]" |
163 apply (erule beta_star.induct) |
84 apply (erule beta_star.induct) |
164 apply auto |
85 apply auto |
165 apply (subgoal_tac "A [x ::= M2] \<longrightarrow>b* A [x ::= M3]") |
86 apply (subgoal_tac "A [x ::= M2] \<longrightarrow>b* A [x ::= M3]") |
166 apply (rotate_tac 1) |
87 apply (rotate_tac 1) |
167 apply (erule beta_star_trans) |
88 apply (erule bs3) |
168 apply assumption |
89 apply assumption |
169 apply (simp add: beta_subst1_pre) |
90 apply (simp add: beta_subst1_pre) |
170 done |
91 done |
171 |
|
172 lemma forget: |
|
173 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
|
174 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
|
175 (auto simp add: lam.fresh fresh_at_base) |
|
176 |
|
177 lemma substitution_lemma: |
|
178 assumes a: "x \<noteq> y" "atom x \<sharp> u" |
|
179 shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]" |
|
180 using a |
|
181 by (nominal_induct t avoiding: x y s u rule: lam.strong_induct) |
|
182 (auto simp add: fresh_fact forget) |
|
183 |
92 |
184 lemma beta_subst2_pre: |
93 lemma beta_subst2_pre: |
185 assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]" |
94 assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]" |
186 using assms |
95 using assms |
187 apply (nominal_induct avoiding: x C rule: beta.strong_induct) |
96 apply (nominal_induct avoiding: x C rule: beta.strong_induct) |
198 lemma beta_subst2: "A \<longrightarrow>b* B \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= C]" |
107 lemma beta_subst2: "A \<longrightarrow>b* B \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= C]" |
199 apply (erule beta_star.induct) |
108 apply (erule beta_star.induct) |
200 apply auto |
109 apply auto |
201 apply (subgoal_tac "M2[x ::= C] \<longrightarrow>b* M3[x ::= C]") |
110 apply (subgoal_tac "M2[x ::= C] \<longrightarrow>b* M3[x ::= C]") |
202 apply (rotate_tac 1) |
111 apply (rotate_tac 1) |
203 apply (erule beta_star_trans) |
112 apply (erule bs3) |
204 apply assumption |
113 apply assumption |
205 apply (simp add: beta_subst2_pre) |
114 apply (simp add: beta_subst2_pre) |
206 done |
115 done |
207 |
116 |
208 lemma beta_subst: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= D]" |
117 lemma beta_subst: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= D]" |
209 using beta_subst1 beta_subst2 beta_star_trans by metis |
118 using beta_subst1 beta_subst2 bs3 by metis |
210 |
119 |
211 lemma subst_rsp_pre: |
120 lemma subst_rsp_pre: |
212 "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]" |
121 "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]" |
213 unfolding equ_def |
122 unfolding equ_def |
214 apply auto |
123 apply auto |
232 (erule equ_trans, assumption) |
141 (erule equ_trans, assumption) |
233 |
142 |
234 quotient_definition "QVar::name \<Rightarrow> qlam" is Var |
143 quotient_definition "QVar::name \<Rightarrow> qlam" is Var |
235 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App |
144 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App |
236 quotient_definition QLam ("QLam [_]._") |
145 quotient_definition QLam ("QLam [_]._") |
237 where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is BetaCR.Lam |
146 where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is CR.Lam |
238 |
147 |
239 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted] |
148 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted] |
240 lemmas qlam_induct = lam.induct[quot_lifted] |
149 lemmas qlam_induct = lam.induct[quot_lifted] |
241 |
150 |
242 instantiation qlam :: pt |
151 instantiation qlam :: pt |