tuned signature;
authorwenzelm
Fri Aug 28 11:53:09 2015 +0200 (2015-08-28)
changeset 6103980f40d89dab6
parent 61038 9c28a4feebd1
child 61040 d08a0c5a68f7
tuned signature;
src/HOL/Matrix_LP/Compute_Oracle/compute.ML
src/HOL/Matrix_LP/Compute_Oracle/linker.ML
src/HOL/Proofs/ex/XML_Data.thy
src/Pure/Proof/extraction.ML
src/Pure/display.ML
src/Pure/goal_display.ML
src/Pure/more_thm.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Aug 28 11:52:06 2015 +0200
     1.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Aug 28 11:53:09 2015 +0200
     1.3 @@ -191,12 +191,8 @@
     1.4  datatype cthm = ComputeThm of term list * sort list * term
     1.5  
     1.6  fun thm2cthm th = 
     1.7 -    let
     1.8 -        val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
     1.9 -        val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
    1.10 -    in
    1.11 -        ComputeThm (hyps, shyps, prop)
    1.12 -    end
    1.13 +    (if not (null (Thm.tpairs_of th)) then raise Make "theorems may not contain tpairs" else ();
    1.14 +     ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th))
    1.15  
    1.16  fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
    1.17      let
     2.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Aug 28 11:52:06 2015 +0200
     2.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Aug 28 11:53:09 2015 +0200
     2.3 @@ -367,16 +367,13 @@
     2.4  
     2.5  datatype cthm = ComputeThm of term list * sort list * term
     2.6  
     2.7 -fun thm2cthm th =
     2.8 -    let
     2.9 -        val {hyps, prop, shyps, ...} = Thm.rep_thm th
    2.10 -    in
    2.11 -        ComputeThm (hyps, shyps, prop)
    2.12 -    end
    2.13 +fun thm2cthm th = ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th)
    2.14  
    2.15 -val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
    2.16 +val cthm_ord' =
    2.17 +  prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
    2.18  
    2.19 -fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
    2.20 +fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) =
    2.21 +  cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
    2.22  
    2.23  structure CThmtab = Table(type key = cthm val ord = cthm_ord)
    2.24  
     3.1 --- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Aug 28 11:52:06 2015 +0200
     3.2 +++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Aug 28 11:53:09 2015 +0200
     3.3 @@ -14,8 +14,9 @@
     3.4  ML {*
     3.5    fun export_proof thy thm =
     3.6      let
     3.7 -      val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
     3.8 -      val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
     3.9 +      val (_, prop) =
    3.10 +        Logic.unconstrainT (Thm.shyps_of thm)
    3.11 +          (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    3.12        val prf =
    3.13          Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
    3.14          Reconstruct.reconstruct_proof thy prop |>
     4.1 --- a/src/Pure/Proof/extraction.ML	Fri Aug 28 11:52:06 2015 +0200
     4.2 +++ b/src/Pure/Proof/extraction.ML	Fri Aug 28 11:53:09 2015 +0200
     4.3 @@ -364,7 +364,7 @@
     4.4    let
     4.5      val S = Sign.defaultS thy;
     4.6      val ((atyp_map, constraints, _), prop') =
     4.7 -      Logic.unconstrainT (#shyps (Thm.rep_thm thm)) (Thm.prop_of thm);
     4.8 +      Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
     4.9      val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
    4.10      val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
    4.11          SOME (TVar (("'" ^ v, i), [])) else NONE)
     5.1 --- a/src/Pure/display.ML	Fri Aug 28 11:52:06 2015 +0200
     5.2 +++ b/src/Pure/display.ML	Fri Aug 28 11:53:09 2015 +0200
     5.3 @@ -52,27 +52,28 @@
     5.4      val show_hyps = Config.get ctxt show_hyps;
     5.5  
     5.6      val th = Thm.strip_shyps raw_th;
     5.7 -    val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
     5.8 -    val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th;
     5.9 +
    5.10 +    val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
    5.11      val extra_shyps = Thm.extra_shyps th;
    5.12      val tags = Thm.get_tags th;
    5.13 +    val tpairs = Thm.tpairs_of th;
    5.14  
    5.15      val q = if quote then Pretty.quote else I;
    5.16      val prt_term = q o Syntax.pretty_term ctxt;
    5.17  
    5.18  
    5.19 -    val hlen = length extra_shyps + length hyps' + length tpairs;
    5.20 +    val hlen = length extra_shyps + length hyps + length tpairs;
    5.21      val hsymbs =
    5.22        if hlen = 0 then []
    5.23        else if show_hyps orelse show_hyps' then
    5.24          [Pretty.brk 2, Pretty.list "[" "]"
    5.25 -          (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    5.26 +          (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
    5.27             map (Syntax.pretty_sort ctxt) extra_shyps)]
    5.28        else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
    5.29      val tsymbs =
    5.30        if null tags orelse not show_tags then []
    5.31        else [Pretty.brk 1, pretty_tags tags];
    5.32 -  in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    5.33 +  in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
    5.34  
    5.35  fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
    5.36  fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
     6.1 --- a/src/Pure/goal_display.ML	Fri Aug 28 11:52:06 2015 +0200
     6.2 +++ b/src/Pure/goal_display.ML	Fri Aug 28 11:53:09 2015 +0200
     6.3 @@ -114,7 +114,7 @@
     6.4      val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
     6.5  
     6.6  
     6.7 -    val {prop, tpairs, ...} = Thm.rep_thm state;
     6.8 +    val prop = Thm.prop_of state;
     6.9      val (As, B) = Logic.strip_horn prop;
    6.10      val ngoals = length As;
    6.11    in
    6.12 @@ -124,7 +124,7 @@
    6.13          pretty_subgoals (take goals_limit As) @
    6.14          [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
    6.15        else pretty_subgoals As) @
    6.16 -    pretty_ffpairs tpairs @
    6.17 +    pretty_ffpairs (Thm.tpairs_of state) @
    6.18      (if show_consts then pretty_consts prop else []) @
    6.19      (if show_types then pretty_vars prop else []) @
    6.20      (if show_sorts0 then pretty_varsT prop else [])
     7.1 --- a/src/Pure/more_thm.ML	Fri Aug 28 11:52:06 2015 +0200
     7.2 +++ b/src/Pure/more_thm.ML	Fri Aug 28 11:53:09 2015 +0200
     7.3 @@ -161,21 +161,19 @@
     7.4  
     7.5  (* thm order: ignores theory context! *)
     7.6  
     7.7 -fun thm_ord (th1, th2) =
     7.8 -  let
     7.9 -    val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
    7.10 -    val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
    7.11 -  in
    7.12 -    (case Term_Ord.fast_term_ord (prop1, prop2) of
    7.13 -      EQUAL =>
    7.14 -        (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of
    7.15 -          EQUAL =>
    7.16 -            (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of
    7.17 -              EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2)
    7.18 -            | ord => ord)
    7.19 -        | ord => ord)
    7.20 -    | ord => ord)
    7.21 -  end;
    7.22 +fun thm_ord ths =
    7.23 +  (case Term_Ord.fast_term_ord (apply2 Thm.prop_of ths) of
    7.24 +    EQUAL =>
    7.25 +      (case
    7.26 +        list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord)
    7.27 +          (apply2 Thm.tpairs_of ths)
    7.28 +       of
    7.29 +        EQUAL =>
    7.30 +          (case list_ord Term_Ord.fast_term_ord (apply2 Thm.hyps_of ths) of
    7.31 +            EQUAL => list_ord Term_Ord.sort_ord (apply2 Thm.shyps_of ths)
    7.32 +          | ord => ord)
    7.33 +      | ord => ord)
    7.34 +  | ord => ord);
    7.35  
    7.36  
    7.37  (* tables and caches *)
    7.38 @@ -240,15 +238,14 @@
    7.39    let
    7.40      val thm = Thm.strip_shyps raw_thm;
    7.41      fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
    7.42 -    val {hyps, prop, tpairs, ...} = Thm.rep_thm thm;
    7.43    in
    7.44 -    if not (null hyps) then
    7.45 +    if not (null (Thm.hyps_of thm)) then
    7.46        err "theorem may not contain hypotheses"
    7.47      else if not (null (Thm.extra_shyps thm)) then
    7.48        err "theorem may not contain sort hypotheses"
    7.49 -    else if not (null tpairs) then
    7.50 +    else if not (null (Thm.tpairs_of thm)) then
    7.51        err "theorem may not contain flex-flex pairs"
    7.52 -    else prop
    7.53 +    else Thm.prop_of thm
    7.54    end;
    7.55  
    7.56  
     8.1 --- a/src/Pure/thm.ML	Fri Aug 28 11:52:06 2015 +0200
     8.2 +++ b/src/Pure/thm.ML	Fri Aug 28 11:53:09 2015 +0200
     8.3 @@ -70,6 +70,7 @@
     8.4    val theory_name_of_thm: thm -> string
     8.5    val maxidx_of: thm -> int
     8.6    val maxidx_thm: thm -> int -> int
     8.7 +  val shyps_of: thm -> sort Ord_List.T
     8.8    val hyps_of: thm -> term list
     8.9    val prop_of: thm -> term
    8.10    val tpairs_of: thm -> (term * term) list
    8.11 @@ -412,6 +413,7 @@
    8.12  
    8.13  val maxidx_of = #maxidx o rep_thm;
    8.14  fun maxidx_thm th i = Int.max (maxidx_of th, i);
    8.15 +val shyps_of = #shyps o rep_thm;
    8.16  val hyps_of = #hyps o rep_thm;
    8.17  val prop_of = #prop o rep_thm;
    8.18  val tpairs_of = #tpairs o rep_thm;