112 |
112 |
113 lemma intrel_refl: "intrel a a" |
113 lemma intrel_refl: "intrel a a" |
114 sorry |
114 sorry |
115 |
115 |
116 lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
116 lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
117 sorry |
117 by (simp) |
|
118 |
|
119 ML {* val consts = [@{const_name "my_plus"}] *} |
|
120 ML {* val rty = @{typ "nat \<times> nat"} *} |
|
121 ML {* val qty = @{typ "my_int"} *} |
|
122 ML {* val rel = @{term "intrel"} *} |
|
123 ML {* val rel_eqv = @{thm equiv_intrel} *} |
|
124 ML {* val rel_refl = @{thm intrel_refl} *} |
|
125 ML {* val quot = @{thm QUOTIENT_my_int} *} |
|
126 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
|
127 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
118 |
128 |
119 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
129 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
120 ML {* val t_r = regularize t_a @{typ "nat \<times> nat"} @{term "intrel"} @{thm equiv_intrel} @{context} *} |
130 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
121 ML {* val consts = [@{const_name "my_plus"}] *} |
131 |
122 |
|
123 ML {* |
|
124 val rt = build_repabs_term @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"} |
|
125 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
|
126 *} |
|
127 ML {* |
|
128 fun r_mk_comb_tac_myint ctxt = |
|
129 r_mk_comb_tac ctxt @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2} |
|
130 (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
|
131 *} |
|
132 ML {* val (g, thm, othm) = |
132 ML {* val (g, thm, othm) = |
133 Toplevel.program (fn () => |
133 Toplevel.program (fn () => |
134 repabs_eq @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"} |
134 repabs_eq @{context} t_r consts rty qty |
135 @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2} |
135 quot rel_refl trans2 |
136 (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
136 rsp_thms |
137 ) |
137 ) |
138 *} |
138 *} |
139 ML {* |
139 ML {* |
140 val t_t2 = |
140 val t_t2 = |
141 Toplevel.program (fn () => |
141 Toplevel.program (fn () => |
151 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
151 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
152 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
152 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
153 done |
153 done |
154 |
154 |
155 ML {* |
155 ML {* |
|
156 fun make_simp_lam_prs_thm lthy quot_thm typ = |
|
157 let |
|
158 val (_, [lty, rty]) = dest_Type typ; |
|
159 val thy = ProofContext.theory_of lthy; |
|
160 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
161 val inst = [SOME lcty, NONE, SOME rcty]; |
|
162 val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; |
|
163 val tac = |
|
164 (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW |
|
165 (quotient_tac quot_thm); |
|
166 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
|
167 val ts = @{thm HOL.sym} OF [t] |
|
168 in |
|
169 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_def}] ts |
|
170 end |
|
171 *} |
|
172 |
|
173 |
|
174 |
|
175 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
|
176 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
177 thm HOL.sym[OF lambda_prs_mn_b,simplified] |
|
178 |
|
179 ML {* |
156 fun simp_lam_prs lthy thm = |
180 fun simp_lam_prs lthy thm = |
157 simp_lam_prs lthy (eqsubst_thm lthy |
181 simp_lam_prs lthy (eqsubst_thm lthy |
158 @{thms HOL.sym[OF lambda_prs_mn_b,simplified]} |
182 @{thms HOL.sym[OF lambda_prs_mn_b,simplified]} |
159 thm) |
183 thm) |
160 handle _ => thm |
184 handle _ => thm |
161 *} |
185 *} |
162 ML {* t_t2 *} |
186 ML {* t_t2 *} |
163 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
187 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
164 ML {* findabs @{typ "nat \<times> nat"} (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
188 ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
165 |
189 |
166 ML {* |
190 ML {* |
167 fun simp_allex_prs lthy thm = |
191 fun simp_allex_prs lthy thm = |
168 let |
192 let |
169 val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]}; |
193 val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]}; |