56 val thy = Proof_Context.theory_of ctxt; |
56 val thy = Proof_Context.theory_of ctxt; |
57 val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt); |
57 val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt); |
58 val meta = Local_Defs.meta_rewrite_rule ctxt; |
58 val meta = Local_Defs.meta_rewrite_rule ctxt; |
59 val ths' = map meta ths; |
59 val ths' = map meta ths; |
60 val unfolds' = map meta unfolds and refolds' = map meta refolds; |
60 val unfolds' = map meta unfolds and refolds' = map meta refolds; |
61 val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t)) |
61 val (_$_$t') = concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (cterm_of thy t)) |
62 val u = unstar_term consts t' |
62 val u = unstar_term consts t' |
63 val tac = |
63 val tac = |
64 rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN |
64 rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN |
65 ALLGOALS Object_Logic.full_atomize_tac THEN |
65 ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN |
66 match_tac [transitive_thm] 1 THEN |
66 match_tac [transitive_thm] 1 THEN |
67 resolve_tac [@{thm transfer_start}] 1 THEN |
67 resolve_tac [@{thm transfer_start}] 1 THEN |
68 REPEAT_ALL_NEW (resolve_tac intros) 1 THEN |
68 REPEAT_ALL_NEW (resolve_tac intros) 1 THEN |
69 match_tac [reflexive_thm] 1 |
69 match_tac [reflexive_thm] 1 |
70 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end |
70 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end |
74 (fn th => |
74 (fn th => |
75 let |
75 let |
76 val tr = transfer_thm_of ctxt ths t |
76 val tr = transfer_thm_of ctxt ths t |
77 val (_$l$r) = concl_of tr; |
77 val (_$l$r) = concl_of tr; |
78 val trs = if l aconv r then [] else [tr]; |
78 val trs = if l aconv r then [] else [tr]; |
79 in rewrite_goals_tac trs th end)) |
79 in rewrite_goals_tac ctxt trs th end)) |
80 |
80 |
81 local |
81 local |
82 |
82 |
83 fun map_intros f = TransferData.map |
83 fun map_intros f = TransferData.map |
84 (fn {intros,unfolds,refolds,consts} => |
84 (fn {intros,unfolds,refolds,consts} => |