# HG changeset patch # User wenzelm # Date 1135207749 -3600 # Node ID bf2a02c82a55a4e51fdcca4d5d25cb51227ed01c # Parent 49dde7b7b14a0aaf051f1cb69ba0d53ba2473cbf consume: expand defs in prems of concls; added add_consumes; make/extract_cases: split cases consisting of meta-conjunctions; added mutual_rule; diff -r 49dde7b7b14a -r bf2a02c82a55 src/Pure/Isar/rule_cases.ML --- 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;