108 apply(cases a) |
108 apply(cases a) |
109 apply(cases b) |
109 apply(cases b) |
110 apply(auto) |
110 apply(auto) |
111 done |
111 done |
112 |
112 |
113 lemma equiv_intrel: "EQUIV intrel" |
|
114 sorry |
|
115 |
|
116 lemma intrel_refl: "intrel a a" |
|
117 sorry |
|
118 |
|
119 lemma ho_plus_rsp: |
113 lemma ho_plus_rsp: |
120 "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
114 "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
121 by (simp) |
115 by (simp) |
122 |
116 |
123 ML {* val consts = [@{const_name "my_plus"}] *} |
117 ML {* val consts = [@{const_name "my_plus"}] *} |
124 ML {* val rty = @{typ "nat \<times> nat"} *} |
118 ML {* val rty = @{typ "nat \<times> nat"} *} |
125 ML {* val qty = @{typ "my_int"} *} |
119 ML {* val qty = @{typ "my_int"} *} |
126 ML {* val rel = @{term "intrel"} *} |
120 ML {* val rel = @{term "intrel"} *} |
127 ML {* val rel_eqv = @{thm equiv_intrel} *} |
121 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
128 ML {* val rel_refl = @{thm intrel_refl} *} |
122 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
129 ML {* val quot = @{thm QUOTIENT_my_int} *} |
123 ML {* val quot = @{thm QUOTIENT_my_int} *} |
130 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
124 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
131 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
125 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
132 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} |
126 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} |
133 ML {* val t_defs = @{thms PLUS_def} *} |
127 ML {* val t_defs = @{thms PLUS_def} *} |
142 lemma plus_assoc_pre: |
136 lemma plus_assoc_pre: |
143 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
137 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
144 apply (cases i) |
138 apply (cases i) |
145 apply (cases j) |
139 apply (cases j) |
146 apply (cases k) |
140 apply (cases k) |
147 apply (simp add: intrel_refl) |
141 apply (simp) |
148 done |
142 done |
149 |
143 |
150 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
144 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
151 |
145 |
152 |
146 |
153 text {* Below is the construction site code used if things do now work *} |
147 |
|
148 |
|
149 |
|
150 |
|
151 |
|
152 |
|
153 text {* Below is the construction site code used if things do not work *} |
|
154 |
|
155 |
|
156 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
|
157 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
158 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
|
159 |
154 |
160 |
155 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
161 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
156 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
162 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
157 |
163 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
158 ML {* val t_t = |
|
159 Toplevel.program (fn () => |
|
160 repabs @{context} t_r consts rty qty |
|
161 quot rel_refl trans2 |
|
162 rsp_thms |
|
163 ) |
|
164 *} |
|
165 |
|
166 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
|
167 |
|
168 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
169 ML {* t_t *} |
|
170 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
164 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
171 |
|
172 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
165 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
173 |
|
174 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
|
175 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} |
166 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} |
176 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
167 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
177 ML {* ObjectLogic.rulify t_r *} |
168 ML {* ObjectLogic.rulify t_r *} |
178 |
169 |
179 |
170 |