added Thm.chyps_of;
authorwenzelm
Sun Aug 16 19:25:08 2015 +0200 (2015-08-16)
changeset 60949ccbf9379e355
parent 60948 b710a5087116
child 60950 35a3f66629ad
added Thm.chyps_of;
eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
src/HOL/Eisbach/match_method.ML
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/Library/old_recdef.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/sat.ML
src/HOL/ex/Meson_Test.thy
src/Pure/Isar/code.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/obtain.ML
src/Pure/drule.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Eisbach/match_method.ML	Sun Aug 16 18:19:30 2015 +0200
     1.2 +++ b/src/HOL/Eisbach/match_method.ML	Sun Aug 16 19:25:08 2015 +0200
     1.3 @@ -400,7 +400,7 @@
     1.4    let
     1.5      val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
     1.6      val hyp =
     1.7 -      (case #hyps (Thm.crep_thm prem) of
     1.8 +      (case Thm.chyps_of prem of
     1.9          [hyp] => hyp
    1.10        | _ => error "Prem should have exactly one hyp");  (* FIXME error vs. raise Fail !? *)
    1.11      val ct = Drule.mk_term (hyp) |> Thm.cprop_of;
    1.12 @@ -455,7 +455,7 @@
    1.13  
    1.14  fun get_thinned_prems goal =
    1.15    let
    1.16 -    val chyps = Thm.crep_thm goal |> #hyps;
    1.17 +    val chyps = Thm.chyps_of goal;
    1.18  
    1.19      fun prem_from_hyp hyp goal =
    1.20      let
    1.21 @@ -735,7 +735,7 @@
    1.22                      (focus_prems inner_ctxt |> snd |> Item_Net.content)
    1.23                      (focus_prems focus_ctxt |> snd |> Item_Net.content))
    1.24                      |> map (fn (id, thm) =>
    1.25 -                        #hyps (Thm.crep_thm thm)
    1.26 +                        Thm.chyps_of thm
    1.27                          |> (fn [chyp] => (id, (SOME chyp, NONE))
    1.28                               | _ => error "Prem should have only one hyp")));
    1.29  
     2.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Aug 16 18:19:30 2015 +0200
     2.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Aug 16 19:25:08 2015 +0200
     2.3 @@ -694,7 +694,7 @@
     2.4      Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq
     2.5  
     2.6    fun declare_hyps ctxt thm =
     2.7 -    (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
     2.8 +    (thm, snd (Assumption.add_assumes (Thm.chyps_of thm) ctxt))
     2.9  in
    2.10  
    2.11  val abstraction_depth = 3
     3.1 --- a/src/HOL/Library/old_recdef.ML	Sun Aug 16 18:19:30 2015 +0200
     3.2 +++ b/src/HOL/Library/old_recdef.ML	Sun Aug 16 19:25:08 2015 +0200
     3.3 @@ -914,8 +914,8 @@
     3.4  fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
     3.5  
     3.6  
     3.7 -fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm));
     3.8 -fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
     3.9 +fun cconcl thm = Dcterm.drop_prop (Thm.cprop_of thm);
    3.10 +fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm);
    3.11  
    3.12  fun dest_thm thm =
    3.13    let val {prop,hyps,...} = Thm.rep_thm thm
    3.14 @@ -971,7 +971,7 @@
    3.15  fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
    3.16    handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
    3.17  
    3.18 -fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
    3.19 +fun DISCH_ALL thm = fold_rev DISCH (Thm.chyps_of thm) thm;
    3.20  
    3.21  
    3.22  fun FILTER_DISCH_ALL P thm =
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Sun Aug 16 18:19:30 2015 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Aug 16 19:25:08 2015 +0200
     4.3 @@ -540,7 +540,7 @@
     4.4      fun simple_choose v th =
     4.5        choose v
     4.6          (Thm.assume
     4.7 -          ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
     4.8 +          ((Thm.apply @{cterm Trueprop} o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
     4.9  
    4.10      val strip_forall =
    4.11        let
     5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Sun Aug 16 18:19:30 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sun Aug 16 19:25:08 2015 +0200
     5.3 @@ -354,7 +354,7 @@
     5.4    val gts' = map replace_rule gts
     5.5    val nubs = map (conjunct2 o norm_mp) asl
     5.6    val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
     5.7 -  val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1))
     5.8 +  val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
     5.9    val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
    5.10    val cps = map (swap o Thm.dest_equals) (cprems_of th11)
    5.11    val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
     6.1 --- a/src/HOL/Tools/Function/mutual.ML	Sun Aug 16 18:19:30 2015 +0200
     6.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sun Aug 16 19:25:08 2015 +0200
     6.3 @@ -182,7 +182,7 @@
     6.4        | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
     6.5        | _ => raise General.Fail "Too many conditions"
     6.6  
     6.7 -    val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
     6.8 +    val simp_ctxt = fold Thm.declare_hyps (Thm.chyps_of simp) ctxt
     6.9    in
    6.10      Goal.prove simp_ctxt [] []
    6.11        (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
     7.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Aug 16 18:19:30 2015 +0200
     7.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Aug 16 19:25:08 2015 +0200
     7.3 @@ -433,7 +433,7 @@
     7.4          val (prems0, concl) = th |> Thm.prop_of |> Logic.strip_horn
     7.5          val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
     7.6          val goal = Logic.list_implies (prems, concl)
     7.7 -        val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
     7.8 +        val ctxt' = fold Thm.declare_hyps (Thm.chyps_of th) ctxt
     7.9          val tac =
    7.10            cut_tac th 1 THEN
    7.11            rewrite_goals_tac ctxt' meta_not_not THEN
    7.12 @@ -727,7 +727,7 @@
    7.13        val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
    7.14                         cat_lines (map string_of_subst_info substs))
    7.15  *)
    7.16 -      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
    7.17 +      val ctxt' = fold Thm.declare_hyps (Thm.chyps_of prems_imp_false) ctxt
    7.18  
    7.19        fun cut_and_ex_tac axiom =
    7.20          cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac ctxt' @{thms exE}) 1)
     8.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Aug 16 18:19:30 2015 +0200
     8.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Aug 16 19:25:08 2015 +0200
     8.3 @@ -522,7 +522,7 @@
     8.4  
     8.5  fun lemma ctxt (thms as [thm]) t =
     8.6      (let
     8.7 -       val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm)))
     8.8 +       val tab = Termtab.make (map (`Thm.term_of) (Thm.chyps_of thm))
     8.9         val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
    8.10       in
    8.11         prove_abstract ctxt [thm'] t prop_tac (
     9.1 --- a/src/HOL/Tools/groebner.ML	Sun Aug 16 18:19:30 2015 +0200
     9.2 +++ b/src/HOL/Tools/groebner.ML	Sun Aug 16 19:25:08 2015 +0200
     9.3 @@ -496,7 +496,7 @@
     9.4  
     9.5  fun simple_choose v th =
     9.6     choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
     9.7 -    ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
     9.8 +    (Thm.dest_arg (hd (Thm.chyps_of th))))) th
     9.9  
    9.10  
    9.11   fun mkexi v th =
    10.1 --- a/src/HOL/Tools/sat.ML	Sun Aug 16 18:19:30 2015 +0200
    10.2 +++ b/src/HOL/Tools/sat.ML	Sun Aug 16 19:25:08 2015 +0200
    10.3 @@ -226,7 +226,7 @@
    10.4              val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
    10.5              val raw = CNF.clause2raw_thm ctxt thm
    10.6              val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
    10.7 -              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
    10.8 +              Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw))
    10.9              val clause = (raw, hyps)
   10.10              val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   10.11            in
    11.1 --- a/src/HOL/ex/Meson_Test.thy	Sun Aug 16 18:19:30 2015 +0200
    11.2 +++ b/src/HOL/ex/Meson_Test.thy	Sun Aug 16 19:25:08 2015 +0200
    11.3 @@ -37,7 +37,7 @@
    11.4      val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
    11.5      val go25 :: _ = Meson.gocls clauses25;
    11.6  
    11.7 -    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
    11.8 +    val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go25 :: horns25)) ctxt;
    11.9      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   11.10        resolve_tac ctxt' [go25] 1 THEN
   11.11        Meson.depth_prolog_tac ctxt' horns25);
   11.12 @@ -63,7 +63,7 @@
   11.13      val _ = @{assert} (length horns26 = 24);
   11.14      val go26 :: _ = Meson.gocls clauses26;
   11.15  
   11.16 -    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
   11.17 +    val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go26 :: horns26)) ctxt;
   11.18      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   11.19        resolve_tac ctxt' [go26] 1 THEN
   11.20        Meson.depth_prolog_tac ctxt' horns26);  (*7 ms*)
   11.21 @@ -90,7 +90,7 @@
   11.22      val _ = @{assert} (length horns43 = 16);
   11.23      val go43 :: _ = Meson.gocls clauses43;
   11.24  
   11.25 -    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
   11.26 +    val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go43 :: horns43)) ctxt;
   11.27      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   11.28        resolve_tac ctxt' [go43] 1 THEN
   11.29        Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43);   (*7ms*)
    12.1 --- a/src/Pure/Isar/code.ML	Sun Aug 16 18:19:30 2015 +0200
    12.2 +++ b/src/Pure/Isar/code.ML	Sun Aug 16 19:25:08 2015 +0200
    12.3 @@ -686,7 +686,7 @@
    12.4  
    12.5  fun get_head thy cert_thm =
    12.6    let
    12.7 -    val [head] = (#hyps o Thm.crep_thm) cert_thm;
    12.8 +    val [head] = Thm.chyps_of cert_thm;
    12.9      val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head;
   12.10    in (typscheme thy (c, ty), head) end;
   12.11  
    13.1 --- a/src/Pure/Isar/element.ML	Sun Aug 16 18:19:30 2015 +0200
    13.2 +++ b/src/Pure/Isar/element.ML	Sun Aug 16 19:25:08 2015 +0200
    13.3 @@ -359,7 +359,7 @@
    13.4    Drule.forall_elim_list (map (Thm.global_cterm_of thy o snd) subst);
    13.5  
    13.6  fun hyps_rule rule th =
    13.7 -  let val {hyps, ...} = Thm.crep_thm th in
    13.8 +  let val hyps = Thm.chyps_of th in
    13.9      Drule.implies_elim_list
   13.10        (rule (Drule.implies_intr_list hyps th))
   13.11        (map (Thm.assume o Drule.cterm_rule rule) hyps)
   13.12 @@ -452,7 +452,7 @@
   13.13    thm |> fold (fn hyp =>
   13.14      (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
   13.15        NONE => I
   13.16 -    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
   13.17 +    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (Thm.chyps_of thm);
   13.18  
   13.19  val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
   13.20  
    14.1 --- a/src/Pure/Isar/expression.ML	Sun Aug 16 18:19:30 2015 +0200
    14.2 +++ b/src/Pure/Isar/expression.ML	Sun Aug 16 19:25:08 2015 +0200
    14.3 @@ -702,7 +702,7 @@
    14.4        |> Conjunction.elim_balanced (length ts);
    14.5  
    14.6      val (_, axioms_ctxt) = defs_ctxt
    14.7 -      |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
    14.8 +      |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts));
    14.9      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   14.10        Element.prove_witness axioms_ctxt t
   14.11         (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
    15.1 --- a/src/Pure/Isar/obtain.ML	Sun Aug 16 18:19:30 2015 +0200
    15.2 +++ b/src/Pure/Isar/obtain.ML	Sun Aug 16 19:25:08 2015 +0200
    15.3 @@ -54,7 +54,7 @@
    15.4        error "Conclusion in obtained context must be object-logic judgment";
    15.5  
    15.6      val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt;
    15.7 -    val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
    15.8 +    val prems = Drule.strip_imp_prems (Thm.cprop_of thm');
    15.9    in
   15.10      ((Drule.implies_elim_list thm' (map Thm.assume prems)
   15.11          |> Drule.implies_intr_list (map (Drule.norm_hhf_cterm ctxt') As)
    16.1 --- a/src/Pure/drule.ML	Sun Aug 16 18:19:30 2015 +0200
    16.2 +++ b/src/Pure/drule.ML	Sun Aug 16 19:25:08 2015 +0200
    16.3 @@ -233,8 +233,7 @@
    16.4      Frees, or outer quantifiers; all generality expressed by Vars of index 0.**)
    16.5  
    16.6  (*Discharge all hypotheses.*)
    16.7 -fun implies_intr_hyps th =
    16.8 -  fold Thm.implies_intr (#hyps (Thm.crep_thm th)) th;
    16.9 +fun implies_intr_hyps th = fold Thm.implies_intr (Thm.chyps_of th) th;
   16.10  
   16.11  (*Squash a theorem's flexflex constraints provided it can be done uniquely.
   16.12    This step can lose information.*)
    17.1 --- a/src/Pure/thm.ML	Sun Aug 16 18:19:30 2015 +0200
    17.2 +++ b/src/Pure/thm.ML	Sun Aug 16 19:25:08 2015 +0200
    17.3 @@ -58,14 +58,6 @@
    17.4      hyps: term Ord_List.T,
    17.5      tpairs: (term * term) list,
    17.6      prop: term}
    17.7 -  val crep_thm: thm ->
    17.8 -   {thy: theory,
    17.9 -    tags: Properties.T,
   17.10 -    maxidx: int,
   17.11 -    shyps: sort Ord_List.T,
   17.12 -    hyps: cterm Ord_List.T,
   17.13 -    tpairs: (cterm * cterm) list,
   17.14 -    prop: cterm}
   17.15    val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
   17.16    val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   17.17    val terms_of_tpairs: (term * term) list -> term list
   17.18 @@ -85,6 +77,7 @@
   17.19    val major_prem_of: thm -> term
   17.20    val cprop_of: thm -> cterm
   17.21    val cprem_of: thm -> int -> cterm
   17.22 +  val chyps_of: thm -> cterm list
   17.23    val transfer: theory -> thm -> thm
   17.24    val renamed_prop: term -> thm -> thm
   17.25    val weaken: cterm -> thm -> thm
   17.26 @@ -353,14 +346,6 @@
   17.27  
   17.28  fun rep_thm (Thm (_, args)) = args;
   17.29  
   17.30 -fun crep_thm (Thm (_, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
   17.31 -  let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in
   17.32 -   {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
   17.33 -    hyps = map (cterm ~1) hyps,
   17.34 -    tpairs = map (apply2 (cterm maxidx)) tpairs,
   17.35 -    prop = cterm maxidx prop}
   17.36 -  end;
   17.37 -
   17.38  fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
   17.39    fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
   17.40  
   17.41 @@ -420,7 +405,6 @@
   17.42      prem :: _ => Logic.strip_assums_concl prem
   17.43    | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
   17.44  
   17.45 -(*the statement of any thm is a cterm*)
   17.46  fun cprop_of (Thm (_, {thy, maxidx, shyps, prop, ...})) =
   17.47    Cterm {thy = thy, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
   17.48  
   17.49 @@ -428,6 +412,9 @@
   17.50    Cterm {thy = thy, maxidx = maxidx, T = propT, sorts = shyps,
   17.51      t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
   17.52  
   17.53 +fun chyps_of (Thm (_, {thy, shyps, hyps, ...})) =
   17.54 +  map (fn t => Cterm {thy = thy, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
   17.55 +
   17.56  (*explicit transfer to a super theory*)
   17.57  fun transfer thy' thm =
   17.58    let