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 r_mk_comb_tac_intex lthy = r_mk_comb_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_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
148 |
148 |
149 |
149 |
150 lemma cheat: "P" sorry |
|
151 |
|
152 lemma "PLUS a b = PLUS b a" |
150 lemma "PLUS a b = PLUS b a" |
153 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
154 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
152 apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) |
155 prefer 2 |
153 prefer 2 |
156 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 ())))) *} |
157 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) *} |
158 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
156 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
157 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
158 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***) |
162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
170 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
171 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
172 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
170 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
173 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
171 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
174 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
172 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
175 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
173 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
176 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
174 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
177 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
175 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
178 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
176 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
179 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
177 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
180 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
178 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
181 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
179 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
182 done |
180 done |
183 |
181 |
184 lemma plus_assoc_pre: |
182 lemma plus_assoc_pre: |
185 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)" |
186 apply (cases i) |
184 apply (cases i) |
189 apply (simp) |
187 apply (simp) |
190 done |
188 done |
191 |
189 |
192 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)" |
193 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
194 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) |
195 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
193 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
196 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 ())))) *} |
197 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) *} |
198 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
196 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
199 done |
197 done |
226 |> writeln |
224 |> writeln |
227 *} |
225 *} |
228 |
226 |
229 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
227 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
230 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
228 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
231 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
229 apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) |
232 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
230 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
233 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
231 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
232 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
233 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
236 done |
234 done |