clarified modules;
authorwenzelm
Fri Oct 23 17:17:11 2015 +0200 (2015-10-23)
changeset 615082c7e2ae6173d
parent 61507 6865140215ef
child 61509 358dfae15d83
clarified modules;
tuned signature;
src/Pure/Isar/proof.ML
src/Pure/goal.ML
src/Pure/more_thm.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Oct 23 16:09:06 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Oct 23 17:17:11 2015 +0200
     1.3 @@ -501,7 +501,7 @@
     1.4        (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
     1.5          handle THM _ => err_lost ())
     1.6        |> Drule.flexflex_unique (SOME ctxt)
     1.7 -      |> Thm.check_shyps ctxt (Variable.sorts_of ctxt)
     1.8 +      |> Thm.check_shyps ctxt
     1.9        |> Thm.check_hyps (Context.Proof ctxt);
    1.10  
    1.11      val goal_propss = filter_out null propss;
    1.12 @@ -947,7 +947,7 @@
    1.13      val goal =
    1.14        Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
    1.15        |> Thm.cterm_of goal_ctxt
    1.16 -      |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
    1.17 +      |> Thm.weaken_sorts' goal_ctxt;
    1.18      val statement = ((kind, pos), propss', Thm.term_of goal);
    1.19  
    1.20      val after_qed' = after_qed |>> (fn after_local => fn results =>
     2.1 --- a/src/Pure/goal.ML	Fri Oct 23 16:09:06 2015 +0200
     2.2 +++ b/src/Pure/goal.ML	Fri Oct 23 17:17:11 2015 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4      val global_prop =
     2.5        Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
     2.6        |> Thm.cterm_of ctxt
     2.7 -      |> Thm.weaken_sorts (Variable.sorts_of ctxt);
     2.8 +      |> Thm.weaken_sorts' ctxt;
     2.9      val global_result = result |> Future.map
    2.10        (Drule.flexflex_unique (SOME ctxt) #>
    2.11          Thm.adjust_maxidx_thm ~1 #>
    2.12 @@ -196,9 +196,8 @@
    2.13        |> fold Variable.declare_term (asms @ props)
    2.14        |> Assumption.add_assumes casms
    2.15        ||> Variable.set_body true;
    2.16 -    val sorts = Variable.sorts_of ctxt';
    2.17  
    2.18 -    val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
    2.19 +    val stmt = Thm.weaken_sorts' ctxt' (Conjunction.mk_conjunction_balanced cprops);
    2.20  
    2.21      fun tac' args st =
    2.22        if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt
    2.23 @@ -214,7 +213,7 @@
    2.24              val res =
    2.25                (finish ctxt' st
    2.26                  |> Drule.flexflex_unique (SOME ctxt')
    2.27 -                |> Thm.check_shyps ctxt' sorts
    2.28 +                |> Thm.check_shyps ctxt'
    2.29                  |> Thm.check_hyps (Context.Proof ctxt'))
    2.30                handle THM (msg, _, _) => err msg | ERROR msg => err msg;
    2.31            in
     3.1 --- a/src/Pure/more_thm.ML	Fri Oct 23 16:09:06 2015 +0200
     3.2 +++ b/src/Pure/more_thm.ML	Fri Oct 23 17:17:11 2015 +0200
     3.3 @@ -48,7 +48,6 @@
     3.4    val equiv_thm: theory -> thm * thm -> bool
     3.5    val class_triv: theory -> class -> thm
     3.6    val of_sort: ctyp * sort -> thm list
     3.7 -  val check_shyps: Proof.context -> sort list -> thm -> thm
     3.8    val is_dummy: thm -> bool
     3.9    val plain_prop_of: thm -> term
    3.10    val add_thm: thm -> thm list -> thm list
    3.11 @@ -63,6 +62,9 @@
    3.12    val restore_hyps: Proof.context -> Proof.context -> Proof.context
    3.13    val undeclared_hyps: Context.generic -> thm -> term list
    3.14    val check_hyps: Context.generic -> thm -> thm
    3.15 +  val declare_term_sorts: term -> Proof.context -> Proof.context
    3.16 +  val check_shyps: Proof.context -> thm -> thm
    3.17 +  val weaken_sorts': Proof.context -> cterm -> cterm
    3.18    val elim_implies: thm -> thm -> thm
    3.19    val forall_intr_name: string * cterm -> thm -> thm
    3.20    val forall_elim_var: int -> thm -> thm
    3.21 @@ -229,16 +231,6 @@
    3.22  
    3.23  fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
    3.24  
    3.25 -fun check_shyps ctxt sorts raw_th =
    3.26 -  let
    3.27 -    val th = Thm.strip_shyps raw_th;
    3.28 -    val pending = Sorts.subtract sorts (Thm.extra_shyps th);
    3.29 -  in
    3.30 -    if null pending then th
    3.31 -    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
    3.32 -      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
    3.33 -  end;
    3.34 -
    3.35  
    3.36  (* misc operations *)
    3.37  
    3.38 @@ -274,22 +266,33 @@
    3.39  
    3.40  
    3.41  
    3.42 -(** declared hyps **)
    3.43 +(** declared hyps and sort hyps **)
    3.44  
    3.45  structure Hyps = Proof_Data
    3.46  (
    3.47 -  type T = Termtab.set * bool;
    3.48 -  fun init _ : T = (Termtab.empty, true);
    3.49 +  type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T};
    3.50 +  fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []};
    3.51  );
    3.52  
    3.53 -fun declare_hyps raw_ct ctxt =
    3.54 -  let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct
    3.55 -  in (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt end;
    3.56 +fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
    3.57 +  let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps)
    3.58 +  in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end);
    3.59 +
    3.60 +
    3.61 +(* hyps *)
    3.62 +
    3.63 +fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
    3.64 +  let
    3.65 +    val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct;
    3.66 +    val hyps' = Termtab.update (Thm.term_of ct, ()) hyps;
    3.67 +  in (checked_hyps, hyps', shyps) end);
    3.68  
    3.69  fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
    3.70  
    3.71 -val unchecked_hyps = (Hyps.map o apsnd) (K false);
    3.72 -fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
    3.73 +val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps));
    3.74 +
    3.75 +fun restore_hyps ctxt =
    3.76 +  map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps));
    3.77  
    3.78  fun undeclared_hyps context th =
    3.79    Thm.hyps_of th
    3.80 @@ -298,8 +301,8 @@
    3.81        Context.Theory _ => K false
    3.82      | Context.Proof ctxt =>
    3.83          (case Hyps.get ctxt of
    3.84 -          (_, false) => K true
    3.85 -        | (hyps, _) => Termtab.defined hyps));
    3.86 +          {checked_hyps = false, ...} => K true
    3.87 +        | {hyps, ...} => Termtab.defined hyps));
    3.88  
    3.89  fun check_hyps context th =
    3.90    (case undeclared_hyps context th of
    3.91 @@ -309,6 +312,25 @@
    3.92          (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared))));
    3.93  
    3.94  
    3.95 +(* shyps *)
    3.96 +
    3.97 +fun declare_term_sorts t =
    3.98 +  map_hyps (fn (checked_hyps, hyps, shyps) =>
    3.99 +    (checked_hyps, hyps, Sorts.insert_term t shyps));
   3.100 +
   3.101 +fun check_shyps ctxt raw_th =
   3.102 +  let
   3.103 +    val th = Thm.strip_shyps raw_th;
   3.104 +    val pending = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
   3.105 +  in
   3.106 +    if null pending then th
   3.107 +    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
   3.108 +      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
   3.109 +  end;
   3.110 +
   3.111 +val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get;
   3.112 +
   3.113 +
   3.114  
   3.115  (** basic derived rules **)
   3.116  
     4.1 --- a/src/Pure/variable.ML	Fri Oct 23 16:09:06 2015 +0200
     4.2 +++ b/src/Pure/variable.ML	Fri Oct 23 17:17:11 2015 +0200
     4.3 @@ -9,7 +9,6 @@
     4.4    val names_of: Proof.context -> Name.context
     4.5    val binds_of: Proof.context -> (typ * term) Vartab.table
     4.6    val maxidx_of: Proof.context -> int
     4.7 -  val sorts_of: Proof.context -> sort list
     4.8    val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
     4.9    val is_declared: Proof.context -> string -> bool
    4.10    val check_name: binding -> string
    4.11 @@ -111,18 +110,17 @@
    4.12    binds: (typ * term) Vartab.table,     (*term bindings*)
    4.13    type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
    4.14    maxidx: int,                          (*maximum var index*)
    4.15 -  sorts: sort Ord_List.T,               (*declared sort occurrences*)
    4.16    constraints:
    4.17      typ Vartab.table *                  (*type constraints*)
    4.18      sort Vartab.table};                 (*default sorts*)
    4.19  
    4.20 -fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
    4.21 +fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =
    4.22    Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds,
    4.23 -    type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
    4.24 +    type_occs = type_occs, maxidx = maxidx, constraints = constraints};
    4.25  
    4.26  val empty_data =
    4.27    make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
    4.28 -    Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
    4.29 +    Symtab.empty, ~1, (Vartab.empty, Vartab.empty));
    4.30  
    4.31  structure Data = Proof_Data
    4.32  (
    4.33 @@ -131,44 +129,40 @@
    4.34  );
    4.35  
    4.36  fun map_data f =
    4.37 -  Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
    4.38 -    make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
    4.39 +  Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} =>
    4.40 +    make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)));
    4.41  
    4.42  fun map_names f =
    4.43 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.44 -    (f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
    4.45 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.46 +    (f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints));
    4.47  
    4.48  fun map_consts f =
    4.49 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.50 -    (names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
    4.51 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.52 +    (names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints));
    4.53  
    4.54  fun map_bounds f =
    4.55 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.56 -    (names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
    4.57 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.58 +    (names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints));
    4.59  
    4.60  fun map_fixes f =
    4.61 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.62 -    (names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
    4.63 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.64 +    (names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints));
    4.65  
    4.66  fun map_binds f =
    4.67 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.68 -    (names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
    4.69 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.70 +    (names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints));
    4.71  
    4.72  fun map_type_occs f =
    4.73 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.74 -    (names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
    4.75 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.76 +    (names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints));
    4.77  
    4.78  fun map_maxidx f =
    4.79 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.80 -    (names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
    4.81 -
    4.82 -fun map_sorts f =
    4.83 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.84 -    (names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
    4.85 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.86 +    (names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints));
    4.87  
    4.88  fun map_constraints f =
    4.89 -  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
    4.90 -    (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
    4.91 +  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
    4.92 +    (names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints));
    4.93  
    4.94  fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
    4.95  
    4.96 @@ -178,7 +172,6 @@
    4.97  val binds_of = #binds o rep_data;
    4.98  val type_occs_of = #type_occs o rep_data;
    4.99  val maxidx_of = #maxidx o rep_data;
   4.100 -val sorts_of = #sorts o rep_data;
   4.101  val constraints_of = #constraints o rep_data;
   4.102  
   4.103  val is_declared = Name.is_declared o names_of;
   4.104 @@ -260,7 +253,7 @@
   4.105  fun declare_internal t =
   4.106    declare_names t #>
   4.107    declare_type_occs t #>
   4.108 -  map_sorts (Sorts.insert_term t);
   4.109 +  Thm.declare_term_sorts t;
   4.110  
   4.111  fun declare_term t =
   4.112    declare_internal t #>