equal
deleted
inserted
replaced
1190 thm REP_ABS_RSP |
1190 thm REP_ABS_RSP |
1191 lemmas REP_ABS_RSP_I = REP_ABS_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1191 lemmas REP_ABS_RSP_I = REP_ABS_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1192 |
1192 |
1193 prove trm |
1193 prove trm |
1194 apply (atomize(full)) |
1194 apply (atomize(full)) |
|
1195 apply (simp only: id_def[symmetric]) |
1195 |
1196 |
1196 ML_prf {* |
1197 ML_prf {* |
1197 val gc = Subgoal.focus @{context} 1 (Isar.goal ()) |
1198 val gc = Subgoal.focus @{context} 1 (Isar.goal ()) |
1198 |> fst |
1199 |> fst |
1199 |> #concl |
1200 |> #concl |
1213 |> #concl |
1214 |> #concl |
1214 val tc = cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }) |
1215 val tc = cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }) |
1215 val (_, tc') = Thm.dest_comb tc |
1216 val (_, tc') = Thm.dest_comb tc |
1216 val (_, gc') = Thm.dest_comb gc |
1217 val (_, gc') = Thm.dest_comb gc |
1217 *} |
1218 *} |
|
1219 ML_prf {* |
|
1220 fun dest_cbinop t = |
|
1221 let |
|
1222 val (t2, rhs) = Thm.dest_comb t; |
|
1223 val (bop, lhs) = Thm.dest_comb t2; |
|
1224 in |
|
1225 (bop, (lhs, rhs)) |
|
1226 end |
|
1227 *} |
|
1228 |
|
1229 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1230 ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *} |
|
1231 ML_prf {* val mr = Thm.match (r1, r2) *} |
|
1232 |
1218 |
1233 |
1219 ML_prf {* val m = Thm.match (tc', gc') *} |
1234 ML_prf {* val m = Thm.match (tc', gc') *} |
1220 ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *} |
1235 ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *} |
1221 apply (tactic {* rtac t2 1 *}) |
1236 apply (tactic {* rtac t2 1 *}) |
1222 |
1237 |