--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 02 13:55:43 2015 +0200
@@ -171,11 +171,10 @@
(* INFERENCE RULE: RESOLVE *)
(*Increment the indexes of only the type variables*)
-fun incr_type_indexes inc th =
+fun incr_type_indexes ctxt inc th =
let
val tvs = Term.add_tvars (Thm.full_prop_of th) []
- val thy = Thm.theory_of_thm th
- fun inc_tvar ((a, i), s) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
+ fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s))
in
Thm.instantiate (map inc_tvar tvs, []) th
end
@@ -185,7 +184,7 @@
Instantiations of those Vars could then fail. *)
fun resolve_inc_tyvars ctxt tha i thb =
let
- val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
fun res (tha, thb) =
(case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
(false, tha, Thm.nprems_of tha) i thb
@@ -393,16 +392,16 @@
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
-fun flexflex_first_order th =
+fun flexflex_first_order ctxt th =
(case Thm.tpairs_of th of
[] => th
| pairs =>
let
- val thy = Thm.theory_of_thm th
+ val thy = Proof_Context.theory_of ctxt
val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
- fun mkT (v, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (v, S), T)
- fun mk (v, (T, t)) = apply2 (Thm.global_cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+ fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T)
+ fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t)
val instsT = Vartab.fold (cons o mkT) tyenv []
val insts = Vartab.fold (cons o mk) tenv []
@@ -462,7 +461,7 @@
val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
- |> flexflex_first_order
+ |> flexflex_first_order ctxt
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg ctxt (fn () => "=============================================")
--- a/src/HOL/Tools/TFL/casesplit.ML Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Tue Jun 02 13:55:43 2015 +0200
@@ -32,28 +32,28 @@
(* for use when there are no prems to the subgoal *)
(* does a case split on the given variable *)
-fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
+fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
let
- val x = Free(vstr,ty)
+ val thy = Proof_Context.theory_of ctxt;
+
+ val x = Free(vstr,ty);
val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
- val ctermify = Thm.global_cterm_of sgn;
- val ctypify = Thm.global_ctyp_of sgn;
- val case_thm = case_thm_of_ty sgn ty;
+ val case_thm = case_thm_of_ty thy ty;
- val abs_ct = ctermify abst;
- val free_ct = ctermify x;
+ val abs_ct = Thm.cterm_of ctxt abst;
+ val free_ct = Thm.cterm_of ctxt x;
val (Pv, Dv, type_insts) =
case (Thm.concl_of case_thm) of
- (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
+ (_ $ (Pv $ (Dv as Var(D, Dty)))) =>
(Pv, Dv,
- Sign.typ_match sgn (Dty, ty) Vartab.empty)
+ Sign.typ_match thy (Dty, ty) Vartab.empty)
| _ => error "not a valid case thm";
- val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
+ val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T))
(Vartab.dest type_insts);
- val cPv = ctermify (Envir.subst_term_types type_insts Pv);
- val cDv = ctermify (Envir.subst_term_types type_insts Dv);
+ val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv);
+ val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv);
in
Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
@@ -117,7 +117,6 @@
fun splitto ctxt splitths genth =
let
val _ = not (null splitths) orelse error "splitto: no given splitths";
- val thy = Thm.theory_of_thm genth;
(* check if we are a member of splitths - FIXME: quicker and
more flexible with discrim net. *)
@@ -134,7 +133,7 @@
| SOME v =>
let
val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
- val split_thm = mk_casesplit_goal_thm thy v gt;
+ val split_thm = mk_casesplit_goal_thm ctxt v gt;
val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
in
expf (map recsplitf subthms)
--- a/src/HOL/Tools/TFL/post.ML Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/TFL/post.ML Tue Jun 02 13:55:43 2015 +0200
@@ -78,7 +78,7 @@
val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *)
val cntxt = union (op aconv) cntxtl cntxtr
in
- Rules.GEN_ALL
+ Rules.GEN_ALL ctxt
(Rules.DISCH_ALL
(rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
end
@@ -211,7 +211,8 @@
#1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
fun defer_i congs fid eqs thy =
- let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
+ let
+ val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
val dummy = writeln "Proving induction theorem ...";
val induction = Prim.mk_induction theory
--- a/src/HOL/Tools/TFL/rules.ML Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Jun 02 13:55:43 2015 +0200
@@ -21,22 +21,22 @@
val SPEC: cterm -> thm -> thm
val ISPEC: cterm -> thm -> thm
val ISPECL: cterm list -> thm -> thm
- val GEN: cterm -> thm -> thm
- val GENL: cterm list -> thm -> thm
+ val GEN: Proof.context -> cterm -> thm -> thm
+ val GENL: Proof.context -> cterm list -> thm -> thm
val LIST_CONJ: thm list -> thm
val SYM: thm -> thm
val DISCH_ALL: thm -> thm
val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
val SPEC_ALL: thm -> thm
- val GEN_ALL: thm -> thm
+ val GEN_ALL: Proof.context -> thm -> thm
val IMP_TRANS: thm -> thm -> thm
val PROVE_HYP: thm -> thm -> thm
val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
val EXISTS: cterm * cterm -> thm -> thm
val EXISTL: cterm list -> thm -> thm
- val IT_EXISTS: (cterm*cterm) list -> thm -> thm
+ val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
val EVEN_ORS: thm list -> thm list
val DISJ_CASESL: thm -> thm list -> thm
@@ -158,19 +158,19 @@
(*----------------------------------------------------------------------------
* Disjunction
*---------------------------------------------------------------------------*)
-local val thy = Thm.theory_of_thm disjI1
- val prop = Thm.prop_of disjI1
- val [P,Q] = Misc_Legacy.term_vars prop
- val disj1 = Thm.forall_intr (Thm.global_cterm_of thy Q) disjI1
+local
+ val prop = Thm.prop_of disjI1
+ val [P,Q] = Misc_Legacy.term_vars prop
+ val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
in
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
end;
-local val thy = Thm.theory_of_thm disjI2
- val prop = Thm.prop_of disjI2
- val [P,Q] = Misc_Legacy.term_vars prop
- val disj2 = Thm.forall_intr (Thm.global_cterm_of thy P) disjI2
+local
+ val prop = Thm.prop_of disjI2
+ val [P,Q] = Misc_Legacy.term_vars prop
+ val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
in
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
@@ -262,11 +262,10 @@
* Universals
*---------------------------------------------------------------------------*)
local (* this is fragile *)
- val thy = Thm.theory_of_thm spec
- val prop = Thm.prop_of spec
- val x = hd (tl (Misc_Legacy.term_vars prop))
- val cTV = Thm.global_ctyp_of thy (type_of x)
- val gspec = Thm.forall_intr (Thm.global_cterm_of thy x) spec
+ val prop = Thm.prop_of spec
+ val x = hd (tl (Misc_Legacy.term_vars prop))
+ val cTV = Thm.ctyp_of @{context} (type_of x)
+ val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
in
fun SPEC tm thm =
let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
@@ -279,41 +278,38 @@
val ISPECL = fold ISPEC;
(* Not optimized! Too complicated. *)
-local val thy = Thm.theory_of_thm allI
- val prop = Thm.prop_of allI
- val [P] = Misc_Legacy.add_term_vars (prop, [])
- fun cty_theta s = map (fn (i, (S, ty)) => (Thm.global_ctyp_of s (TVar (i, S)), Thm.global_ctyp_of s ty))
- fun ctm_theta s = map (fn (i, (_, tm2)) =>
- let val ctm2 = Thm.global_cterm_of s tm2
- in (Thm.global_cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
- end)
- fun certify s (ty_theta,tm_theta) =
- (cty_theta s (Vartab.dest ty_theta),
- ctm_theta s (Vartab.dest tm_theta))
+local
+ val prop = Thm.prop_of allI
+ val [P] = Misc_Legacy.add_term_vars (prop, [])
+ fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty))
+ fun ctm_theta ctxt =
+ map (fn (i, (_, tm2)) =>
+ let val ctm2 = Thm.cterm_of ctxt tm2
+ in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end)
+ fun certify ctxt (ty_theta,tm_theta) =
+ (cty_theta ctxt (Vartab.dest ty_theta),
+ ctm_theta ctxt (Vartab.dest tm_theta))
in
-fun GEN v th =
+fun GEN ctxt v th =
let val gth = Thm.forall_intr v th
- val thy = Thm.theory_of_thm gth
+ val thy = Proof_Context.theory_of ctxt
val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
- val allI2 = Drule.instantiate_normalize (certify thy theta) allI
+ val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
val thm = Thm.implies_elim allI2 gth
val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
val prop' = tp $ (A $ Abs(x,ty,M))
- in ALPHA thm (Thm.global_cterm_of thy prop')
- end
+ in ALPHA thm (Thm.cterm_of ctxt prop') end
end;
-val GENL = fold_rev GEN;
+fun GENL ctxt = fold_rev (GEN ctxt);
-fun GEN_ALL thm =
- let val thy = Thm.theory_of_thm thm
- val prop = Thm.prop_of thm
- val tycheck = Thm.global_cterm_of thy
- val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
- in GENL vlist thm
- end;
+fun GEN_ALL ctxt thm =
+ let
+ val prop = Thm.prop_of thm
+ val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
+ in GENL ctxt vlist thm end;
fun MATCH_MP th1 th2 =
@@ -344,24 +340,19 @@
val t$u = Thm.term_of redex
val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
in
- GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
+ GEN ctxt fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
end;
-local val thy = Thm.theory_of_thm exI
- val prop = Thm.prop_of exI
- val [P,x] = Misc_Legacy.term_vars prop
+local
+ val prop = Thm.prop_of exI
+ val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
in
fun EXISTS (template,witness) thm =
- let val thy = Thm.theory_of_thm thm
- val prop = Thm.prop_of thm
- val P' = Thm.global_cterm_of thy P
- val x' = Thm.global_cterm_of thy x
- val abstr = #2 (Dcterm.dest_comb template)
- in
- thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
- handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
- end
+ let val abstr = #2 (Dcterm.dest_comb template) in
+ thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
+ handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
+ end
end;
(*----------------------------------------------------------------------------
@@ -386,16 +377,14 @@
*---------------------------------------------------------------------------*)
(* Could be improved, but needs "subst_free" for certified terms *)
-fun IT_EXISTS blist th =
- let val thy = Thm.theory_of_thm th
- val tych = Thm.global_cterm_of thy
- val blist' = map (apply2 Thm.term_of) blist
- fun ex v M = Thm.global_cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
-
+fun IT_EXISTS ctxt blist th =
+ let
+ val blist' = map (apply2 Thm.term_of) blist
+ fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
in
- fold_rev (fn (b as (r1,r2)) => fn thm =>
+ fold_rev (fn (b as (r1,r2)) => fn thm =>
EXISTS(ex r2 (subst_free [b]
- (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)
+ (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
thm)
blist' th
end;
@@ -509,13 +498,10 @@
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
- let val thy = Thm.theory_of_thm thm
- val tych = Thm.global_cterm_of thy
- val ants = Logic.strip_imp_prems (Thm.prop_of thm)
- val news = get (ants,1,[])
- in
- fold Thm.rename_params_rule news thm
- end;
+ let
+ val ants = Logic.strip_imp_prems (Thm.prop_of thm)
+ val news = get (ants,1,[])
+ in fold Thm.rename_params_rule news thm end;
(*---------------------------------------------------------------------------
@@ -737,10 +723,9 @@
handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
fun restrict_prover ctxt thm =
- let val dummy = say "restrict_prover:"
+ let val _ = say "restrict_prover:"
val cntxt = rev (Simplifier.prems_of ctxt)
- val dummy = print_thms ctxt "cntxt:" cntxt
- val thy = Thm.theory_of_thm thm
+ val _ = print_thms ctxt "cntxt:" cntxt
val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
@@ -762,14 +747,13 @@
val antl = case rcontext of [] => []
| _ => [USyntax.list_mk_conj(map cncl rcontext)]
val TC = genl(USyntax.list_mk_imp(antl, A))
- val dummy = print_cterm ctxt "func:" (Thm.global_cterm_of thy func)
- val dummy = print_cterm ctxt "TC:" (Thm.global_cterm_of thy (HOLogic.mk_Trueprop TC))
+ val dummy = print_cterm ctxt "func:" (Thm.cterm_of ctxt func)
+ val dummy = print_cterm ctxt "TC:" (Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC))
val dummy = tc_list := (TC :: !tc_list)
val nestedp = is_some (USyntax.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
- else let val cTC = Thm.global_cterm_of thy
- (HOLogic.mk_Trueprop TC)
+ else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
in case rcontext of
[] => SPEC_ALL(ASSUME cTC)
| _ => MP (SPEC_ALL (ASSUME cTC))
--- a/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 13:55:43 2015 +0200
@@ -535,30 +535,30 @@
val (c,args) = USyntax.strip_comb lhs
val (name,Ty) = dest_atom c
val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
- val ([def0], theory) =
+ val ([def0], thy') =
thy
|> Global_Theory.add_defs false
[Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
val def = Thm.unvarify_global def0;
+ val ctxt' = Syntax.init_pretty_global thy';
val dummy =
- if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
+ if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def)
else ()
(* val fconst = #lhs(USyntax.dest_eq(concl def)) *)
- val tych = Thry.typecheck theory
+ val tych = Thry.typecheck thy'
val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
(*lcp: a lot of object-logic inference to remove*)
val baz = Rules.DISCH_ALL
(fold_rev Rules.DISCH full_rqt_prop
(Rules.LIST_CONJ extractants))
- val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
- else ()
+ val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else ()
val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
val SV' = map tych SV;
val SVrefls = map Thm.reflexive SV'
val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
SVrefls def)
RS meta_eq_to_obj_eq
- val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0
+ val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN ctxt' (tych R1) baz)) def0
val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
theory Hilbert_Choice*)
@@ -566,7 +566,7 @@
handle ERROR msg => cat_error msg
"defer_recdef requires theory Main or at least Hilbert_Choice as parent"
val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
- in {theory = theory, R=R1, SV=SV,
+ in {theory = thy', R=R1, SV=SV,
rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def',
full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
patterns = pats}
@@ -633,7 +633,7 @@
fun fail s = raise TFL_ERR "mk_case" s
fun mk{rows=[],...} = fail"no rows"
| mk{path=[], rows = [([], (thm, bindings))]} =
- Rules.IT_EXISTS (map tych_binding bindings) thm
+ Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
| mk{path = u::rstp, rows as (p::_, _)::_} =
let val (pat_rectangle,rights) = ListPair.unzip rows
val col0 = map hd pat_rectangle
@@ -693,7 +693,7 @@
val th0 = Rules.ASSUME (tych a_eq_v)
val rows = map (fn x => ([x], (th0,[]))) pats
in
- Rules.GEN (tych a)
+ Rules.GEN ctxt (tych a)
(Rules.RIGHT_ASSOC ctxt
(Rules.CHOOSE ctxt (tych v, ex_th0)
(mk_case ty_info (vname::aname::names)
@@ -774,14 +774,14 @@
* TCs = TC_1[pat] ... TC_n[pat]
* thm = ih1 /\ ... /\ ih_n |- ih[pat]
*---------------------------------------------------------------------------*)
-fun prove_case f thy (tm,TCs_locals,thm) =
- let val tych = Thry.typecheck thy
+fun prove_case ctxt f (tm,TCs_locals,thm) =
+ let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
val antc = tych(#ant(USyntax.dest_imp tm))
val thm' = Rules.SPEC_ALL thm
fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
- Rules.GENL (map tych locals)
+ Rules.GENL ctxt (map tych locals)
(if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
else Rules.MP th2 TC)
@@ -845,7 +845,7 @@
val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
- val proved_cases = map (prove_case fconst thy) tasks
+ val proved_cases = map (prove_case ctxt fconst) tasks
val v =
Free (singleton
(Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
@@ -855,14 +855,14 @@
val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
(substs, proved_cases)
val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
- val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
+ val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
val dc = Rules.MP Sinduct dant
val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
- val dc' = fold_rev (Rules.GEN o tych) vars
+ val dc' = fold_rev (Rules.GEN ctxt o tych) vars
(Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
in
- Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
+ Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
end
handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
@@ -966,7 +966,7 @@
fun simplify_nested_tc tc =
let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
in
- Rules.GEN_ALL
+ Rules.GEN_ALL ctxt
(Rules.MATCH_MP Thms.eqT tc_eq
handle Utils.ERR _ =>
(Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
--- a/src/HOL/Tools/split_rule.ML Tue Jun 02 11:03:02 2015 +0200
+++ b/src/HOL/Tools/split_rule.ML Tue Jun 02 13:55:43 2015 +0200
@@ -53,9 +53,8 @@
(incr_boundvars 1 u) $ Bound 0))
| ap_split' _ _ u = u;
-fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
+fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) =
let
- val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
val (Us', U') = strip_type T;
val Us = take (length ts) Us';
val U = drop (length ts) Us' ---> U';
@@ -64,17 +63,19 @@
let
val Ts = HOLogic.flatten_tupleT T;
val ys = Name.variant_list xs (replicate (length Ts) a);
- in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
- (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
+ in
+ (xs @ ys,
+ apply2 (Thm.cterm_of ctxt)
+ (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
+ (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts)
end
| mk_tuple _ x = x;
val newt = ap_split' Us U (Var (v, T'));
- val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
val (vs', insts) = fold mk_tuple ts (vs, []);
in
- (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+ (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs')
end
- | complete_split_rule_var _ x = x;
+ | complete_split_rule_var _ _ x = x;
fun collect_vars (Abs (_, _, t)) = collect_vars t
| collect_vars t =
@@ -99,7 +100,7 @@
val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
val vars = collect_vars prop [];
in
- fst (fold_rev complete_split_rule_var vars (rl, xs))
+ fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs))
|> remove_internal_split ctxt
|> Drule.export_without_context
|> Rule_Cases.save rl