46 apply simp_all |
46 apply simp_all |
47 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
47 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
48 apply simp_all |
48 apply simp_all |
49 done |
49 done |
50 |
50 |
51 (* We need sth like: |
51 ML {* @{term "\<Union>a"} *} |
52 lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) |
52 |
|
53 lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" |
|
54 apply (rule ext) |
|
55 apply (induct_tac x) |
|
56 apply simp_all |
|
57 done |
53 |
58 |
54 notation |
59 notation |
55 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
60 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
56 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
61 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
57 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
62 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
58 |
63 |
59 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} |
64 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)) *} |
60 thm alpha4_inj |
65 thm alpha4_inj |
61 |
66 |
62 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (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)) *} |
67 lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3] |
63 thm alpha4_inj_no |
|
64 |
68 |
65 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} |
69 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} |
66 thm eqvts(1-2) |
70 thm eqvts(1-2) |
67 |
71 |
68 local_setup {* |
72 local_setup {* |
69 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), |
73 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), |
70 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt)) |
74 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt)) |
71 *} |
75 *} |
72 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
76 thm alpha4_eqvt |
|
77 lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3] |
73 |
78 |
74 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), |
79 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), |
75 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_no} ctxt) ctxt)) *} |
80 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)) *} |
76 thm alpha4_reflp |
81 thm alpha4_reflp |
77 ML build_equivps |
82 lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3] |
78 |
83 |
79 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
84 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
80 (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_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} |
85 (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)) *} |
81 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
86 lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3] |
82 |
87 |
83 quotient_type |
88 quotient_type |
84 trm4 = rtrm4 / alpha_rtrm4 |
89 trm4 = rtrm4 / alpha_rtrm4 |
85 (*and |
|
86 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
|
87 by (simp_all add: alpha4_equivp) |
90 by (simp_all add: alpha4_equivp) |
88 |
91 |
89 local_setup {* |
92 local_setup {* |
90 (fn ctxt => ctxt |
93 (fn ctxt => ctxt |
91 |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) |
94 |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) |
92 |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4})) |
95 |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4})) |
93 |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})) |
96 |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})) |
94 |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4}))) |
97 |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4}))) |
95 *} |
98 *} |
96 print_theorems |
99 print_theorems |
97 |
|
98 |
100 |
99 |
101 |
100 lemma fv_rtrm4_rsp: |
102 lemma fv_rtrm4_rsp: |
101 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
103 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
102 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
104 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
113 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
115 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
114 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
116 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
115 |
117 |
116 lemma [quot_respect]: |
118 lemma [quot_respect]: |
117 "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
119 "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
118 by (simp add: alpha4_inj) |
120 by (simp add: alpha4_inj_fixed) |
119 |
121 |
120 (* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *) |
|
121 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
122 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
122 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
123 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
123 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
124 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
|
125 |
|
126 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} *} |
124 print_theorems |
127 print_theorems |
125 |
128 |
126 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_append} *} |
129 (* Instead of permute for trm4_list we may need the following 2 lemmas: *) |
127 print_theorems |
130 lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute" |
|
131 apply (simp add: expand_fun_eq) |
|
132 apply clarify |
|
133 apply (rename_tac "pi" x) |
|
134 apply (induct_tac x) |
|
135 apply simp |
|
136 apply simp |
|
137 apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified]) |
|
138 done |
128 |
139 |
|
140 lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute" |
|
141 apply simp |
|
142 apply (rule allI)+ |
|
143 apply (induct_tac xa y rule: list_induct2') |
|
144 apply simp_all |
|
145 apply clarify |
|
146 apply (erule alpha4_eqvt) |
|
147 done |
129 |
148 |
|
149 ML {* |
|
150 map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed} |
|
151 *} |
130 |
152 |
131 lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) = |
153 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
132 (trm4 = trm4a \<and> list_rel (op =) list lista)" |
|
133 by (lifting alpha4_inj(2)) |
|
134 |
154 |
135 thm bla[simplified list_rel_eq] |
155 ML {* |
|
156 map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]} |
|
157 *} |
136 |
158 |
137 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *} |
159 ML {* |
138 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *} |
160 val liftd = |
139 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *} |
161 map (Local_Defs.unfold @{context} @{thms id_simps}) ( |
140 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
162 map (Local_Defs.fold @{context} @{thms alphas}) ( |
141 . |
163 map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]} |
|
164 ) |
|
165 ) |
|
166 *} |
142 |
167 |
143 (*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*) |
168 ML {* |
|
169 map (lift_thm [@{typ trm4}] @{context}) |
|
170 (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})])) |
|
171 *} |
|
172 |
|
173 ML {* |
|
174 map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]} |
|
175 *} |
144 |
176 |
145 end |
177 end |