# HG changeset patch # User wenzelm # Date 1027710579 -7200 # Node ID 119ae829ad9b22aeb97072128f37a088c467437e # Parent 584a4a4c30ed52a25fb2b4f3a319e78fcd064eb9 support for split assumptions in cases (hyps vs. prems); diff -r 584a4a4c30ed -r 119ae829ad9b NEWS --- a/NEWS Fri Jul 26 21:07:57 2002 +0200 +++ b/NEWS Fri Jul 26 21:09:39 2002 +0200 @@ -15,6 +15,10 @@ context; potential INCOMPATIBILITY, use "(open)" option to fall back on the old view without predicates; +* improved induct method: assumptions introduced by case "foo" are +split into "foo.hyps" (from the rule) and "foo.prems" (from the goal +statement); "foo" still refers to all facts collectively; + * improved thms_containing: proper indexing of facts instead of raw theorems; check validity of results wrt. current name space; include local facts of proof configuration (also covers active locales); an diff -r 584a4a4c30ed -r 119ae829ad9b doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Fri Jul 26 21:07:57 2002 +0200 +++ b/doc-src/IsarRef/generic.tex Fri Jul 26 21:09:39 2002 +0200 @@ -1227,6 +1227,12 @@ $\vec\phi$. Also note that local definitions may be expressed as $\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. +In induction proofs, local assumptions introduced by cases are split into two +different kinds: $hyps$ stemming from the rule and $prems$ from the goal +statement. This is reflected in the extracted cases accordingly, so invoking +``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and +$c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list. + \medskip Facts presented to either method are consumed according to the number of diff -r 584a4a4c30ed -r 119ae829ad9b src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Fri Jul 26 21:07:57 2002 +0200 +++ b/src/Provers/induct_method.ML Fri Jul 26 21:09:39 2002 +0200 @@ -111,7 +111,7 @@ fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases) (Method.multi_resolves (take (n, facts)) [th]); - in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end; + in resolveq_cases_tac (RuleCases.make open_parms None) (Seq.flat (Seq.map prep_rule ruleq)) end; in @@ -186,7 +186,7 @@ (map (fn x => Drule.implies_elim_list x asms) (th :: ths)) |> Drule.implies_intr_list cprems |> Drule.standard' - |> RuleCases.save th] + |> RuleCases.save r] end; @@ -230,7 +230,7 @@ |> (Method.insert_tac more_facts THEN' atomize_tac) i |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' => st' |> Tactic.rtac rule' i - |> Seq.map (rpair (make (rulified_term rule') cases))) + |> Seq.map (rpair (make (Some (Thm.prop_of rule')) (rulified_term rule') cases))) |> Seq.flat) |> Seq.flat) |> Seq.flat; @@ -329,7 +329,7 @@ val term_dummy = Scan.unless (Scan.lift kind_inst) (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some); -val instss = Args.and_list (Scan.repeat1 term_dummy); +val instss = Args.and_list (Scan.repeat term_dummy); in diff -r 584a4a4c30ed -r 119ae829ad9b src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Jul 26 21:07:57 2002 +0200 +++ b/src/Pure/Isar/proof.ML Fri Jul 26 21:09:39 2002 +0200 @@ -621,10 +621,17 @@ let val (state', (lets, asms)) = map_context_result (ProofContext.apply_case (get_case state name xs)) state; + val assumptions = asms |> map (fn (a, ts) => + ((if a = "" then "" else NameSpace.append name a, atts), map (rpair ([], [])) ts)); + val qnames = filter_out (equal "") (map (#1 o #1) assumptions); in state' |> add_binds_i lets - |> assume_i [((name, atts), map (rpair ([], [])) asms)] + |> map_context (ProofContext.qualified true) + |> assume_i assumptions + |> map_context (ProofContext.hide_thms false qnames) + |> (fn st => simple_have_thms name (the_facts st) st) + |> map_context (ProofContext.restore_qualified (context_of state)) end; @@ -678,7 +685,7 @@ (after_qed o map_context gen_binds, pr))) |> map_context (ProofContext.add_cases (if length props = 1 then - RuleCases.make true (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] + RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] else [(rule_contextN, RuleCases.empty)])) |> auto_bind_goal props |> (if is_chain state then use_facts else reset_facts) diff -r 584a4a4c30ed -r 119ae829ad9b src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Jul 26 21:07:57 2002 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Jul 26 21:09:39 2002 +0200 @@ -79,6 +79,7 @@ val cond_extern: context -> string -> xstring val qualified: bool -> context -> context val restore_qualified: context -> context -> context + val hide_thms: bool -> string list -> context -> context val put_thm: string * thm -> context -> context val put_thms: string * thm list -> context -> context val put_thmss: (string * thm list) list -> context -> context @@ -109,7 +110,8 @@ val bind_skolem: context -> string list -> term -> term val get_case: context -> string -> string option list -> RuleCases.T val add_cases: (string * RuleCases.T) list -> context -> context - val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list) + val apply_case: RuleCases.T -> context + -> context * ((indexname * term option) list * (string * term list) list) val pretty_term: context -> term -> Pretty.T val pretty_typ: context -> typ -> Pretty.T val pretty_sort: context -> sort -> Pretty.T @@ -946,7 +948,7 @@ val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I); -(* qualified names *) +(* name space operations *) fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space; @@ -956,6 +958,11 @@ fun restore_qualified (Context {thms, ...}) = qualified (#1 thms); +fun hide_thms fully names = + map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) => + (thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index), + cases, defs)); + (* put_thm(s) *) @@ -1201,7 +1208,7 @@ | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); in if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso - null (foldr Term.add_term_vars (assumes, [])) then + null (foldr Term.add_term_vars (flat (map #2 assumes), [])) then {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds} else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt) end; @@ -1272,7 +1279,7 @@ fun bind (c, (x, T)) = (c |> fix_i [([x], Some T)], bind_skolem c [x] (Free (x, T))); val (ctxt', xs) = foldl_map bind (ctxt, fixes); fun app t = foldl Term.betapply (t, xs); - in (ctxt', (map (apsnd (apsome app)) binds, map app assumes)) end; + in (ctxt', (map (apsnd (apsome app)) binds, map (apsnd (map app)) assumes)) end; fun pretty_cases (ctxt as Context {cases, ...}) = let @@ -1282,6 +1289,9 @@ [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, Pretty.quote (prt_term t)]; + fun prt_asm (a, ts) = Pretty.block (Pretty.breaks + ((if a = "" then [] else [Pretty.str (a ^ ":")]) @ map (Pretty.quote o prt_term) ts)); + fun prt_sect _ _ _ [] = [] | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s :: flat (Library.separate sep (map (Library.single o prt) xs))))]; @@ -1291,7 +1301,8 @@ prt_sect "fix" [] (Pretty.str o fst) fixes @ prt_sect "let" [Pretty.str "and"] prt_let (mapfilter (fn (xi, Some t) => Some (xi, t) | _ => None) lets) @ - prt_sect "assume" [] (Pretty.quote o prt_term) asms)); + (if forall (null o #2) asms then [] + else prt_sect "assume" [Pretty.str "and"] prt_asm asms))); val cases' = rev (Library.gen_distinct Library.eq_fst cases); in diff -r 584a4a4c30ed -r 119ae829ad9b src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Fri Jul 26 21:07:57 2002 +0200 +++ b/src/Pure/Isar/rule_cases.ML Fri Jul 26 21:09:39 2002 +0200 @@ -17,7 +17,7 @@ val add: thm -> thm * (string list * int) type T val empty: T - val make: bool -> Sign.sg * term -> string list -> (string * T) list + val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list val rename_params: string list list -> thm -> thm val params: string list list -> 'a attribute end; @@ -86,23 +86,35 @@ (* prepare cases *) -type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list}; +type T = + {fixes: (string * typ) list, + assumes: (string * term list) list, + binds: (indexname * term option) list}; + +val hypsN = "hyps"; +val premsN = "prems"; val empty = {fixes = [], assumes = [], binds = []}; -fun prep_case open_parms sg prop name i = +fun prep_case is_open split sg prop name i = let val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop)))); - val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi); + val xs = map (if is_open then I else apfst Syntax.internal) (Logic.strip_params Bi); val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); + val named_asms = + (case split of None => [("", asms)] + | Some t => + let val h = length (Logic.strip_assums_hyp + (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs t))))) + in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end); val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi); val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); - in (name, {fixes = xs, assumes = asms, binds = [bind]}) end; + in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; -fun make open_parms (sg, prop) names = +fun make is_open split (sg, prop) names = let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in - #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms sg prop name i :: cases, i - 1)) - (Library.drop (length names - nprems, names), ([], length names))) + foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1)) + (Library.drop (length names - nprems, names), ([], length names)) |> #1 end;