126 apply(cases a) |
126 apply(cases a) |
127 apply(cases b) |
127 apply(cases b) |
128 apply(auto) |
128 apply(auto) |
129 done |
129 done |
130 |
130 |
131 lemma ho_plus_rsp: |
131 lemma ho_plus_rsp[quot_rsp]: |
132 "(intrel ===> intrel ===> intrel) my_plus my_plus" |
132 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
133 by (simp) |
133 by (simp) |
134 |
134 |
135 ML {* val qty = @{typ "my_int"} *} |
135 ML {* val qty = @{typ "my_int"} *} |
136 ML {* val ty_name = "my_int" *} |
136 ML {* val ty_name = "my_int" *} |
137 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
137 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
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 {* 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] defs *} |
144 |
144 |
145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
147 |
147 |
148 |
148 |
149 lemma "PLUS a b = PLUS b a" |
149 lemma "PLUS a b = PLUS b a" |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
197 |
197 |
198 lemma ho_tst: "foldl my_plus x [] = x" |
198 lemma ho_tst: "foldl my_plus x [] = x" |
199 apply simp |
199 apply simp |
200 done |
200 done |
201 |
201 |
202 lemma map_prs: "map REP_my_int (map ABS_my_int x) = x" |
202 (* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *) |
|
203 lemma map_prs: |
|
204 "map REP_my_int (map ABS_my_int x) = x" |
203 sorry |
205 sorry |
204 |
206 |
205 lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl" |
207 lemma foldl_prs[quot_rsp]: |
|
208 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl" |
206 sorry |
209 sorry |
207 |
210 |
208 lemma "foldl PLUS x [] = x" |
211 lemma "foldl PLUS x [] = x" |
209 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
212 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
210 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
213 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
211 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
214 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
212 apply(rule foldl_prs) |
|
213 apply(simp add: map_prs) |
215 apply(simp add: map_prs) |
214 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
216 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
215 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *} |
217 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *} |
216 sorry |
218 sorry |
217 |
219 |