141 ML {* val consts = lookup_quot_consts defs *} |
141 ML {* val consts = lookup_quot_consts defs *} |
142 |
142 |
143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
144 |
144 |
145 |
145 |
146 ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
146 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
147 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
147 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
148 |
148 |
149 |
149 |
150 lemma "PLUS a b = PLUS b a" |
150 lemma "PLUS a b = PLUS b a" |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
152 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
152 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
153 prefer 2 |
153 prefer 2 |
154 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
154 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
155 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
155 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
156 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
156 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
157 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
158 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
158 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
160 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
161 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
162 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
163 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
164 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
165 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
166 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
167 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
168 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
169 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
170 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
170 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
171 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
171 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
172 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
172 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
173 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
173 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
174 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
174 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
175 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
175 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
176 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
176 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
177 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
177 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
178 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
178 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
179 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
179 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
180 done |
180 done |
181 |
181 |
182 lemma plus_assoc_pre: |
182 lemma plus_assoc_pre: |
183 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
183 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
184 apply (cases i) |
184 apply (cases i) |
188 done |
188 done |
189 |
189 |
190 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
190 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
192 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
192 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
193 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
193 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
194 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
194 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
195 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
195 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
196 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
196 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
197 done |
197 done |
198 |
198 |
205 |
205 |
206 lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl" |
206 lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl" |
207 sorry |
207 sorry |
208 |
208 |
209 lemma "foldl PLUS x [] = x" |
209 lemma "foldl PLUS x [] = x" |
210 apply (tactic {* lift_tac_intex @{context} @{thm ho_tst} 1 *}) |
210 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
211 apply (simp_all only: map_prs foldl_prs) |
211 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
|
212 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
213 apply(rule foldl_prs) |
|
214 apply(simp add: map_prs) |
|
215 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
216 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *} |
212 sorry |
217 sorry |
213 |
218 |
214 (* |
219 (* |
215 FIXME: All below is your construction code; mostly commented out as it |
220 FIXME: All below is your construction code; mostly commented out as it |
216 does not work. |
221 does not work. |
217 *) |
222 *) |
218 |
223 |
219 ML {* |
|
220 regularize_trm @{context} |
|
221 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
|
222 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
|
223 |> Syntax.string_of_term @{context} |
|
224 |> writeln |
|
225 *} |
|
226 |
|
227 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
224 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
228 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
225 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
229 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
226 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
230 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
227 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
231 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
228 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
232 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
229 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
233 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
230 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
234 done |
231 done |
235 |
232 |