support for split assumptions in cases (hyps vs. prems);
authorwenzelm
Fri Jul 26 21:09:39 2002 +0200 (2002-07-26)
changeset 13425119ae829ad9b
parent 13424 584a4a4c30ed
child 13426 e0e2351043d2
support for split assumptions in cases (hyps vs. prems);
NEWS
doc-src/IsarRef/generic.tex
src/Provers/induct_method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
     1.1 --- a/NEWS	Fri Jul 26 21:07:57 2002 +0200
     1.2 +++ b/NEWS	Fri Jul 26 21:09:39 2002 +0200
     1.3 @@ -15,6 +15,10 @@
     1.4  context; potential INCOMPATIBILITY, use "(open)" option to fall back
     1.5  on the old view without predicates;
     1.6  
     1.7 +* improved induct method: assumptions introduced by case "foo" are
     1.8 +split into "foo.hyps" (from the rule) and "foo.prems" (from the goal
     1.9 +statement); "foo" still refers to all facts collectively;
    1.10 +
    1.11  * improved thms_containing: proper indexing of facts instead of raw
    1.12  theorems; check validity of results wrt. current name space; include
    1.13  local facts of proof configuration (also covers active locales); an
     2.1 --- a/doc-src/IsarRef/generic.tex	Fri Jul 26 21:07:57 2002 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Fri Jul 26 21:09:39 2002 +0200
     2.3 @@ -1227,6 +1227,12 @@
     2.4  $\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
     2.5    x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
     2.6  
     2.7 +In induction proofs, local assumptions introduced by cases are split into two
     2.8 +different kinds: $hyps$ stemming from the rule and $prems$ from the goal
     2.9 +statement.  This is reflected in the extracted cases accordingly, so invoking
    2.10 +``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and
    2.11 +$c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list.
    2.12 +
    2.13  \medskip
    2.14  
    2.15  Facts presented to either method are consumed according to the number of
     3.1 --- a/src/Provers/induct_method.ML	Fri Jul 26 21:07:57 2002 +0200
     3.2 +++ b/src/Provers/induct_method.ML	Fri Jul 26 21:09:39 2002 +0200
     3.3 @@ -111,7 +111,7 @@
     3.4  
     3.5      fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
     3.6        (Method.multi_resolves (take (n, facts)) [th]);
     3.7 -  in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end;
     3.8 +  in resolveq_cases_tac (RuleCases.make open_parms None) (Seq.flat (Seq.map prep_rule ruleq)) end;
     3.9  
    3.10  in
    3.11  
    3.12 @@ -186,7 +186,7 @@
    3.13              (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
    3.14            |> Drule.implies_intr_list cprems
    3.15            |> Drule.standard'
    3.16 -          |> RuleCases.save th]
    3.17 +          |> RuleCases.save r]
    3.18          end;
    3.19  
    3.20  
    3.21 @@ -230,7 +230,7 @@
    3.22      |> (Method.insert_tac more_facts THEN' atomize_tac) i
    3.23      |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
    3.24            st' |> Tactic.rtac rule' i
    3.25 -          |> Seq.map (rpair (make (rulified_term rule') cases)))
    3.26 +          |> Seq.map (rpair (make (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
    3.27        |> Seq.flat)
    3.28      |> Seq.flat)
    3.29    |> Seq.flat;
    3.30 @@ -329,7 +329,7 @@
    3.31  val term_dummy = Scan.unless (Scan.lift kind_inst)
    3.32    (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
    3.33  
    3.34 -val instss = Args.and_list (Scan.repeat1 term_dummy);
    3.35 +val instss = Args.and_list (Scan.repeat term_dummy);
    3.36  
    3.37  in
    3.38  
     4.1 --- a/src/Pure/Isar/proof.ML	Fri Jul 26 21:07:57 2002 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Fri Jul 26 21:09:39 2002 +0200
     4.3 @@ -621,10 +621,17 @@
     4.4    let
     4.5      val (state', (lets, asms)) =
     4.6        map_context_result (ProofContext.apply_case (get_case state name xs)) state;
     4.7 +    val assumptions = asms |> map (fn (a, ts) =>
     4.8 +      ((if a = "" then "" else NameSpace.append name a, atts), map (rpair ([], [])) ts));
     4.9 +    val qnames = filter_out (equal "") (map (#1 o #1) assumptions);
    4.10    in
    4.11      state'
    4.12      |> add_binds_i lets
    4.13 -    |> assume_i [((name, atts), map (rpair ([], [])) asms)]
    4.14 +    |> map_context (ProofContext.qualified true)
    4.15 +    |> assume_i assumptions
    4.16 +    |> map_context (ProofContext.hide_thms false qnames)
    4.17 +    |> (fn st => simple_have_thms name (the_facts st) st)
    4.18 +    |> map_context (ProofContext.restore_qualified (context_of state))
    4.19    end;
    4.20  
    4.21  
    4.22 @@ -678,7 +685,7 @@
    4.23        (after_qed o map_context gen_binds, pr)))
    4.24      |> map_context (ProofContext.add_cases
    4.25       (if length props = 1 then
    4.26 -      RuleCases.make true (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
    4.27 +      RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
    4.28        else [(rule_contextN, RuleCases.empty)]))
    4.29      |> auto_bind_goal props
    4.30      |> (if is_chain state then use_facts else reset_facts)
     5.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jul 26 21:07:57 2002 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jul 26 21:09:39 2002 +0200
     5.3 @@ -79,6 +79,7 @@
     5.4    val cond_extern: context -> string -> xstring
     5.5    val qualified: bool -> context -> context
     5.6    val restore_qualified: context -> context -> context
     5.7 +  val hide_thms: bool -> string list -> context -> context
     5.8    val put_thm: string * thm -> context -> context
     5.9    val put_thms: string * thm list -> context -> context
    5.10    val put_thmss: (string * thm list) list -> context -> context
    5.11 @@ -109,7 +110,8 @@
    5.12    val bind_skolem: context -> string list -> term -> term
    5.13    val get_case: context -> string -> string option list -> RuleCases.T
    5.14    val add_cases: (string * RuleCases.T) list -> context -> context
    5.15 -  val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
    5.16 +  val apply_case: RuleCases.T -> context
    5.17 +    -> context * ((indexname * term option) list * (string * term list) list)
    5.18    val pretty_term: context -> term -> Pretty.T
    5.19    val pretty_typ: context -> typ -> Pretty.T
    5.20    val pretty_sort: context -> sort -> Pretty.T
    5.21 @@ -946,7 +948,7 @@
    5.22  val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I);
    5.23  
    5.24  
    5.25 -(* qualified names *)
    5.26 +(* name space operations *)
    5.27  
    5.28  fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
    5.29  
    5.30 @@ -956,6 +958,11 @@
    5.31  
    5.32  fun restore_qualified (Context {thms, ...}) = qualified (#1 thms);
    5.33  
    5.34 +fun hide_thms fully names =
    5.35 +  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
    5.36 +    (thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index),
    5.37 +      cases, defs));
    5.38 +
    5.39  
    5.40  (* put_thm(s) *)
    5.41  
    5.42 @@ -1201,7 +1208,7 @@
    5.43        | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
    5.44    in
    5.45      if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso
    5.46 -      null (foldr Term.add_term_vars (assumes, [])) then
    5.47 +      null (foldr Term.add_term_vars (flat (map #2 assumes), [])) then
    5.48          {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
    5.49      else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
    5.50    end;
    5.51 @@ -1272,7 +1279,7 @@
    5.52      fun bind (c, (x, T)) = (c |> fix_i [([x], Some T)], bind_skolem c [x] (Free (x, T)));
    5.53      val (ctxt', xs) = foldl_map bind (ctxt, fixes);
    5.54      fun app t = foldl Term.betapply (t, xs);
    5.55 -  in (ctxt', (map (apsnd (apsome app)) binds, map app assumes)) end;
    5.56 +  in (ctxt', (map (apsnd (apsome app)) binds, map (apsnd (map app)) assumes)) end;
    5.57  
    5.58  fun pretty_cases (ctxt as Context {cases, ...}) =
    5.59    let
    5.60 @@ -1282,6 +1289,9 @@
    5.61        [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
    5.62          Pretty.quote (prt_term t)];
    5.63  
    5.64 +    fun prt_asm (a, ts) = Pretty.block (Pretty.breaks
    5.65 +      ((if a = "" then [] else [Pretty.str (a ^ ":")]) @ map (Pretty.quote o prt_term) ts));
    5.66 +
    5.67      fun prt_sect _ _ _ [] = []
    5.68        | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s ::
    5.69              flat (Library.separate sep (map (Library.single o prt) xs))))];
    5.70 @@ -1291,7 +1301,8 @@
    5.71          prt_sect "fix" [] (Pretty.str o fst) fixes @
    5.72          prt_sect "let" [Pretty.str "and"] prt_let
    5.73            (mapfilter (fn (xi, Some t) => Some (xi, t) | _ => None) lets) @
    5.74 -        prt_sect "assume" [] (Pretty.quote o prt_term) asms));
    5.75 +        (if forall (null o #2) asms then []
    5.76 +          else prt_sect "assume" [Pretty.str "and"] prt_asm asms)));
    5.77  
    5.78      val cases' = rev (Library.gen_distinct Library.eq_fst cases);
    5.79    in
     6.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Jul 26 21:07:57 2002 +0200
     6.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Jul 26 21:09:39 2002 +0200
     6.3 @@ -17,7 +17,7 @@
     6.4    val add: thm -> thm * (string list * int)
     6.5    type T
     6.6    val empty: T
     6.7 -  val make: bool -> Sign.sg * term -> string list -> (string * T) list
     6.8 +  val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list
     6.9    val rename_params: string list list -> thm -> thm
    6.10    val params: string list list -> 'a attribute
    6.11  end;
    6.12 @@ -86,23 +86,35 @@
    6.13  
    6.14  (* prepare cases *)
    6.15  
    6.16 -type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
    6.17 +type T =
    6.18 + {fixes: (string * typ) list,
    6.19 +  assumes: (string * term list) list,
    6.20 +  binds: (indexname * term option) list};
    6.21 +
    6.22 +val hypsN = "hyps";
    6.23 +val premsN = "prems";
    6.24  
    6.25  val empty = {fixes = [], assumes = [], binds = []};
    6.26  
    6.27 -fun prep_case open_parms sg prop name i =
    6.28 +fun prep_case is_open split sg prop name i =
    6.29    let
    6.30      val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop))));
    6.31 -    val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
    6.32 +    val xs = map (if is_open then I else apfst Syntax.internal) (Logic.strip_params Bi);
    6.33      val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
    6.34 +    val named_asms =
    6.35 +      (case split of None => [("", asms)]
    6.36 +      | Some t =>
    6.37 +          let val h = length (Logic.strip_assums_hyp
    6.38 +            (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs t)))))
    6.39 +          in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end);
    6.40      val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
    6.41      val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl));
    6.42 -  in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
    6.43 +  in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
    6.44  
    6.45 -fun make open_parms (sg, prop) names =
    6.46 +fun make is_open split (sg, prop) names =
    6.47    let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in
    6.48 -    #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms sg prop name i :: cases, i - 1))
    6.49 -      (Library.drop (length names - nprems, names), ([], length names)))
    6.50 +    foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
    6.51 +      (Library.drop (length names - nprems, names), ([], length names)) |> #1
    6.52    end;
    6.53  
    6.54