# HG changeset patch # User wenzelm # Date 1425673230 -3600 # Node ID bb1e4a35d5064f118cf8074ab0fe69bf0f8a75f8 # Parent a6e977d8b0709413a23cd9761adf51642ce398d7 clarified context; diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Fri Mar 06 21:14:27 2015 +0100 +++ b/src/HOL/Tools/Function/fun.ML Fri Mar 06 21:20:30 2015 +0100 @@ -28,7 +28,6 @@ fun err str = error (cat_lines ["Malformed definition:", str ^ " not allowed in sequential mode.", Syntax.string_of_term ctxt geq]) - val thy = Proof_Context.theory_of ctxt fun check_constr_pattern (Bound _) = () | check_constr_pattern t = diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Mar 06 21:14:27 2015 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Fri Mar 06 21:20:30 2015 +0100 @@ -228,12 +228,12 @@ (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) (* if j < i, then turn around *) -fun get_compat_thm thy cts i j ctxi ctxj = +fun get_compat_thm ctxt cts i j ctxi ctxj = let val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj - val lhsi_eq_lhsj = Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) + val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) in if j < i then let val compat = lookup_compat_thm j i cts @@ -287,8 +287,10 @@ end -fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj = +fun mk_uniqueness_clause ctxt globals compat_store clausei clausej RLj = let + val thy = Proof_Context.theory_of ctxt + val Globals {h, y, x, fvar, ...} = globals val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei @@ -298,18 +300,18 @@ mk_clause_context x ctxti cdescj val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' - val compat = get_compat_thm thy compat_store i j cctxi cctxj + val compat = get_compat_thm ctxt compat_store i j cctxi cctxj val Ghsj' = map (fn RCInfo {h_assum, ...} => - Thm.assume (Thm.global_cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj + Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj val RLj_import = RLj |> fold Thm.forall_elim cqsj' |> fold Thm.elim_implies agsj' |> fold Thm.elim_implies Ghsj' - val y_eq_rhsj'h = Thm.assume (Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = Thm.assume (Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) + val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) @@ -324,12 +326,13 @@ (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h) |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj') - |> fold_rev Thm.forall_intr (Thm.global_cterm_of thy h :: cqsj') + |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj') end -fun mk_uniqueness_case ctxt globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = +fun mk_uniqueness_case ctxt + globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = let val thy = Proof_Context.theory_of ctxt val Globals {x, y, ranT, fvar, ...} = globals @@ -348,7 +351,7 @@ val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = - map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas + map2 (mk_uniqueness_clause ctxt globals compat_store clausei) clauses rep_lemmas fun elim_implies_eta A AB = Thm.bicompose (SOME ctxt) {flatten = false, match = true, incremented = false} @@ -548,11 +551,11 @@ ctxt') end -fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = +fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) = let fun inst_term t = subst_bound(f, abstract_over (fvar, t)) in - (rcfix, map (Thm.assume o Thm.global_cterm_of thy o inst_term o Thm.prop_of) rcassm, inst_term rcarg) + (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg) end @@ -594,34 +597,35 @@ val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} -fun mk_partial_induct_rule thy globals R complete_thm clauses = +fun mk_partial_induct_rule ctxt globals R complete_thm clauses = let val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R - val x_D = Thm.assume (Thm.global_cterm_of thy (HOLogic.mk_Trueprop (D $ x))) - val a_D = Thm.global_cterm_of thy (HOLogic.mk_Trueprop (D $ a)) + val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x))) + val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a)) - val D_subset = Thm.global_cterm_of thy (Logic.all x - (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) + val D_subset = + Thm.cterm_of ctxt (Logic.all x + (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), HOLogic.mk_Trueprop (D $ z))))) - |> Thm.global_cterm_of thy + |> Thm.cterm_of ctxt (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (P $ Bound 0))) - |> Thm.global_cterm_of thy + |> Thm.cterm_of ctxt val aihyp = Thm.assume ihyp fun prove_case clause = let - val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, + val ClauseInfo {cdata = ClauseContext {ctxt = ctxt1, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, qglr = (oqs, _, _, _), ...} = clause val case_hyp_conv = K (case_hyp RS eq_reflection) @@ -629,14 +633,14 @@ val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D val sih = fconv_rule (Conv.binder_conv - (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp + (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp end fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih - |> Thm.forall_elim (Thm.global_cterm_of thy rcarg) + |> Thm.forall_elim (Thm.cterm_of ctxt rcarg) |> Thm.elim_implies llRI |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas - |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy o Free) RIvs + |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) @@ -645,7 +649,7 @@ |> fold_rev (curry Logic.mk_implies) gs |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - |> Thm.global_cterm_of thy + |> Thm.cterm_of ctxt val P_lhs = Thm.assume step |> fold Thm.forall_elim cqs @@ -653,7 +657,7 @@ |> fold Thm.elim_implies ags |> fold Thm.elim_implies P_recs - val res = Thm.global_cterm_of thy (HOLogic.mk_Trueprop (P $ x)) + val res = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x)) |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |> Thm.symmetric (* P lhs == P x *) |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) @@ -671,7 +675,7 @@ |> fold (curry op COMP) cases (* P x *) |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cprop_of x_D) - |> Thm.forall_intr (Thm.global_cterm_of thy x) + |> Thm.forall_intr (Thm.cterm_of ctxt x) val subset_induct_rule = acc_subset_induct @@ -686,16 +690,15 @@ val simple_induct_rule = subset_induct_rule - |> Thm.forall_intr (Thm.global_cterm_of thy D) - |> Thm.forall_elim (Thm.global_cterm_of thy acc_R) + |> Thm.forall_intr (Thm.cterm_of ctxt D) + |> Thm.forall_elim (Thm.cterm_of ctxt acc_R) |> atac 1 |> Seq.hd |> (curry op COMP) (acc_downward - |> (instantiate' [SOME (Thm.global_ctyp_of thy domT)] - (map (SOME o Thm.global_cterm_of thy) [R, x, z])) - |> Thm.forall_intr (Thm.global_cterm_of thy z) - |> Thm.forall_intr (Thm.global_cterm_of thy x)) - |> Thm.forall_intr (Thm.global_cterm_of thy a) - |> Thm.forall_intr (Thm.global_cterm_of thy P) + |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z])) + |> Thm.forall_intr (Thm.cterm_of ctxt z) + |> Thm.forall_intr (Thm.cterm_of ctxt x)) + |> Thm.forall_intr (Thm.cterm_of ctxt a) + |> Thm.forall_intr (Thm.cterm_of ctxt P) in simple_induct_rule end @@ -860,7 +863,7 @@ val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy - val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss + val RCss = map (map (inst_RC lthy fvar f)) RCss val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees val ((R, RIntro_thmss, R_elim), lthy) = @@ -906,7 +909,7 @@ (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function val simple_pinduct = PROFILE "Proving partial induction rule" - (mk_partial_induct_rule newthy globals R complete_thm) xclauses + (mk_partial_induct_rule newctxt globals R complete_thm) xclauses val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newctxt globals R R_elim) xclauses diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/function_elims.ML --- a/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 21:14:27 2015 +0100 +++ b/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 21:20:30 2015 +0100 @@ -79,8 +79,6 @@ fun mk_partial_elim_rules ctxt result = let - val thy = Proof_Context.theory_of ctxt; - val FunctionResult {fs, R, dom, psimps, cases, ...} = result; val n_fs = length fs; diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Fri Mar 06 21:14:27 2015 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Fri Mar 06 21:20:30 2015 +0100 @@ -45,8 +45,8 @@ fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true (map meta (@{thm split_conv} :: @{thms sum.case})) -fun term_conv thy cv t = - cv (Thm.global_cterm_of thy t) +fun term_conv ctxt cv t = + cv (Thm.cterm_of ctxt t) |> Thm.prop_of |> Logic.dest_equals |> snd fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) @@ -194,7 +194,7 @@ HOLogic.mk_Trueprop (list_comb (P, map Free xs)) |> fold_rev (curry Logic.mk_implies) Cs |> fold_rev (Logic.all o Free) ws - |> term_conv thy (ind_atomize ctxt) + |> term_conv ctxt (ind_atomize ctxt) |> Object_Logic.drop_judgment thy |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) in diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 21:14:27 2015 +0100 +++ b/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 21:20:30 2015 +0100 @@ -23,10 +23,10 @@ fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var -fun inst_case_thm thy x P thm = +fun inst_case_thm ctxt x P thm = let val [Pv, xv] = Term.add_vars (Thm.prop_of thm) [] in - thm |> cterm_instantiate (map (apply2 (Thm.global_cterm_of thy)) [(Var xv, x), (Var Pv, P)]) + thm |> cterm_instantiate (map (apply2 (Thm.cterm_of ctxt)) [(Var xv, x), (Var Pv, P)]) end fun invent_vars constr i = @@ -40,26 +40,24 @@ (avs, pvs, j) end -fun filter_pats ctxt cons pvars [] = [] - | filter_pats ctxt cons pvars (([], thm) :: pts) = raise Match +fun filter_pats _ _ _ [] = [] + | filter_pats _ _ _ (([], _) :: _) = raise Match | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) = - let val inst = list_comb (cons, pvars) in - (inst :: pats, - inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm) - :: (filter_pats ctxt cons pvars pts) - end - | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = - if fst (strip_comb pat) = cons - then (pat :: pats, thm) :: (filter_pats thy cons pvars pts) - else filter_pats thy cons pvars pts + let val inst = list_comb (cons, pvars) in + (inst :: pats, inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm) :: + filter_pats ctxt cons pvars pts + end + | filter_pats ctxt cons pvars ((pat :: pats, thm) :: pts) = + if fst (strip_comb pat) = cons + then (pat :: pats, thm) :: filter_pats ctxt cons pvars pts + else filter_pats ctxt cons pvars pts -fun transform_pat _ avars c_assum ([] , thm) = raise Match +fun transform_pat _ _ _ ([] , _) = raise Match | transform_pat ctxt avars c_assum (pat :: pats, thm) = let val (_, subps) = strip_comb pat - val eqs = - map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) + val eqs = map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) val c_eq_pat = simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum in @@ -95,13 +93,12 @@ (Thm.cterm_of ctxt v) thm))) pts) else (* Cons case *) let - val thy = Proof_Context.theory_of ctxt val T as Type (tname, _) = fastype_of v val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname val constrs = inst_constrs_of ctxt T val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs in - inst_case_thm thy v P case_thm + inst_case_thm ctxt v P case_thm |> fold (curry op COMP) c_cases end | o_alg _ _ _ _ _ = raise Match diff -r a6e977d8b070 -r bb1e4a35d506 src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Fri Mar 06 21:14:27 2015 +0100 +++ b/src/HOL/Tools/Function/relation.ML Fri Mar 06 21:20:30 2015 +0100 @@ -15,17 +15,15 @@ (* tactic version *) -fun inst_state_tac inst st = +fun inst_state_tac ctxt inst st = (case Term.add_vars (Thm.prop_of st) [] of (* FIXME tactic should not inspect main conclusion *) [v as (_, T)] => - let val thy = Thm.theory_of_thm st in - PRIMITIVE (Thm.instantiate ([], [(Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy (inst T))])) st - end + PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) st | _ => Seq.empty); fun relation_tac ctxt rel i = TRY (Function_Common.termination_rule_tac ctxt i) - THEN inst_state_tac rel; + THEN inst_state_tac ctxt rel; (* version with type inference *)