60 fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t))) |
60 fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t))) |
61 | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) |
61 | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) |
62 fun tryext x = (x RS ext2 handle THM _ => x) |
62 fun tryext x = (x RS ext2 handle THM _ => x) |
63 val cong = (Goal.prove ctxt'' [] (map mk_def env) |
63 val cong = (Goal.prove ctxt'' [] (map mk_def env) |
64 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) |
64 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) |
65 (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x)) |
65 (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x)) |
66 THEN rtac th' 1)) RS sym |
66 THEN rtac th' 1)) RS sym |
67 |
67 |
68 val (cong' :: vars') = |
68 val (cong' :: vars') = |
69 Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs) |
69 Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs) |
70 val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars' |
70 val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars' |