more elementary management of declared hyps, below structure Assumption;
authorwenzelm
Fri Jan 10 21:37:28 2014 +0100 (2014-01-10)
changeset 54984da70ab8531f4
parent 54983 2c57fc1f7a8c
child 54985 9a1710a64412
more elementary management of declared hyps, below structure Assumption;
Goal.prove: insist in declared hyps;
Simplifier: declare hyps via Thm.assume_hyps;
more accurate tool context in some boundary cases;
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/ex/Meson_Test.thy
src/Pure/Isar/proof.ML
src/Pure/assumption.ML
src/Pure/goal.ML
src/Pure/more_thm.ML
src/Pure/raw_simplifier.ML
     1.1 --- a/src/HOL/Tools/Function/mutual.ML	Fri Jan 10 17:44:41 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/mutual.ML	Fri Jan 10 21:37:28 2014 +0100
     1.3 @@ -187,8 +187,7 @@
     1.4        | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
     1.5        | _ => raise General.Fail "Too many conditions"
     1.6  
     1.7 -    val (_, simp_ctxt) = ctxt
     1.8 -      |> Assumption.add_assumes (#hyps (Thm.crep_thm simp))
     1.9 +    val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
    1.10    in
    1.11      Goal.prove simp_ctxt [] []
    1.12        (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jan 10 17:44:41 2014 +0100
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jan 10 21:37:28 2014 +0100
     2.3 @@ -425,16 +425,17 @@
     2.4          val (prems0, concl) = th |> prop_of |> Logic.strip_horn
     2.5          val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
     2.6          val goal = Logic.list_implies (prems, concl)
     2.7 +        val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
     2.8          val tac =
     2.9            cut_tac th 1
    2.10 -          THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]}
    2.11 +          THEN rewrite_goals_tac ctxt' @{thms not_not [THEN eq_reflection]}
    2.12            THEN ALLGOALS assume_tac
    2.13        in
    2.14          if length prems = length prems0 then
    2.15            raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
    2.16          else
    2.17 -          Goal.prove ctxt [] [] goal (K tac)
    2.18 -          |> resynchronize ctxt fol_th
    2.19 +          Goal.prove ctxt' [] [] goal (K tac)
    2.20 +          |> resynchronize ctxt' fol_th
    2.21        end
    2.22    end
    2.23  
    2.24 @@ -722,8 +723,9 @@
    2.25          THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
    2.26        fun rotation_of_subgoal i =
    2.27          find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
    2.28 +      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
    2.29      in
    2.30 -      Goal.prove ctxt [] [] @{prop False}
    2.31 +      Goal.prove ctxt' [] [] @{prop False}
    2.32            (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
    2.33                                    o fst) ax_counts)
    2.34                        THEN rename_tac outer_param_names 1
    2.35 @@ -736,9 +738,9 @@
    2.36                         THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    2.37                         THEN assume_tac i
    2.38                         THEN flexflex_tac)))
    2.39 -      handle ERROR _ =>
    2.40 -             error ("Cannot replay Metis proof in Isabelle:\n\
    2.41 -                    \Error when discharging Skolem assumptions.")
    2.42 +      handle ERROR msg =>
    2.43 +        cat_error msg
    2.44 +          "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions."
    2.45      end
    2.46  
    2.47  end;
     3.1 --- a/src/HOL/ex/Meson_Test.thy	Fri Jan 10 17:44:41 2014 +0100
     3.2 +++ b/src/HOL/ex/Meson_Test.thy	Fri Jan 10 21:37:28 2014 +0100
     3.3 @@ -37,7 +37,7 @@
     3.4      val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
     3.5      val go25 :: _ = Meson.gocls clauses25;
     3.6  
     3.7 -    val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
     3.8 +    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
     3.9      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
    3.10        rtac go25 1 THEN
    3.11        Meson.depth_prolog_tac horns25);
    3.12 @@ -63,7 +63,7 @@
    3.13      val _ = @{assert} (length horns26 = 24);
    3.14      val go26 :: _ = Meson.gocls clauses26;
    3.15  
    3.16 -    val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
    3.17 +    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
    3.18      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
    3.19        rtac go26 1 THEN
    3.20        Meson.depth_prolog_tac horns26);  (*7 ms*)
    3.21 @@ -90,7 +90,7 @@
    3.22      val _ = @{assert} (length horns43 = 16);
    3.23      val go43 :: _ = Meson.gocls clauses43;
    3.24  
    3.25 -    val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
    3.26 +    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
    3.27      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
    3.28        rtac go43 1 THEN
    3.29        Meson.best_prolog_tac Meson.size_of_subgoals horns43);   (*7ms*)
     4.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 10 17:44:41 2014 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Fri Jan 10 21:37:28 2014 +0100
     4.3 @@ -492,7 +492,7 @@
     4.4          handle THM _ => lost_structure ())
     4.5        |> Drule.flexflex_unique
     4.6        |> Thm.check_shyps (Variable.sorts_of ctxt)
     4.7 -      |> Assumption.check_hyps ctxt;
     4.8 +      |> Thm.check_hyps ctxt;
     4.9  
    4.10      val goal_propss = filter_out null propss;
    4.11      val results =
     5.1 --- a/src/Pure/assumption.ML	Fri Jan 10 17:44:41 2014 +0100
     5.2 +++ b/src/Pure/assumption.ML	Fri Jan 10 21:37:28 2014 +0100
     5.3 @@ -10,9 +10,9 @@
     5.4    val assume_export: export
     5.5    val presume_export: export
     5.6    val assume: Proof.context -> cterm -> thm
     5.7 +  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
     5.8    val all_assms_of: Proof.context -> cterm list
     5.9    val all_prems_of: Proof.context -> thm list
    5.10 -  val check_hyps: Proof.context -> thm -> thm
    5.11    val local_assms_of: Proof.context -> Proof.context -> cterm list
    5.12    val local_prems_of: Proof.context -> Proof.context -> thm list
    5.13    val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    5.14 @@ -48,8 +48,13 @@
    5.15  *)
    5.16  fun presume_export _ = assume_export false;
    5.17  
    5.18 +
    5.19  fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
    5.20  
    5.21 +fun assume_hyps ct ctxt =
    5.22 +  let val (th, ctxt') = Thm.assume_hyps ct ctxt
    5.23 +  in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end;
    5.24 +
    5.25  
    5.26  
    5.27  (** local context data **)
    5.28 @@ -76,13 +81,6 @@
    5.29  val all_assms_of = maps #2 o all_assumptions_of;
    5.30  val all_prems_of = #prems o rep_data;
    5.31  
    5.32 -fun check_hyps ctxt th =
    5.33 -  let
    5.34 -    val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    5.35 -    val _ = null extra_hyps orelse
    5.36 -      error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps));
    5.37 -  in th end;
    5.38 -
    5.39  
    5.40  (* local assumptions *)
    5.41  
    5.42 @@ -98,8 +96,8 @@
    5.43  (* add assumptions *)
    5.44  
    5.45  fun add_assms export new_asms ctxt =
    5.46 -  let val new_prems = map (assume ctxt) new_asms in
    5.47 -    ctxt
    5.48 +  let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
    5.49 +    ctxt'
    5.50      |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
    5.51      |> pair new_prems
    5.52    end;
     6.1 --- a/src/Pure/goal.ML	Fri Jan 10 17:44:41 2014 +0100
     6.2 +++ b/src/Pure/goal.ML	Fri Jan 10 21:37:28 2014 +0100
     6.3 @@ -221,7 +221,7 @@
     6.4                (finish ctxt' st
     6.5                  |> Drule.flexflex_unique
     6.6                  |> Thm.check_shyps sorts
     6.7 -                (* |> Assumption.check_hyps ctxt' FIXME *))
     6.8 +                |> Thm.check_hyps ctxt')
     6.9                handle THM (msg, _, _) => err msg | ERROR msg => err msg;
    6.10            in
    6.11              if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
     7.1 --- a/src/Pure/more_thm.ML	Fri Jan 10 17:44:41 2014 +0100
     7.2 +++ b/src/Pure/more_thm.ML	Fri Jan 10 21:37:28 2014 +0100
     7.3 @@ -52,6 +52,9 @@
     7.4    val full_rules: thm Item_Net.T
     7.5    val intro_rules: thm Item_Net.T
     7.6    val elim_rules: thm Item_Net.T
     7.7 +  val declare_hyps: cterm -> Proof.context -> Proof.context
     7.8 +  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
     7.9 +  val check_hyps: Proof.context -> thm -> thm
    7.10    val elim_implies: thm -> thm -> thm
    7.11    val forall_elim_var: int -> thm -> thm
    7.12    val forall_elim_vars: int -> thm -> thm
    7.13 @@ -259,6 +262,30 @@
    7.14  
    7.15  
    7.16  
    7.17 +(** declared hyps **)
    7.18 +
    7.19 +structure Hyps = Proof_Data
    7.20 +(
    7.21 +  type T = Termtab.set;
    7.22 +  fun init _ : T = Termtab.empty;
    7.23 +);
    7.24 +
    7.25 +fun declare_hyps ct ctxt =
    7.26 +  if Theory.subthy (theory_of_cterm ct, Proof_Context.theory_of ctxt) then
    7.27 +    Hyps.map (Termtab.update (term_of ct, ())) ctxt
    7.28 +  else raise CTERM ("assume_hyps: bad background theory", [ct]);
    7.29 +
    7.30 +fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
    7.31 +
    7.32 +fun check_hyps ctxt th =
    7.33 +  let
    7.34 +    val undeclared = filter_out (Termtab.defined (Hyps.get ctxt)) (Thm.hyps_of th);
    7.35 +    val _ = null undeclared orelse
    7.36 +      error ("Undeclared hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) undeclared));
    7.37 +  in th end;
    7.38 +
    7.39 +
    7.40 +
    7.41  (** basic derived rules **)
    7.42  
    7.43  (*Elimination of implication
     8.1 --- a/src/Pure/raw_simplifier.ML	Fri Jan 10 17:44:41 2014 +0100
     8.2 +++ b/src/Pure/raw_simplifier.ML	Fri Jan 10 21:37:28 2014 +0100
     8.3 @@ -1190,14 +1190,14 @@
     8.4        if mutsimp then mut_impc0 [] ct [] [] ctxt
     8.5        else nonmut_impc ct ctxt
     8.6  
     8.7 -    and rules_of_prem ctxt prem =
     8.8 +    and rules_of_prem prem ctxt =
     8.9        if maxidx_of_term (term_of prem) <> ~1
    8.10        then (trace_cterm ctxt true
    8.11          (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
    8.12 -        prem; ([], NONE))
    8.13 +        prem; (([], NONE), ctxt))
    8.14        else
    8.15 -        let val asm = Thm.assume prem
    8.16 -        in (extract_safe_rrules ctxt asm, SOME asm) end
    8.17 +        let val (asm, ctxt') = Thm.assume_hyps prem ctxt
    8.18 +        in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end
    8.19  
    8.20      and add_rrules (rrss, asms) ctxt =
    8.21        (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms)
    8.22 @@ -1242,10 +1242,10 @@
    8.23      and mut_impc0 prems concl rrss asms ctxt =
    8.24        let
    8.25          val prems' = strip_imp_prems concl;
    8.26 -        val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems');
    8.27 +        val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt |>> split_list;
    8.28        in
    8.29          mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
    8.30 -          (asms @ asms') [] [] [] [] ctxt ~1 ~1
    8.31 +          (asms @ asms') [] [] [] [] ctxt' ~1 ~1
    8.32        end
    8.33  
    8.34      and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k =
    8.35 @@ -1270,7 +1270,7 @@
    8.36                val tprems = map term_of prems;
    8.37                val i = 1 + fold Integer.max (map (fn p =>
    8.38                  find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
    8.39 -              val (rrs', asm') = rules_of_prem ctxt prem';
    8.40 +              val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt;
    8.41              in
    8.42                mut_impc prems concl rrss asms (prem' :: prems')
    8.43                  (rrs' :: rrss') (asm' :: asms')
    8.44 @@ -1278,7 +1278,7 @@
    8.45                    (take i prems)
    8.46                    (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
    8.47                      (drop i prems, concl))))) :: eqns)
    8.48 -                ctxt (length prems') ~1
    8.49 +                ctxt' (length prems') ~1
    8.50              end)
    8.51  
    8.52      (*legacy code -- only for backwards compatibility*)
    8.53 @@ -1289,7 +1289,9 @@
    8.54          val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
    8.55          val ctxt1 =
    8.56            if not useprem then ctxt
    8.57 -          else add_rrules (apsnd single (apfst single (rules_of_prem ctxt prem1))) ctxt
    8.58 +          else
    8.59 +            let val ((rrs, asm), ctxt') = rules_of_prem prem1 ctxt
    8.60 +            in add_rrules ([rrs], [asm]) ctxt' end;
    8.61        in
    8.62          (case botc skel0 ctxt1 conc of
    8.63            NONE =>