# HG changeset patch # User wenzelm # Date 1440755589 -7200 # Node ID 80f40d89dab609a8491047d0e19b3360d0c446d6 # Parent 9c28a4feebd18cee84fafb3bf6ba4a93e548f094 tuned signature; diff -r 9c28a4feebd1 -r 80f40d89dab6 src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Aug 28 11:53:09 2015 +0200 @@ -191,12 +191,8 @@ datatype cthm = ComputeThm of term list * sort list * term fun thm2cthm th = - let - val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th - val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else () - in - ComputeThm (hyps, shyps, prop) - end + (if not (null (Thm.tpairs_of th)) then raise Make "theorems may not contain tpairs" else (); + ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th)) fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths = let diff -r 9c28a4feebd1 -r 80f40d89dab6 src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Aug 28 11:53:09 2015 +0200 @@ -367,16 +367,13 @@ datatype cthm = ComputeThm of term list * sort list * term -fun thm2cthm th = - let - val {hyps, prop, shyps, ...} = Thm.rep_thm th - in - ComputeThm (hyps, shyps, prop) - end +fun thm2cthm th = ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th) -val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord +val cthm_ord' = + prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord -fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) +fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = + cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) structure CThmtab = Table(type key = cthm val ord = cthm_ord) diff -r 9c28a4feebd1 -r 80f40d89dab6 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Fri Aug 28 11:52:06 2015 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Aug 28 11:53:09 2015 +0200 @@ -14,8 +14,9 @@ ML {* fun export_proof thy thm = let - val {prop, hyps, shyps, ...} = Thm.rep_thm thm; - val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)); + val (_, prop) = + Logic.unconstrainT (Thm.shyps_of thm) + (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> Reconstruct.reconstruct_proof thy prop |> diff -r 9c28a4feebd1 -r 80f40d89dab6 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/Pure/Proof/extraction.ML Fri Aug 28 11:53:09 2015 +0200 @@ -364,7 +364,7 @@ let val S = Sign.defaultS thy; val ((atyp_map, constraints, _), prop') = - Logic.unconstrainT (#shyps (Thm.rep_thm thm)) (Thm.prop_of thm); + Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm); val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) []; val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then SOME (TVar (("'" ^ v, i), [])) else NONE) diff -r 9c28a4feebd1 -r 80f40d89dab6 src/Pure/display.ML --- a/src/Pure/display.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/Pure/display.ML Fri Aug 28 11:53:09 2015 +0200 @@ -52,27 +52,28 @@ val show_hyps = Config.get ctxt show_hyps; val th = Thm.strip_shyps raw_th; - val {hyps, tpairs, prop, ...} = Thm.rep_thm th; - val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th; + + val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = Thm.extra_shyps th; val tags = Thm.get_tags th; + val tpairs = Thm.tpairs_of th; val q = if quote then Pretty.quote else I; val prt_term = q o Syntax.pretty_term ctxt; - val hlen = length extra_shyps + length hyps' + length tpairs; + val hlen = length extra_shyps + length hyps + length tpairs; val hsymbs = if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" - (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ + (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ map (Syntax.pretty_sort ctxt) extra_shyps)] else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; - in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; + in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; diff -r 9c28a4feebd1 -r 80f40d89dab6 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/Pure/goal_display.ML Fri Aug 28 11:53:09 2015 +0200 @@ -114,7 +114,7 @@ val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of; - val {prop, tpairs, ...} = Thm.rep_thm state; + val prop = Thm.prop_of state; val (As, B) = Logic.strip_horn prop; val ngoals = length As; in @@ -124,7 +124,7 @@ pretty_subgoals (take goals_limit As) @ [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] else pretty_subgoals As) @ - pretty_ffpairs tpairs @ + pretty_ffpairs (Thm.tpairs_of state) @ (if show_consts then pretty_consts prop else []) @ (if show_types then pretty_vars prop else []) @ (if show_sorts0 then pretty_varsT prop else []) diff -r 9c28a4feebd1 -r 80f40d89dab6 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/Pure/more_thm.ML Fri Aug 28 11:53:09 2015 +0200 @@ -161,21 +161,19 @@ (* thm order: ignores theory context! *) -fun thm_ord (th1, th2) = - let - val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1; - val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2; - in - (case Term_Ord.fast_term_ord (prop1, prop2) of - EQUAL => - (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of - EQUAL => - (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of - EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2) - | ord => ord) - | ord => ord) - | ord => ord) - end; +fun thm_ord ths = + (case Term_Ord.fast_term_ord (apply2 Thm.prop_of ths) of + EQUAL => + (case + list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) + (apply2 Thm.tpairs_of ths) + of + EQUAL => + (case list_ord Term_Ord.fast_term_ord (apply2 Thm.hyps_of ths) of + EQUAL => list_ord Term_Ord.sort_ord (apply2 Thm.shyps_of ths) + | ord => ord) + | ord => ord) + | ord => ord); (* tables and caches *) @@ -240,15 +238,14 @@ let val thm = Thm.strip_shyps raw_thm; fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); - val {hyps, prop, tpairs, ...} = Thm.rep_thm thm; in - if not (null hyps) then + if not (null (Thm.hyps_of thm)) then err "theorem may not contain hypotheses" else if not (null (Thm.extra_shyps thm)) then err "theorem may not contain sort hypotheses" - else if not (null tpairs) then + else if not (null (Thm.tpairs_of thm)) then err "theorem may not contain flex-flex pairs" - else prop + else Thm.prop_of thm end; diff -r 9c28a4feebd1 -r 80f40d89dab6 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Aug 28 11:52:06 2015 +0200 +++ b/src/Pure/thm.ML Fri Aug 28 11:53:09 2015 +0200 @@ -70,6 +70,7 @@ val theory_name_of_thm: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int + val shyps_of: thm -> sort Ord_List.T val hyps_of: thm -> term list val prop_of: thm -> term val tpairs_of: thm -> (term * term) list @@ -412,6 +413,7 @@ val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); +val shyps_of = #shyps o rep_thm; val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; val tpairs_of = #tpairs o rep_thm;