1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Term4
|
2061
|
2 |
imports "../NewAlpha" "../Abs" "../Perm" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
section {*** lam with indirect list recursion ***}
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
datatype rtrm4 =
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
rVr4 "name"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
| rAp4 "rtrm4" "rtrm4 list"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
(* there cannot be a clause for lists, as *)
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
(* permutations are already defined in Nominal (also functions, options, and so on) *)
|
2060
|
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) *}
|
2063
|
21 |
lemmas perm = permute_rtrm4_permute_rtrm4_list.simps(1-3)
|
|
22 |
lemma perm_fix:
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
fixes ts::"rtrm4 list"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
shows "permute_rtrm4_list p ts = p \<bullet> ts"
|
2063
|
25 |
by (induct ts) simp_all
|
|
26 |
lemmas perm_fixed = perm[simplified perm_fix]
|
1862
|
27 |
|
2061
|
28 |
ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
|
2149
|
30 |
local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *}
|
2063
|
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)
|
2061
|
40 |
|
|
41 |
local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *}
|
2063
|
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)
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
|
2326
|
45 |
lemma alpha_fix: "alpha_rtrm4_list = list_all2 alpha_rtrm4"
|
2063
|
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
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
57 |
|
2063
|
58 |
lemmas alpha_inj_fixed = alpha_inj[simplified alpha_fix (*fv_fix*)]
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
59 |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
notation
|
2063
|
61 |
alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
|
|
62 |
and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
|
2121
|
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*)]
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
68 |
|
1854
|
69 |
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
|
1906
|
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)) *}
|
1854
|
71 |
thm alpha4_reflp
|
|
72 |
|
1906
|
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)) *}
|
2063
|
75 |
lemmas alpha4_equivp_fixed = alpha4_equivp[simplified alpha_fix fv_fix]
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
76 |
|
2063
|
77 |
quotient_type
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
78 |
trm4 = rtrm4 / alpha_rtrm4
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
79 |
by (simp_all add: alpha4_equivp)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
80 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
81 |
local_setup {*
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
82 |
(fn ctxt => ctxt
|
1855
|
83 |
|> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))
|
1856
|
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})))
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
87 |
*}
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
print_theorems
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
|
1856
|
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]:
|
2326
|
108 |
"(alpha_rtrm4 ===> list_all2 alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
|
2063
|
109 |
by (simp add: alpha_inj_fixed)
|
1856
|
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) *}
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
114 |
|
1906
|
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} *}
|
1862
|
116 |
print_theorems
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
117 |
|
1906
|
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
|
1856
|
128 |
|
2326
|
129 |
lemma [quot_respect]: "(op = ===> list_all2 alpha_rtrm4 ===> list_all2 alpha_rtrm4) permute permute"
|
1906
|
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
|
1856
|
137 |
|
1906
|
138 |
ML {*
|
|
139 |
map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed}
|
|
140 |
*}
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
141 |
|
1856
|
142 |
ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
|
1906
|
143 |
|
|
144 |
ML {*
|
2063
|
145 |
map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fv_fix] fv_rtrm4_list.simps[simplified fv_fix]}
|
1906
|
146 |
*}
|
1856
|
147 |
|
1906
|
148 |
ML {*
|
|
149 |
val liftd =
|
|
150 |
map (Local_Defs.unfold @{context} @{thms id_simps}) (
|
|
151 |
map (Local_Defs.fold @{context} @{thms alphas}) (
|
2063
|
152 |
map (lift_thm [@{typ trm4}] @{context}) @{thms alpha_inj_fixed[unfolded alphas]}
|
1906
|
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 |
|
2121
|
162 |
thm eqvts(6-7)
|
1906
|
163 |
ML {*
|
2121
|
164 |
map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(6-7)[simplified fv_fix]}
|
1906
|
165 |
*}
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
end
|