15 thm rtrm4.recs |
15 thm rtrm4.recs |
16 |
16 |
17 (* there cannot be a clause for lists, as *) |
17 (* there cannot be a clause for lists, as *) |
18 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
18 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
19 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} |
19 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} |
|
20 print_theorems |
20 |
21 |
21 (* "repairing" of the permute function *) |
22 (* "repairing" of the permute function *) |
22 lemma repaired: |
23 lemma repaired: |
23 fixes ts::"rtrm4 list" |
24 fixes ts::"rtrm4 list" |
24 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
25 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
25 apply(induct ts) |
26 apply(induct ts) |
26 apply(simp_all) |
27 apply(simp_all) |
27 done |
28 done |
28 |
29 |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
30 thm permute_rtrm4_permute_rtrm4_list.simps |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
31 lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
|
32 |
31 |
33 |
32 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4") |
34 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4") |
33 [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *} |
35 [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *} |
34 print_theorems |
36 print_theorems |
35 |
37 |
104 |
106 |
105 local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}] |
107 local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}] |
106 (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *} |
108 (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *} |
107 print_theorems |
109 print_theorems |
108 |
110 |
109 ML constr_rsp_tac |
|
110 |
|
111 local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}] |
111 local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}] |
112 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
112 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
113 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
113 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) *} |
114 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
115 |
115 |
121 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
121 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
122 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
122 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
123 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
123 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
124 print_theorems |
124 print_theorems |
125 |
125 |
126 lemma list_rel_rsp: |
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} *} |
127 "\<lbrakk>\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b); list_rel R x y; list_rel R a b\<rbrakk> |
127 print_theorems |
128 \<Longrightarrow> list_rel S x a = list_rel T y b" |
|
129 sorry |
|
130 |
128 |
131 lemma[quot_respect]: |
|
132 "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel" |
|
133 by (simp add: list_rel_rsp) |
|
134 |
129 |
135 lemma[quot_preserve]: |
|
136 assumes a: "Quotient R abs1 rep1" |
|
137 shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel" |
|
138 apply (simp add: expand_fun_eq) |
|
139 apply clarify |
|
140 apply (induct_tac xa xb rule: list_induct2') |
|
141 apply (simp_all add: Quotient_abs_rep[OF a]) |
|
142 done |
|
143 |
|
144 lemma[quot_preserve]: |
|
145 assumes a: "Quotient R abs1 rep1" |
|
146 shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" |
|
147 by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a]) |
|
148 |
130 |
149 lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) = |
131 lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) = |
150 (trm4 = trm4a \<and> list_rel (op =) list lista)" |
132 (trm4 = trm4a \<and> list_rel (op =) list lista)" |
151 by (lifting alpha4_inj(2)) |
133 by (lifting alpha4_inj(2)) |
152 |
134 |
153 thm bla[simplified list_rel_eq] |
135 thm bla[simplified list_rel_eq] |
154 |
|
155 lemma " (Lm4 name rtrm4 = Lm4 namea rtrm4a) = |
|
156 (\<exists>pi\<Colon>perm. |
|
157 fv_trm4 rtrm4 - {atom name} = fv_trm4 rtrm4a - {atom namea} \<and> |
|
158 (fv_trm4 rtrm4 - {atom name}) \<sharp>* pi \<and> |
|
159 pi \<bullet> rtrm4 = rtrm4a \<and> pi \<bullet> {atom name} = {atom namea})" |
|
160 |
136 |
161 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *} |
137 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *} |
162 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *} |
138 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *} |
163 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *} |
139 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *} |
164 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
140 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |