1 theory Term4 |
|
2 imports "../NewAlpha" "../Abs" "../Perm" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 section {*** lam with indirect list recursion ***} |
|
8 |
|
9 datatype rtrm4 = |
|
10 rVr4 "name" |
|
11 | rAp4 "rtrm4" "rtrm4 list" |
|
12 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
|
13 |
|
14 (* there cannot be a clause for lists, as *) |
|
15 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
|
16 ML {* |
|
17 val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4"; |
|
18 val {descr, sorts, ...} = dtinfo; |
|
19 *} |
|
20 setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *} |
|
21 lemmas perm = permute_rtrm4_permute_rtrm4_list.simps(1-3) |
|
22 lemma perm_fix: |
|
23 fixes ts::"rtrm4 list" |
|
24 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
|
25 by (induct ts) simp_all |
|
26 lemmas perm_fixed = perm[simplified perm_fix] |
|
27 |
|
28 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *} |
|
29 |
|
30 local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *} |
|
31 lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*) |
|
32 |
|
33 lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" |
|
34 by (rule ext) (induct_tac x, simp_all) |
|
35 lemmas fv_fixed = fv[simplified fv_fix] |
|
36 |
|
37 (* TODO: check remove 2 *) |
|
38 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms perm_fixed fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} |
|
39 thm eqvts(1-2) |
|
40 |
|
41 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *} |
|
42 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
|
43 lemmas alpha_inj = alpha4_inj(1-3) |
|
44 |
|
45 lemma alpha_fix: "alpha_rtrm4_list = list_all2 alpha_rtrm4" |
|
46 apply (rule ext)+ |
|
47 apply (induct_tac x xa rule: list_induct2') |
|
48 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
|
49 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
|
50 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
|
51 apply rule |
|
52 apply (erule alpha_rtrm4_list.cases) |
|
53 apply simp_all |
|
54 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
|
55 apply simp_all |
|
56 done |
|
57 |
|
58 lemmas alpha_inj_fixed = alpha_inj[simplified alpha_fix (*fv_fix*)] |
|
59 |
|
60 notation |
|
61 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) |
|
62 and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
|
63 |
|
64 declare perm_fixed[eqvt] |
|
65 equivariance alpha_rtrm4 |
|
66 lemmas alpha4_eqvt = eqvts(1-2) |
|
67 lemmas alpha4_eqvt_fixed = alpha4_eqvt(2)[simplified alpha_fix (*fv_fix*)] |
|
68 |
|
69 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), |
|
70 build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *} |
|
71 thm alpha4_reflp |
|
72 |
|
73 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
|
74 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
|
75 lemmas alpha4_equivp_fixed = alpha4_equivp[simplified alpha_fix fv_fix] |
|
76 |
|
77 quotient_type |
|
78 trm4 = rtrm4 / alpha_rtrm4 |
|
79 by (simp_all add: alpha4_equivp) |
|
80 |
|
81 local_setup {* |
|
82 (fn ctxt => ctxt |
|
83 |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) |
|
84 |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4})) |
|
85 |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})) |
|
86 |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4}))) |
|
87 *} |
|
88 print_theorems |
|
89 |
|
90 |
|
91 lemma fv_rtrm4_rsp: |
|
92 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
|
93 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
|
94 apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) |
|
95 apply (simp_all add: alpha_gen) |
|
96 done |
|
97 |
|
98 local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}] |
|
99 (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *} |
|
100 print_theorems |
|
101 |
|
102 local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}] |
|
103 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
|
104 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
|
105 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
|
106 |
|
107 lemma [quot_respect]: |
|
108 "(alpha_rtrm4 ===> list_all2 alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
|
109 by (simp add: alpha_inj_fixed) |
|
110 |
|
111 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
|
112 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
|
113 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
|
114 |
|
115 setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *} |
|
116 print_theorems |
|
117 |
|
118 (* Instead of permute for trm4_list we may need the following 2 lemmas: *) |
|
119 lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute" |
|
120 apply (simp add: expand_fun_eq) |
|
121 apply clarify |
|
122 apply (rename_tac "pi" x) |
|
123 apply (induct_tac x) |
|
124 apply simp |
|
125 apply simp |
|
126 apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified]) |
|
127 done |
|
128 |
|
129 lemma [quot_respect]: "(op = ===> list_all2 alpha_rtrm4 ===> list_all2 alpha_rtrm4) permute permute" |
|
130 apply simp |
|
131 apply (rule allI)+ |
|
132 apply (induct_tac xa y rule: list_induct2') |
|
133 apply simp_all |
|
134 apply clarify |
|
135 apply (erule alpha4_eqvt) |
|
136 done |
|
137 |
|
138 ML {* |
|
139 map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed} |
|
140 *} |
|
141 |
|
142 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
|
143 |
|
144 ML {* |
|
145 map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fv_fix] fv_rtrm4_list.simps[simplified fv_fix]} |
|
146 *} |
|
147 |
|
148 ML {* |
|
149 val liftd = |
|
150 map (Local_Defs.unfold @{context} @{thms id_simps}) ( |
|
151 map (Local_Defs.fold @{context} @{thms alphas}) ( |
|
152 map (lift_thm [@{typ trm4}] @{context}) @{thms alpha_inj_fixed[unfolded alphas]} |
|
153 ) |
|
154 ) |
|
155 *} |
|
156 |
|
157 ML {* |
|
158 map (lift_thm [@{typ trm4}] @{context}) |
|
159 (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})])) |
|
160 *} |
|
161 |
|
162 thm eqvts(6-7) |
|
163 ML {* |
|
164 map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(6-7)[simplified fv_fix]} |
|
165 *} |
|
166 |
|
167 end |
|