clarified context;
authorwenzelm
Tue Jun 02 11:03:02 2015 +0200 (2015-06-02)
changeset 60362befdc10ebb42
parent 60361 88505460fde7
child 60363 5568b16aa477
clarified context;
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/split_rule.ML
src/Provers/splitter.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jun 02 10:12:46 2015 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jun 02 11:03:02 2015 +0200
     1.3 @@ -591,7 +591,7 @@
     1.4      val monos = Inductive.get_monos ctxt;
     1.5      val intrs' = Inductive.unpartition_rules intrs
     1.6        (map (fn (((s, ths), (_, k)), th) =>
     1.7 -           (s, ths ~~ Inductive.infer_intro_vars th k ths))
     1.8 +           (s, ths ~~ Inductive.infer_intro_vars thy th k ths))
     1.9           (Inductive.partition_rules raw_induct intrs ~~
    1.10            Inductive.arities_of raw_induct ~~ elims));
    1.11      val k = length (Inductive.params_of raw_induct);
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jun 02 10:12:46 2015 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jun 02 11:03:02 2015 +0200
     2.3 @@ -1449,7 +1449,7 @@
     2.4                  (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
     2.5                |> K |> Goal.prove_sorry lthy [] [] goal
     2.6                |> Thm.close_derivation
     2.7 -              |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
     2.8 +              |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
     2.9                  @{thms eqTrueE eq_False[THEN iffD1] notnotD}
    2.10                |> pair eqn_pos
    2.11                |> single
     3.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 10:12:46 2015 +0200
     3.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 11:03:02 2015 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4    val trace : bool Config.T
     3.5    val max_clauses : int Config.T
     3.6    val term_pair_of: indexname * (typ * 'a) -> term * 'a
     3.7 -  val first_order_resolve : thm -> thm -> thm
     3.8 +  val first_order_resolve : Proof.context -> thm -> thm -> thm
     3.9    val size_of_subgoals: thm -> int
    3.10    val has_too_many_clauses: Proof.context -> term -> bool
    3.11    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    3.12 @@ -98,16 +98,16 @@
    3.13  fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    3.14  
    3.15  (*FIXME: currently does not "rename variables apart"*)
    3.16 -fun first_order_resolve thA thB =
    3.17 +fun first_order_resolve ctxt thA thB =
    3.18    (case
    3.19      try (fn () =>
    3.20 -      let val thy = Thm.theory_of_thm thA
    3.21 +      let val thy = Proof_Context.theory_of ctxt
    3.22            val tmA = Thm.concl_of thA
    3.23            val Const(@{const_name Pure.imp},_) $ tmB $ _ = Thm.prop_of thB
    3.24            val tenv =
    3.25              Pattern.first_order_match thy (tmB, tmA)
    3.26                                            (Vartab.empty, Vartab.empty) |> snd
    3.27 -          val ct_pairs = map (apply2 (Thm.global_cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    3.28 +          val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
    3.29        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    3.30      SOME th => th
    3.31    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    3.32 @@ -359,11 +359,10 @@
    3.33      in (th RS spec', ctxt') end
    3.34  end;
    3.35  
    3.36 -fun apply_skolem_theorem (th, rls) =
    3.37 +fun apply_skolem_theorem ctxt (th, rls) =
    3.38    let
    3.39      fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
    3.40 -      | tryall (rl :: rls) =
    3.41 -        first_order_resolve th rl handle THM _ => tryall rls
    3.42 +      | tryall (rl :: rls) = first_order_resolve ctxt th rl handle THM _ => tryall rls
    3.43    in tryall rls end
    3.44  
    3.45  (* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    3.46 @@ -383,7 +382,7 @@
    3.47                  in  ctxt_ref := ctxt'; cnf_aux (th', ths) end
    3.48            | Const (@{const_name Ex}, _) =>
    3.49                (*existential quantifier: Insert Skolem functions*)
    3.50 -              cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
    3.51 +              cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths)
    3.52            | Const (@{const_name HOL.disj}, _) =>
    3.53                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    3.54                  all combinations of converting P, Q to CNF.*)
     4.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jun 02 10:12:46 2015 +0200
     4.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jun 02 11:03:02 2015 +0200
     4.3 @@ -85,7 +85,7 @@
     4.4                (case add_vars_and_frees u [] of
     4.5                  [] =>
     4.6                  Conv.abs_conv (conv false o snd) ctxt ct
     4.7 -                |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
     4.8 +                |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI})
     4.9                | v :: _ =>
    4.10                  Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
    4.11                  |> Thm.cterm_of ctxt
     5.1 --- a/src/HOL/Tools/choice_specification.ML	Tue Jun 02 10:12:46 2015 +0200
     5.2 +++ b/src/HOL/Tools/choice_specification.ML	Tue Jun 02 11:03:02 2015 +0200
     5.3 @@ -140,7 +140,7 @@
     5.4              val cT = Thm.ctyp_of_cterm cv
     5.5              val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
     5.6            in thm RS spec' end
     5.7 -        fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm
     5.8 +        fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
     5.9          fun process_single ((name, atts), rew_imp, frees) args =
    5.10            let
    5.11              fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm
    5.12 @@ -152,7 +152,7 @@
    5.13                  Global_Theory.store_thm (Binding.name name, thm) thy)
    5.14            in
    5.15              swap args
    5.16 -            |> apfst (remove_alls frees)
    5.17 +            |> remove_alls frees
    5.18              |> apfst undo_imps
    5.19              |> apfst Drule.export_without_context
    5.20              |-> Thm.theory_attributes
     6.1 --- a/src/HOL/Tools/inductive.ML	Tue Jun 02 10:12:46 2015 +0200
     6.2 +++ b/src/HOL/Tools/inductive.ML	Tue Jun 02 11:03:02 2015 +0200
     6.3 @@ -65,7 +65,7 @@
     6.4    val partition_rules: thm -> thm list -> (string * thm list) list
     6.5    val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
     6.6    val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
     6.7 -  val infer_intro_vars: thm -> int -> thm list -> term list list
     6.8 +  val infer_intro_vars: theory -> thm -> int -> thm list -> term list list
     6.9  end;
    6.10  
    6.11  signature INDUCTIVE =
    6.12 @@ -1132,9 +1132,8 @@
    6.13      (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
    6.14  
    6.15  (* infer order of variables in intro rules from order of quantifiers in elim rule *)
    6.16 -fun infer_intro_vars elim arity intros =
    6.17 +fun infer_intro_vars thy elim arity intros =
    6.18    let
    6.19 -    val thy = Thm.theory_of_thm elim;
    6.20      val _ :: cases = Thm.prems_of elim;
    6.21      val used = map (fst o fst) (Term.add_vars (Thm.prop_of elim) []);
    6.22      fun mtch (t, u) =
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 02 10:12:46 2015 +0200
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 02 11:03:02 2015 +0200
     7.3 @@ -19,9 +19,9 @@
     7.4      [name] => name
     7.5    | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
     7.6  
     7.7 -fun prf_of thm =
     7.8 +fun prf_of thy thm =
     7.9    Reconstruct.proof_of thm
    7.10 -  |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)];  (* FIXME *)
    7.11 +  |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
    7.12  
    7.13  fun subsets [] = [[]]
    7.14    | subsets (x::xs) =
    7.15 @@ -268,7 +268,7 @@
    7.16      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    7.17      Extraction.abs_corr_shyps thy rule vs vs2
    7.18        (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
    7.19 -         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
    7.20 +         (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
    7.21    end;
    7.22  
    7.23  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
    7.24 @@ -285,7 +285,7 @@
    7.25      val params' = map dest_Var params;
    7.26      val rss = Inductive.partition_rules raw_induct intrs;
    7.27      val rss' = map (fn (((s, rs), (_, arity)), elim) =>
    7.28 -      (s, (Inductive.infer_intro_vars elim arity rs ~~ rs)))
    7.29 +      (s, (Inductive.infer_intro_vars thy elim arity rs ~~ rs)))
    7.30          (rss ~~ arities ~~ elims);
    7.31      val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
    7.32      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
     8.1 --- a/src/HOL/Tools/split_rule.ML	Tue Jun 02 10:12:46 2015 +0200
     8.2 +++ b/src/HOL/Tools/split_rule.ML	Tue Jun 02 11:03:02 2015 +0200
     8.3 @@ -39,12 +39,11 @@
     8.4    | ap_split _ T3 u = u;
     8.5  
     8.6  (*Curries any Var of function type in the rule*)
     8.7 -fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
     8.8 +fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
     8.9        let val T' = HOLogic.flatten_tupleT T1 ---> T2;
    8.10            val newt = ap_split T1 T2 (Var (v, T'));
    8.11 -          val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
    8.12 -      in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    8.13 -  | split_rule_var' _ rl = rl;
    8.14 +      in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end
    8.15 +  | split_rule_var' _ _ rl = rl;
    8.16  
    8.17  
    8.18  (* complete splitting of partially split rules *)
    8.19 @@ -85,11 +84,11 @@
    8.20  
    8.21  
    8.22  fun split_rule_var ctxt =
    8.23 -  (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var';
    8.24 +  (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt;
    8.25  
    8.26  (*curries ALL function variables occurring in a rule's conclusion*)
    8.27  fun split_rule ctxt rl =
    8.28 -  fold_rev split_rule_var' (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
    8.29 +  fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
    8.30    |> remove_internal_split ctxt
    8.31    |> Drule.export_without_context;
    8.32  
     9.1 --- a/src/Provers/splitter.ML	Tue Jun 02 10:12:46 2015 +0200
     9.2 +++ b/src/Provers/splitter.ML	Tue Jun 02 11:03:02 2015 +0200
     9.3 @@ -285,9 +285,8 @@
     9.4     call split_posns with appropriate parameters
     9.5  *************************************************************)
     9.6  
     9.7 -fun select cmap state i =
     9.8 +fun select thy cmap state i =
     9.9    let
    9.10 -    val thy = Thm.theory_of_thm state
    9.11      val goal = Thm.term_of (Thm.cprem_of state i);
    9.12      val Ts = rev (map #2 (Logic.strip_params goal));
    9.13      val _ $ t $ _ = Logic.strip_assums_concl goal;
    9.14 @@ -313,16 +312,14 @@
    9.15     i       : no. of subgoal
    9.16  **************************************************************)
    9.17  
    9.18 -fun inst_lift Ts t (T, U, pos) state i =
    9.19 +fun inst_lift ctxt Ts t (T, U, pos) state i =
    9.20    let
    9.21 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
    9.22      val (cntxt, u) = mk_cntxt t pos (T --> U);
    9.23      val trlift' = Thm.lift_rule (Thm.cprem_of state i)
    9.24        (Thm.rename_boundvars abs_lift u trlift);
    9.25      val (P, _) = strip_comb (fst (Logic.dest_equals
    9.26        (Logic.strip_assums_concl (Thm.prop_of trlift'))));
    9.27 -  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] trlift'
    9.28 -  end;
    9.29 +  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end;
    9.30  
    9.31  
    9.32  (*************************************************************
    9.33 @@ -338,15 +335,13 @@
    9.34     i     : number of subgoal
    9.35  **************************************************************)
    9.36  
    9.37 -fun inst_split Ts t tt thm TB state i =
    9.38 +fun inst_split ctxt Ts t tt thm TB state i =
    9.39    let
    9.40      val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
    9.41      val (P, _) = strip_comb (fst (Logic.dest_equals
    9.42        (Logic.strip_assums_concl (Thm.prop_of thm'))));
    9.43 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
    9.44      val cntxt = mk_cntxt_splitthm t tt TB;
    9.45 -  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
    9.46 -  end;
    9.47 +  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end;
    9.48  
    9.49  
    9.50  (*****************************************************************************
    9.51 @@ -359,14 +354,15 @@
    9.52  fun split_tac _ [] i = no_tac
    9.53    | split_tac ctxt splits i =
    9.54    let val cmap = cmap_of_split_thms splits
    9.55 -      fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st
    9.56 +      fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift ctxt Ts t p st i, 2) i st
    9.57        fun lift_split_tac state =
    9.58 -            let val (Ts, t, splits) = select cmap state i
    9.59 +            let val (Ts, t, splits) = select (Proof_Context.theory_of ctxt) cmap state i
    9.60              in case splits of
    9.61                   [] => no_tac state
    9.62                 | (thm, apsns, pos, TB, tt)::_ =>
    9.63                     (case apsns of
    9.64 -                      [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state
    9.65 +                      [] =>
    9.66 +                        compose_tac ctxt (false, inst_split ctxt Ts t tt thm TB state i, 0) i state
    9.67                      | p::_ => EVERY [lift_tac Ts t p,
    9.68                                       resolve_tac ctxt [reflexive_thm] (i+1),
    9.69                                       lift_split_tac] state)