# HG changeset patch # User wenzelm # Date 1132684490 -3600 # Node ID e5a624483a23c1a3ba85fad153a22f07fff15673 # Parent 628c117800770ab5e0bf4fdeb5b05734991fe7ad added type cases/cases_tactic, and CASES, SUBGOAL_CASES; added consume rule; support named case conclusions; tuned interfaces; diff -r 628c11780077 -r e5a624483a23 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Tue Nov 22 19:34:48 2005 +0100 +++ b/src/Pure/Isar/rule_cases.ML Tue Nov 22 19:34:50 2005 +0100 @@ -2,48 +2,80 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Manage local contexts of rules. +Annotations and local contexts of rules. *) infix 1 THEN_ALL_NEW_CASES; +signature BASIC_RULE_CASES = +sig + type cases + type cases_tactic + val CASES: cases -> tactic -> cases_tactic + val NO_CASES: tactic -> cases_tactic + val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic + val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic +end + signature RULE_CASES = sig + include BASIC_RULE_CASES + type T + val consume: thm list -> ('a * int) * thm -> (('a * (int * thm list)) * thm) Seq.seq val consumes: int -> 'a attribute val consumes_default: int -> 'a attribute val name: string list -> thm -> thm val case_names: string list -> 'a attribute + val case_conclusion: string -> (string * string) list -> 'a attribute + val case_conclusion_binops: string -> string list -> 'a attribute val save: thm -> thm -> thm - val get: thm -> string list * int - val add: thm -> thm * (string list * int) - type T + val get: thm -> (string * (string * string) list) list * int val strip_params: term -> (string * typ) list - val make: bool -> term option -> theory * term -> string list -> (string * T option) list + val make: bool -> term option -> theory * term -> + (string * (string * string) list) list -> cases val simple: bool -> theory * term -> string -> string * T option val rename_params: string list list -> thm -> thm val params: string list list -> 'a attribute - type tactic - val NO_CASES: Tactical.tactic -> tactic - val THEN_ALL_NEW_CASES: (int -> tactic) * (int -> Tactical.tactic) -> int -> tactic end; structure RuleCases: RULE_CASES = struct -(* names *) +(** tactics with cases **) + +type T = + {fixes: (string * typ) list, + assumes: (string * term list) list, + binds: (indexname * term option) list}; + +type cases = (string * T option) list; +type cases_tactic = thm -> (cases * thm) Seq.seq; + +fun CASES cases tac st = Seq.map (pair cases) (tac st); +fun NO_CASES tac = CASES [] tac; + +fun SUBGOAL_CASES tac i st = + (case try Logic.nth_prem (i, Thm.prop_of st) of + SOME goal => tac (goal, i) st + | NONE => Seq.empty); + +fun (tac1 THEN_ALL_NEW_CASES tac2) i st = + st |> tac1 i |> Seq.maps (fn (cases, st') => + Seq.map (pair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')); + + + +(** consume facts **) + +fun consume facts ((x, n), th) = + Drule.multi_resolves (Library.take (n, facts)) [th] + |> Seq.map (pair (x, (n - length facts, Library.drop (n, facts)))); val consumes_tagN = "consumes"; -val cases_tagN = "cases"; -val case_conclN = "case"; -val case_hypsN = "hyps"; -val case_premsN = "prems"; - -(* number of consumed facts *) - -fun lookup_consumes thm = - let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in - (case AList.lookup (op =) (Thm.tags_of_thm thm) (consumes_tagN) of +fun lookup_consumes th = + let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in + (case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of NONE => NONE | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ()) | _ => err ()) @@ -61,109 +93,155 @@ if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x; -(* case names *) + +(** case names **) + +val cases_tagN = "cases"; -fun put_case_names NONE thm = thm - | put_case_names (SOME names) thm = - thm - |> Drule.untag_rule cases_tagN - |> Drule.tag_rule (cases_tagN, names); +fun add_case_names NONE = I + | add_case_names (SOME names) = + Drule.untag_rule cases_tagN + #> Drule.tag_rule (cases_tagN, names); -fun lookup_case_names thm = AList.lookup (op =) (Thm.tags_of_thm thm) cases_tagN; +fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) cases_tagN; -val save_case_names = put_case_names o lookup_case_names; -val name = put_case_names o SOME; +val save_case_names = add_case_names o lookup_case_names; +val name = add_case_names o SOME; fun case_names ss = Drule.rule_attribute (K (name ss)); + +(** case conclusions **) + +(* term positions *) + +fun term_at pos tm = + let + fun at [] t = t + | at ("0" :: ps) (t $ _) = at ps t + | at ("1" :: ps) (_ $ u) = at ps u + | at _ _ = raise TERM ("Bad term position: " ^ pos, [tm]); + in at (explode pos) tm end; + +fun binop_positions [] = [] + | binop_positions [x] = [(x, "")] + | binop_positions xs = + let + fun pos i = replicate_string i "1"; + val k = length xs - 1; + in xs ~~ (map (suffix "01" o pos) (0 upto k - 1) @ [pos k]) end; + + +(* conclusion tags *) + +val case_concl_tagN = "case_conclusion"; + +fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name) + | is_case_concl _ _ = false; + +fun add_case_concl (name, cs) = Drule.map_tags (fn tags => + filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]); + +fun lookup_case_concl th name = + find_first (is_case_concl name) (Thm.tags_of_thm th) |> Option.map (tl o snd); + +fun get_case_concls th name = + let + fun concls (x :: pos :: cs) = (x, pos) :: concls cs + | concls [] = [] + | concls [x] = error ("No position for conclusion " ^ quote x ^ " of case " ^ quote name); + in concls (these (lookup_case_concl th name)) end; + +fun save_case_concls th = + let val concls = Thm.tags_of_thm th |> List.mapPartial + (fn (a, b :: bs) => + if a = case_concl_tagN then SOME (b, bs) else NONE + | _ => NONE) + in fold add_case_concl concls end; + +fun case_conclusion name concls = Drule.rule_attribute (fn _ => + add_case_concl (name, List.concat (map (fn (a, b) => [a, b]) concls))); + +fun case_conclusion_binops name xs = case_conclusion name (binop_positions xs); + + + +(** case declarations **) + (* access hints *) -fun save thm = save_case_names thm o save_consumes thm; +fun save th = save_consumes th #> save_case_names th #> save_case_concls th; -fun get thm = +fun get th = let - val n = if_none (lookup_consumes thm) 0; - val ss = - (case lookup_case_names thm of - NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n)) - | SOME ss => ss); - in (ss, n) end; - -fun add thm = (thm, get thm); + val n = the_default 0 (lookup_consumes th); + val cases = + (case lookup_case_names th of + NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n)) + | SOME names => map (fn name => (name, get_case_concls th name)) names); + in (cases, n) end; -(* prepare cases *) +(* extract cases *) -type T = - {fixes: (string * typ) list, - assumes: (string * term list) list, - binds: (indexname * term option) list}; +val case_conclN = "case"; +val case_hypsN = "hyps"; +val case_premsN = "prems"; val strip_params = map (apfst Syntax.deskolem) o Logic.strip_params; -fun prep_case is_open thy (split, raw_prop) name = +fun extract_case is_open thy (split, raw_prop) name concls = let val prop = Drule.norm_hhf thy raw_prop; val xs = strip_params prop; val rename = if is_open then I else map (apfst Syntax.internal); - val named_xs = + val fixes = (case split of NONE => rename xs | SOME t => let val (us, vs) = splitAt (length (Logic.strip_params t), xs) in rename us @ vs end); + fun abs_fixes t = Term.list_abs (fixes, t); - val asms = map (curry Term.list_abs named_xs) (Logic.strip_assums_hyp prop); - val named_asms = + val asms = map abs_fixes (Logic.strip_assums_hyp prop); + val assumes = (case split of NONE => [("", asms)] | SOME t => let val (hyps, prems) = splitAt (length (Logic.strip_assums_hyp t), asms) in [(case_hypsN, hyps), (case_premsN, prems)] end); - val concl = Term.list_abs (named_xs, Logic.strip_assums_concl prop); - val bind = ((case_conclN, 0), SOME (ObjectLogic.drop_judgment thy concl)); - in (name, SOME {fixes = named_xs, assumes = named_asms, binds = [bind]}) end; + val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop); + fun bind (x, pos) = ((x, 0), SOME (abs_fixes (term_at pos concl))); + val binds = bind (case_conclN, "") :: map bind concls; + in {fixes = fixes, assumes = assumes, binds = binds} end; -fun make is_open split (thy, prop) names = +fun make is_open split (thy, prop) cases = let + val n = length cases; val nprems = Logic.count_prems (prop, 0); - fun add_case name (cases, i) = + fun add_case (name, concls) (cs, i) = ((case try (fn () => (Option.map (curry Logic.nth_prem i) split, Logic.nth_prem (i, prop))) () of NONE => (name, NONE) - | SOME sp => prep_case is_open thy sp name) :: cases, i - 1); - in - fold_rev add_case (Library.drop (length names - nprems, names)) ([], length names) - |> #1 - end; + | SOME sp => (name, SOME (extract_case is_open thy sp name concls))) :: cs, i - 1); + in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end; -fun simple is_open (thy, prop) = prep_case is_open thy (NONE, prop); +fun simple is_open (thy, prop) name = + (name, SOME (extract_case is_open thy (NONE, prop) name [])); (* params *) -fun rename_params xss thm = - thm - |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i+1)) xss - |> save thm; +fun rename_params xss th = + th + |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss + |> save th; fun params xss = Drule.rule_attribute (K (rename_params xss)); - -(* tactics with cases *) - -type tactic = thm -> (thm * (string * T option) list) Seq.seq; - -fun NO_CASES tac = Seq.map (rpair []) o tac; - -fun (tac1 THEN_ALL_NEW_CASES tac2) i st = - st |> tac1 i |> Seq.maps (fn (st', cases) => - Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')); - end; -val NO_CASES = RuleCases.NO_CASES; -val op THEN_ALL_NEW_CASES = RuleCases.THEN_ALL_NEW_CASES; - +structure BasicRuleCases: BASIC_RULE_CASES = RuleCases; +open BasicRuleCases;