--- 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 =