--- a/src/Pure/Isar/rule_cases.ML Thu Dec 22 00:29:08 2005 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Dec 22 00:29:09 2005 +0100
@@ -23,6 +23,7 @@
type T
val consume: thm list -> thm list -> ('a * int) * thm ->
(('a * (int * thm list)) * thm) Seq.seq
+ val add_consumes: int -> thm -> thm
val consumes: int -> 'a attribute
val consumes_default: int -> 'a attribute
val name: string list -> thm -> thm
@@ -32,9 +33,10 @@
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: bool -> theory * term -> string -> string * T option
+ 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
end;
structure RuleCases: RULE_CASES =
@@ -66,14 +68,32 @@
(** consume facts **)
-fun consume defs facts ((cases, n), th) =
+local
+
+fun unfold_prems n defs th =
+ if null defs then th
+ else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th;
+
+fun unfold_prems_concls defs th =
+ if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
+ else
+ Drule.fconv_rule
+ (Drule.concl_conv ~1 (Drule.conjunction_conv ~1
+ (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
+
+in
+
+fun consume defs facts ((xx, n), th) =
let val m = Int.min (length facts, n) in
- th |> K (not (null defs)) ?
- Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs))
+ th
+ |> unfold_prems n defs
+ |> unfold_prems_concls defs
|> Drule.multi_resolve (Library.take (m, facts))
- |> Seq.map (pair (cases, (n - m, Library.drop (m, facts))))
+ |> Seq.map (pair (xx, (n - m, Library.drop (m, facts))))
end;
+end;
+
val consumes_tagN = "consumes";
fun lookup_consumes th =
@@ -84,11 +104,15 @@
| _ => err ())
end;
+fun get_consumes th = the_default 0 (lookup_consumes th);
+
fun put_consumes NONE th = th
| put_consumes (SOME n) th = th
|> Drule.untag_rule consumes_tagN
|> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
+fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
+
val save_consumes = put_consumes o lookup_consumes;
fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
@@ -148,7 +172,7 @@
fun get th =
let
- val n = the_default 0 (lookup_consumes th);
+ val n = get_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))
@@ -164,6 +188,8 @@
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;
@@ -173,32 +199,42 @@
| dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
in cs ~~ dest n tm end;
-fun extract_case is_open thy (split, raw_prop) name concls =
+fun extract_cases is_open thy (split, raw_prop) name concls =
let
- val prop = Drule.norm_hhf thy raw_prop;
+ 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 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 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 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 = 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;
- 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 {fixes = fixes, assumes = assumes, binds = binds} end;
+in
fun make is_open split (thy, prop) cases =
let
@@ -207,12 +243,14 @@
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 => (name, SOME (extract_case is_open thy sp name concls))) :: cs, i - 1);
+ 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 is_open (thy, prop) name =
- (name, SOME (extract_case is_open thy (NONE, prop) name []));
+fun simple (thy, prop) name =
+ extract_cases true thy (NONE, prop) name [];
+
+end;
(* params *)
@@ -224,6 +262,45 @@
fun params xss = Drule.rule_attribute (K (rename_params xss));
+
+
+(** mutual_rule **)
+
+local
+
+fun equal_cterms ts us =
+ list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us) = EQUAL;
+
+fun prep_rule th =
+ let
+ val n = get_consumes th;
+ val th' = Drule.freeze_all (Thm.permute_prems 0 n th);
+ val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th');
+ val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
+ in (prems, (n, th'')) end;
+
+in
+
+fun mutual_rule [] = NONE
+ | mutual_rule [th] = SOME ([0], th)
+ | mutual_rule raw_rules =
+ let
+ val rules as (prems, _) :: _ = map prep_rule raw_rules;
+ val (ns, ths) = split_list (map #2 rules);
+ in
+ if not (forall (equal_cterms prems o #1) rules) then NONE
+ else
+ SOME (ns,
+ ths
+ |> foldr1 (uncurry Drule.conj_intr)
+ |> Drule.implies_intr_list prems
+ |> Drule.standard'
+ |> save (hd raw_rules)
+ |> put_consumes (SOME 0))
+ end;
+
+end;
+
end;
structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;