# HG changeset patch # User wenzelm # Date 1136633193 -3600 # Node ID 9cdcc2a5c8b36653e0b3d47e953e987a08501d7a # Parent 7b074c340aac0ba663ecdec23a2936f84e87a10c support nested cases; added apply_case; replaced make/simple by make_common/nested/simple; diff -r 7b074c340aac -r 9cdcc2a5c8b3 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Sat Jan 07 12:26:32 2006 +0100 +++ b/src/Pure/Isar/rule_cases.ML Sat Jan 07 12:26:33 2006 +0100 @@ -20,7 +20,16 @@ signature RULE_CASES = sig include BASIC_RULE_CASES - type T + datatype T = Case of + {fixes: (string * typ) list, + assumes: (string * term list) list, + binds: (indexname * term option) list, + cases: (string * T) list} + val strip_params: term -> (string * typ) list + val make_common: bool -> theory * term -> (string * string list) list -> cases + val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases + val make_simple: bool -> theory * term -> string -> cases + val apply: term list -> T -> T val consume: thm list -> thm list -> ('a * int) * thm -> (('a * (int * thm list)) * thm) Seq.seq val add_consumes: int -> thm -> thm @@ -31,9 +40,6 @@ val case_conclusion: string * string list -> 'a attribute val save: thm -> thm -> thm val get: thm -> (string * string list) list * int - val strip_params: term -> (string * typ) list - val make: bool -> term option -> theory * term -> (string * string list) list -> cases - val simple: theory * term -> string -> cases val rename_params: string list list -> thm -> thm val params: string list list -> 'a attribute val mutual_rule: thm list -> (int list * thm) option @@ -43,14 +49,124 @@ structure RuleCases: RULE_CASES = struct +(** cases **) + +datatype T = Case of + {fixes: (string * typ) list, + assumes: (string * term list) list, + binds: (indexname * term option) list, + cases: (string * T) list}; + +type cases = (string * T option) list; + +val case_conclN = "case"; +val case_hypsN = "hyps"; +val case_premsN = "prems"; + +val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params; + +local + +fun abs xs t = Term.list_abs (xs, t); +fun app us t = Term.betapplys (t, us); + +fun dest_binops cs tm = + let + val n = length cs; + fun dest 0 _ = [] + | dest 1 t = [t] + | dest k (_ $ t $ u) = t :: dest (k - 1) u + | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]); + in cs ~~ dest n tm end; + +fun extract_fixes NONE prop = (strip_params prop, []) + | extract_fixes (SOME outline) prop = + splitAt (length (Logic.strip_params outline), strip_params prop); + +fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], []) + | extract_assumes qual (SOME outline) prop = + let val (hyps, prems) = + splitAt (length (Logic.strip_assums_hyp outline), Logic.strip_assums_hyp prop) + in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end; + +fun extract_case is_open thy (case_outline, raw_prop) name concls = + let + val rename = if is_open then I else (apfst Syntax.internal); + + val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop); + val len = length props; + val nested = is_some case_outline andalso len > 1; + + fun extract prop = + let + val (fixes1, fixes2) = extract_fixes case_outline prop + |> apfst (map rename); + val abs_fixes = abs (fixes1 @ fixes2); + fun abs_fixes1 t = + if not nested then abs_fixes t + else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t)); + + val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop + |> pairself (map (apsnd (List.concat o map Logic.dest_conjunctions))); + + val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop); + val binds = + (case_conclN, concl) :: dest_binops concls concl + |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t))); + in + ((fixes1, map (apsnd (map abs_fixes1)) assumes1), + ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds)) + end; + + val cases = map extract props; + + fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) = + Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []}; + fun inner_case (_, ((fixes2, assumes2), binds)) = + Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []}; + fun nested_case ((fixes1, assumes1), _) = + Case {fixes = fixes1, assumes = assumes1, binds = [], + cases = map string_of_int (1 upto len) ~~ map inner_case cases}; + in + if len = 0 then NONE + else if len = 1 then SOME (common_case (hd cases)) + else if is_none case_outline orelse length (gen_distinct (op =) (map fst cases)) > 1 then NONE + else SOME (nested_case (hd cases)) + end; + +fun make is_open rule_struct (thy, prop) cases = + let + val n = length cases; + val nprems = Logic.count_prems (prop, 0); + fun add_case (name, concls) (cs, i) = + ((case try (fn () => + (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of + NONE => (name, NONE) + | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1); + in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end; + +in + +fun make_common is_open = make is_open NONE; +fun make_nested is_open rule_struct = make is_open (SOME rule_struct); +fun make_simple is_open (thy, prop) name = [(name, extract_case is_open thy (NONE, prop) "" [])]; + +fun apply args = + let + fun appl (Case {fixes, assumes, binds, cases}) = + let + val assumes' = map (apsnd (map (app args))) assumes; + val binds' = map (apsnd (Option.map (app args))) binds; + val cases' = map (apsnd appl) cases; + in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end; + in appl end; + +end; + + + (** 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); @@ -181,79 +297,6 @@ in (cases, n) end; -(* extract cases *) - -val case_conclN = "case"; -val case_hypsN = "hyps"; -val case_premsN = "prems"; - -val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params; - -local - -fun dest_binops cs tm = - let - val n = length cs; - fun dest 0 _ = [] - | dest 1 t = [t] - | dest k (_ $ t $ u) = t :: dest (k - 1) u - | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]); - in cs ~~ dest n tm end; - -fun extract_cases is_open thy (split, raw_prop) name concls = - let - fun extract prop idx = - let - val xs = strip_params prop; - val rename = if is_open then I else map (apfst Syntax.internal); - 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 dest_conjuncts = map abs_fixes o List.concat o map Logic.dest_conjunctions; - - val asms = Logic.strip_assums_hyp prop; - val assumes = - (case split of - NONE => [("", dest_conjuncts asms)] - | SOME t => - let val (hyps, prems) = splitAt (length (Logic.strip_assums_hyp t), asms) in - [(case_hypsN, dest_conjuncts hyps), - (case_premsN, dest_conjuncts prems)] - end); - - val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop); - val binds = (case_conclN, concl) :: dest_binops concls concl - |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t))); - in (name ^ idx, SOME {fixes = fixes, assumes = assumes, binds = binds}) end; - in - (case Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop) of - [prop] => [extract prop ""] - | props => map2 extract props (map string_of_int (1 upto length props))) - end; - -in - -fun make is_open split (thy, prop) cases = - let - val n = length cases; - val nprems = Logic.count_prems (prop, 0); - 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 => extract_cases is_open thy sp name concls) @ cs, i - 1); - in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end; - -fun simple (thy, prop) name = - extract_cases true thy (NONE, prop) name []; - -end; - - (* params *) fun rename_params xss th =