138 ML {* val defs = @{thms PLUS_def} *} |
138 ML {* val defs = @{thms PLUS_def} *} |
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
141 ML {* val consts = lookup_quot_consts defs *} |
141 ML {* val consts = lookup_quot_consts defs *} |
142 |
142 |
143 ML {* |
143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
144 fun lift_tac_fset lthy t = |
144 |
145 lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs |
145 |
146 *} |
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 *} |
|
148 |
|
149 |
|
150 lemma cheat: "P" sorry |
147 |
151 |
148 lemma "PLUS a b = PLUS b a" |
152 lemma "PLUS a b = PLUS b a" |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
153 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
|
154 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
|
155 prefer 2 |
|
156 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) *} |
|
158 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
|
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
170 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
171 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
172 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
173 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
174 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
175 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
176 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
177 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
178 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
179 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
180 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
|
181 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
|
182 done |
150 |
183 |
151 lemma plus_assoc_pre: |
184 lemma plus_assoc_pre: |
152 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
185 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
153 apply (cases i) |
186 apply (cases i) |
154 apply (cases j) |
187 apply (cases j) |
155 apply (cases k) |
188 apply (cases k) |
156 apply (simp) |
189 apply (simp) |
157 done |
190 done |
158 |
191 |
159 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
192 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
160 by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *}) |
193 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
161 |
194 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
|
195 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
|
196 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) *} |
|
198 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
|
199 done |
162 |
200 |
163 lemma ho_tst: "foldl my_plus x [] = x" |
201 lemma ho_tst: "foldl my_plus x [] = x" |
164 apply simp |
202 apply simp |
165 done |
203 done |
166 |
204 |