|
1 theory Term1 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 section {*** lets with binding patterns ***} |
|
8 |
|
9 datatype rtrm1 = |
|
10 rVr1 "name" |
|
11 | rAp1 "rtrm1" "rtrm1" |
|
12 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
13 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
14 and bp = |
|
15 BUnit |
|
16 | BVr "name" |
|
17 | BPr "bp" "bp" |
|
18 |
|
19 print_theorems |
|
20 |
|
21 (* to be given by the user *) |
|
22 |
|
23 primrec |
|
24 bv1 |
|
25 where |
|
26 "bv1 (BUnit) = {}" |
|
27 | "bv1 (BVr x) = {atom x}" |
|
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
29 |
|
30 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Term1.rtrm1", "Term1.bp"] *} |
|
31 thm permute_rtrm1_permute_bp.simps |
|
32 |
|
33 local_setup {* |
|
34 snd o define_fv_alpha "Term1.rtrm1" |
|
35 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
|
36 [[], [[]], [[], []]]] *} |
|
37 |
|
38 notation |
|
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
|
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
|
41 thm alpha_rtrm1_alpha_bp.intros |
|
42 thm fv_rtrm1_fv_bp.simps |
|
43 |
|
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
|
45 thm alpha1_inj |
|
46 |
|
47 local_setup {* |
|
48 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
|
49 *} |
|
50 |
|
51 local_setup {* |
|
52 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
|
53 *} |
|
54 |
|
55 |
|
56 local_setup {* |
|
57 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
|
58 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) |
|
59 *} |
|
60 print_theorems |
|
61 |
|
62 lemma alpha1_eqvt_proper[eqvt]: |
|
63 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
|
64 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
|
65 apply (simp_all only: eqvts) |
|
66 apply rule |
|
67 apply (simp_all add: alpha1_eqvt) |
|
68 apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"]) |
|
69 apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"]) |
|
70 apply (simp_all only: alpha1_eqvt) |
|
71 apply rule |
|
72 apply (simp_all add: alpha1_eqvt) |
|
73 apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"]) |
|
74 apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"]) |
|
75 apply (simp_all only: alpha1_eqvt) |
|
76 done |
|
77 |
|
78 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
|
79 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
|
80 thm alpha1_equivp |
|
81 |
|
82 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
|
83 (rtac @{thm alpha1_equivp(1)} 1) *} |
|
84 |
|
85 local_setup {* |
|
86 (fn ctxt => ctxt |
|
87 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
|
88 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
|
89 |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1})) |
|
90 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
|
91 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
|
92 *} |
|
93 print_theorems |
|
94 |
|
95 thm alpha_rtrm1_alpha_bp.induct |
|
96 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] |
|
97 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
|
98 local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] |
|
99 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
100 local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] |
|
101 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
102 local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] |
|
103 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
104 local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] |
|
105 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
106 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}] |
|
107 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
|
108 |
|
109 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
|
110 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
|
111 |
|
112 setup {* define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
|
113 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
|
114 |
|
115 lemmas |
|
116 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
117 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
|
118 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted] |
|
119 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
120 |
|
121 lemma supports: |
|
122 "(supp (atom x)) supports (Vr1 x)" |
|
123 "(supp t \<union> supp s) supports (Ap1 t s)" |
|
124 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
|
125 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
|
126 "{} supports BUnit" |
|
127 "(supp (atom x)) supports (BVr x)" |
|
128 "(supp a \<union> supp b) supports (BPr a b)" |
|
129 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) |
|
130 apply(rule_tac [!] allI)+ |
|
131 apply(rule_tac [!] impI) |
|
132 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
|
133 apply(simp_all add: fresh_atom) |
|
134 done |
|
135 |
|
136 lemma rtrm1_bp_fs: |
|
137 "finite (supp (x :: trm1))" |
|
138 "finite (supp (b :: bp))" |
|
139 apply (induct x and b rule: trm1_bp_inducts) |
|
140 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
|
141 apply(simp_all add: supp_atom) |
|
142 done |
|
143 |
|
144 instance trm1 :: fs |
|
145 apply default |
|
146 apply (rule rtrm1_bp_fs(1)) |
|
147 done |
|
148 |
|
149 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
|
150 apply(induct bp rule: trm1_bp_inducts(2)) |
|
151 apply(simp_all) |
|
152 done |
|
153 |
|
154 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}" |
|
155 apply auto |
|
156 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
|
157 apply auto |
|
158 done |
|
159 |
|
160 lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" |
|
161 apply rule |
|
162 apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2)) |
|
163 apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)]) |
|
164 done |
|
165 |
|
166 lemma alpha_bp_eq: "alpha_bp = (op =)" |
|
167 apply (rule ext)+ |
|
168 apply (rule alpha_bp_eq_eq) |
|
169 done |
|
170 |
|
171 lemma supp_fv: |
|
172 "supp t = fv_trm1 t" |
|
173 "supp b = fv_bp b" |
|
174 apply(induct t and b rule: trm1_bp_inducts) |
|
175 apply(simp_all) |
|
176 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
177 apply(simp only: supp_at_base[simplified supp_def]) |
|
178 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
179 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
180 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
|
181 apply(simp add: supp_Abs fv_trm1) |
|
182 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
|
183 apply(simp add: alpha1_INJ) |
|
184 apply(simp add: Abs_eq_iff) |
|
185 apply(simp add: alpha_gen.simps) |
|
186 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
|
187 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
|
188 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
|
189 apply(simp (no_asm) add: supp_def permute_trm1) |
|
190 apply(simp add: alpha1_INJ alpha_bp_eq) |
|
191 apply(simp add: Abs_eq_iff) |
|
192 apply(simp add: alpha_gen) |
|
193 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
|
194 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) |
|
195 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
|
196 apply(simp (no_asm) add: supp_def eqvts) |
|
197 apply(fold supp_def) |
|
198 apply(simp add: supp_at_base) |
|
199 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
|
200 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
|
201 done |
|
202 |
|
203 lemma trm1_supp: |
|
204 "supp (Vr1 x) = {atom x}" |
|
205 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
|
206 "supp (Lm1 x t) = (supp t) - {atom x}" |
|
207 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
|
208 by (simp_all add: supp_fv fv_trm1 fv_eq_bv) |
|
209 |
|
210 lemma trm1_induct_strong: |
|
211 assumes "\<And>name b. P b (Vr1 name)" |
|
212 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
|
213 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
|
214 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
|
215 shows "P a rtrma" |
|
216 sorry |
|
217 |
|
218 end |