117 ML {* val quot = @{thm QUOTIENT_lam} *} |
117 ML {* val quot = @{thm QUOTIENT_lam} *} |
118 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
118 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
119 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
119 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
120 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
120 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
121 |
121 |
122 thm a3 |
122 ML {* |
123 ML {* val t_a = atomize_thm @{thm a3} *} |
123 fun lift_thm_lam lthy t = |
124 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
124 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
125 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
125 *} |
126 ML {* val abs = findabs rty (prop_of t_a) *} |
126 ML {* lift_thm_lam @{context} @{thm a3} *} |
127 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
128 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
|
129 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
|
130 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
|
131 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
|
132 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
133 ML {* ObjectLogic.rulify t_b *} |
|
134 |
|
135 thm fresh_def |
|
136 thm supp_def |
|
137 |
127 |
138 local_setup {* |
128 local_setup {* |
139 old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
129 old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
140 *} |
130 *} |
141 |
131 |
142 ML {* val consts = @{const_name perm} :: consts *} |
132 ML {* val consts = @{const_name perm} :: consts *} |
143 ML {* val defs = @{thms lperm_def} @ defs *} |
133 ML {* val defs = @{thms lperm_def} @ defs *} |
144 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
134 ML {* |
145 ML {* val t_a = atomize_thm @{thm a3} *} |
135 fun lift_thm_lam lthy t = |
146 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
136 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
147 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
137 *} |
148 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
138 ML {* val t_b = lift_thm_lam @{context} @{thm a3} *} |
149 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
139 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms lperm_def}))] *} |
150 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
|
151 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
|
152 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
153 ML {* val rr = (add_lower_defs @{context} @{thms lperm_def}) *} |
|
154 ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *} |
|
155 lemma prod_fun_id: "prod_fun id id = id" |
140 lemma prod_fun_id: "prod_fun id id = id" |
156 apply (simp add: prod_fun_def) |
141 apply (simp add: prod_fun_def) |
157 done |
142 done |
158 lemma map_id: "map id x = x" |
143 lemma map_id: "map id x = x" |
159 apply (induct x) |
144 apply (induct x) |
160 apply (simp_all add: map.simps) |
145 apply (simp_all add: map.simps) |
161 done |
146 done |
162 |
147 |
163 ML {* val rrrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rrr *} |
148 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
164 ML {* val t_b' = eqsubst_thm @{context} [rrrr] t_b *} |
149 ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *} |
165 ML {* ObjectLogic.rulify t_b' *} |
150 ML {* ObjectLogic.rulify t_b' *} |
166 |
151 |
167 |
152 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
168 |
153 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *) |
169 local_setup {* |
|
170 make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
|
171 *} |
|
172 @{const_name fresh} :: |
|
173 lfresh_def |
|
174 ML {* |
|
175 fun lift_thm_lam lthy t = |
|
176 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
177 *} |
|
178 |
|
179 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
|
180 |
|