misc tuning -- eliminated old-fashioned rep_thm;
authorwenzelm
Mon Aug 08 17:23:15 2011 +0200 (2011-08-08)
changeset 44058ae85c5d64913
parent 44057 fda143b5c2f5
child 44059 5d367ceecf56
misc tuning -- eliminated old-fashioned rep_thm;
src/HOL/Library/positivstellensatz.ML
src/HOL/Orderings.thy
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/sat_funcs.ML
src/Provers/hypsubst.ML
src/Pure/Isar/element.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Proof/proofchecker.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 08 16:38:59 2011 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Aug 08 17:23:15 2011 +0200
     1.3 @@ -170,8 +170,8 @@
     1.4      Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
     1.5       (Thm.implies_intr (cprop_of tha) thb);
     1.6  
     1.7 -fun prove_hyp tha thb = 
     1.8 -  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
     1.9 +fun prove_hyp tha thb =
    1.10 +  if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb)  (* FIXME !? *)
    1.11    then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
    1.12  
    1.13  val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
     2.1 --- a/src/HOL/Orderings.thy	Mon Aug 08 16:38:59 2011 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Mon Aug 08 17:23:15 2011 +0200
     2.3 @@ -531,7 +531,7 @@
     2.4  setup {*
     2.5  let
     2.6  
     2.7 -fun prp t thm = (#prop (rep_thm thm) = t);
     2.8 +fun prp t thm = Thm.prop_of thm = t;  (* FIXME aconv!? *)
     2.9  
    2.10  fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
    2.11    let val prems = Simplifier.prems_of ss;
     3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 16:38:59 2011 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 17:23:15 2011 +0200
     3.3 @@ -46,7 +46,7 @@
     3.4      val recTs = Datatype_Aux.get_rec_types descr' sorts;
     3.5      val newTs = take (length (hd descr)) recTs;
     3.6  
     3.7 -    val {maxidx, ...} = rep_thm induct;
     3.8 +    val maxidx = Thm.maxidx_of induct;
     3.9      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    3.10  
    3.11      fun prove_casedist_thm (i, (T, t)) =
     4.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Aug 08 16:38:59 2011 +0200
     4.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Aug 08 17:23:15 2011 +0200
     4.3 @@ -270,7 +270,7 @@
     4.4  fun lemma thm ct =
     4.5    let
     4.6      val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
     4.7 -    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
     4.8 +    val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
     4.9      val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
    4.10    in Thm (Z3_Proof_Tools.compose ccontr th) end
    4.11  end
     5.1 --- a/src/HOL/Tools/TFL/rules.ML	Mon Aug 08 16:38:59 2011 +0200
     5.2 +++ b/src/HOL/Tools/TFL/rules.ML	Mon Aug 08 17:23:15 2011 +0200
     5.3 @@ -245,9 +245,7 @@
     5.4  
     5.5  fun DISJ_CASESL disjth thl =
     5.6     let val c = cconcl disjth
     5.7 -       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
     5.8 -                                       aconv term_of atm)
     5.9 -                              (#hyps(rep_thm th))
    5.10 +       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (Thm.hyps_of th)
    5.11         val tml = Dcterm.strip_disj c
    5.12         fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
    5.13           | DL th [th1] = PROVE_HYP th th1
     6.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Aug 08 16:38:59 2011 +0200
     6.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Aug 08 17:23:15 2011 +0200
     6.3 @@ -581,7 +581,7 @@
     6.4          (ks @ [SOME k]))) arities));
     6.5  
     6.6  fun prep_intrs intrs =
     6.7 -  map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
     6.8 +  map (Codegen.rename_term o Thm.prop_of o Drule.export_without_context) intrs;
     6.9  
    6.10  fun constrain cs [] = []
    6.11    | constrain cs ((s, xs) :: ys) =
     7.1 --- a/src/HOL/Tools/sat_funcs.ML	Mon Aug 08 16:38:59 2011 +0200
     7.2 +++ b/src/HOL/Tools/sat_funcs.ML	Mon Aug 08 17:23:15 2011 +0200
     7.3 @@ -153,11 +153,13 @@
     7.4          fun resolution (c1, hyps1) (c2, hyps2) =
     7.5            let
     7.6              val _ =
     7.7 -              if ! trace_sat then
     7.8 +              if ! trace_sat then  (* FIXME !? *)
     7.9                  tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
    7.10 -                  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
    7.11 +                  " (hyps: " ^ ML_Syntax.print_list
    7.12 +                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
    7.13                    ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
    7.14 -                  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
    7.15 +                  " (hyps: " ^ ML_Syntax.print_list
    7.16 +                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
    7.17                else ()
    7.18  
    7.19              (* the two literals used for resolution *)
    7.20 @@ -189,7 +191,7 @@
    7.21                if !trace_sat then
    7.22                  tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
    7.23                    " (hyps: " ^ ML_Syntax.print_list
    7.24 -                      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
    7.25 +                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
    7.26                else ()
    7.27              val _ = Unsynchronized.inc counter
    7.28            in
     8.1 --- a/src/Provers/hypsubst.ML	Mon Aug 08 16:38:59 2011 +0200
     8.2 +++ b/src/Provers/hypsubst.ML	Mon Aug 08 17:23:15 2011 +0200
     8.3 @@ -116,8 +116,7 @@
     8.4  (*For the simpset.  Adds ALL suitable equalities, even if not first!
     8.5    No vars are allowed here, as simpsets are built from meta-assumptions*)
     8.6  fun mk_eqs bnd th =
     8.7 -    [ if inspect_pair bnd false (Data.dest_eq
     8.8 -                                   (Data.dest_Trueprop (#prop (rep_thm th))))
     8.9 +    [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
    8.10        then th RS Data.eq_reflection
    8.11        else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
    8.12      handle TERM _ => [] | Match => [];
     9.1 --- a/src/Pure/Isar/element.ML	Mon Aug 08 16:38:59 2011 +0200
     9.2 +++ b/src/Pure/Isar/element.ML	Mon Aug 08 17:23:15 2011 +0200
     9.3 @@ -266,7 +266,7 @@
     9.4  
     9.5  val mark_witness = Logic.protect;
     9.6  fun witness_prop (Witness (t, _)) = t;
     9.7 -fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
     9.8 +fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
     9.9  fun map_witness f (Witness witn) = Witness (f witn);
    9.10  
    9.11  fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
    10.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Aug 08 16:38:59 2011 +0200
    10.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Aug 08 17:23:15 2011 +0200
    10.3 @@ -312,7 +312,7 @@
    10.4                (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
    10.5                (xis ~~ ts));
    10.6          (* Lift and instantiate rule *)
    10.7 -        val {maxidx, ...} = rep_thm st;
    10.8 +        val maxidx = Thm.maxidx_of st;
    10.9          val paramTs = map #2 params
   10.10          and inc = maxidx+1
   10.11          fun liftvar (Var ((a,j), T)) =
    11.1 --- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:38:59 2011 +0200
    11.2 +++ b/src/Pure/Proof/proofchecker.ML	Mon Aug 08 17:23:15 2011 +0200
    11.3 @@ -86,7 +86,7 @@
    11.4      fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
    11.5            let
    11.6              val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
    11.7 -            val {prop, ...} = rep_thm thm;
    11.8 +            val prop = Thm.prop_of thm;
    11.9              val _ =
   11.10                if is_equal prop prop' then ()
   11.11                else
    12.1 --- a/src/Pure/raw_simplifier.ML	Mon Aug 08 16:38:59 2011 +0200
    12.2 +++ b/src/Pure/raw_simplifier.ML	Mon Aug 08 17:23:15 2011 +0200
    12.3 @@ -1197,7 +1197,7 @@
    12.4                val prem' = Thm.rhs_of eqn;
    12.5                val tprems = map term_of prems;
    12.6                val i = 1 + fold Integer.max (map (fn p =>
    12.7 -                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
    12.8 +                find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
    12.9                val (rrs', asm') = rules_of_prem ss prem'
   12.10              in mut_impc prems concl rrss asms (prem' :: prems')
   12.11                (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
    13.1 --- a/src/Pure/simplifier.ML	Mon Aug 08 16:38:59 2011 +0200
    13.2 +++ b/src/Pure/simplifier.ML	Mon Aug 08 17:23:15 2011 +0200
    13.3 @@ -410,7 +410,7 @@
    13.4        if can Logic.dest_equals (Thm.concl_of thm) then [thm]
    13.5        else [thm RS reflect] handle THM _ => [];
    13.6  
    13.7 -    fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
    13.8 +    fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
    13.9    in
   13.10      empty_ss setsubgoaler asm_simp_tac
   13.11      setSSolver safe_solver
    14.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Aug 08 16:38:59 2011 +0200
    14.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Aug 08 17:23:15 2011 +0200
    14.3 @@ -339,7 +339,7 @@
    14.4        end
    14.5  
    14.6    val constructors =
    14.7 -      map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
    14.8 +      map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
    14.9  
   14.10    val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
   14.11  
    15.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Aug 08 16:38:59 2011 +0200
    15.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Aug 08 17:23:15 2011 +0200
    15.3 @@ -123,8 +123,7 @@
    15.4                                Syntax.string_of_term_global thy eqn);
    15.5  
    15.6      val constructors =
    15.7 -        map (head_of o const_of o FOLogic.dest_Trueprop o
    15.8 -             #prop o rep_thm) case_eqns;
    15.9 +        map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
   15.10  
   15.11      val Const (@{const_name mem}, _) $ _ $ data =
   15.12          FOLogic.dest_Trueprop (hd (prems_of elim));
    16.1 --- a/src/ZF/arith_data.ML	Mon Aug 08 16:38:59 2011 +0200
    16.2 +++ b/src/ZF/arith_data.ML	Mon Aug 08 17:23:15 2011 +0200
    16.3 @@ -61,7 +61,7 @@
    16.4  (*We remove equality assumptions because they confuse the simplifier and
    16.5    because only type-checking assumptions are necessary.*)
    16.6  fun is_eq_thm th =
    16.7 -    can FOLogic.dest_eq (FOLogic.dest_Trueprop (#prop (rep_thm th)));
    16.8 +    can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
    16.9  
   16.10  fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
   16.11  
   16.12 @@ -69,7 +69,7 @@
   16.13    if t aconv u then NONE
   16.14    else
   16.15    let val prems' = filter_out is_eq_thm prems
   16.16 -      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
   16.17 +      val goal = Logic.list_implies (map Thm.prop_of prems',
   16.18          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
   16.19    in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
   16.20        handle ERROR msg =>