src/Pure/Isar/rule_cases.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 21646 c07b5b0e8492
child 21708 45e7491bea47
permissions -rw-r--r--
Attrib.internal: morphism;
     1 (*  Title:      Pure/Isar/rule_cases.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Annotations and local contexts of rules.
     6 *)
     7 
     8 infix 1 THEN_ALL_NEW_CASES;
     9 
    10 signature BASIC_RULE_CASES =
    11 sig
    12   type cases
    13   type cases_tactic
    14   val CASES: cases -> tactic -> cases_tactic
    15   val NO_CASES: tactic -> cases_tactic
    16   val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
    17   val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
    18 end
    19 
    20 signature RULE_CASES =
    21 sig
    22   include BASIC_RULE_CASES
    23   datatype T = Case of
    24    {fixes: (string * typ) list,
    25     assumes: (string * term list) list,
    26     binds: (indexname * term option) list,
    27     cases: (string * T) list}
    28   val strip_params: term -> (string * typ) list
    29   val make_common: bool -> theory * term -> (string * string list) list -> cases
    30   val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases
    31   val make_simple: bool -> theory * term -> string -> cases
    32   val apply: term list -> T -> T
    33   val consume: thm list -> thm list -> ('a * int) * thm ->
    34     (('a * (int * thm list)) * thm) Seq.seq
    35   val add_consumes: int -> thm -> thm
    36   val consumes: int -> attribute
    37   val consumes_default: int -> attribute
    38   val name: string list -> thm -> thm
    39   val case_names: string list -> attribute
    40   val case_conclusion: string * string list -> attribute
    41   val save: thm -> thm -> thm
    42   val get: thm -> (string * string list) list * int
    43   val rename_params: string list list -> thm -> thm
    44   val params: string list list -> attribute
    45   val mutual_rule: Proof.context -> thm list -> (int list * thm) option
    46   val strict_mutual_rule: Proof.context -> thm list -> int list * thm
    47 end;
    48 
    49 structure RuleCases: RULE_CASES =
    50 struct
    51 
    52 (** cases **)
    53 
    54 datatype T = Case of
    55  {fixes: (string * typ) list,
    56   assumes: (string * term list) list,
    57   binds: (indexname * term option) list,
    58   cases: (string * T) list};
    59 
    60 type cases = (string * T option) list;
    61 
    62 val case_conclN = "case";
    63 val case_hypsN = "hyps";
    64 val case_premsN = "prems";
    65 
    66 val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
    67 
    68 local
    69 
    70 fun abs xs t = Term.list_abs (xs, t);
    71 fun app us t = Term.betapplys (t, us);
    72 
    73 fun dest_binops cs tm =
    74   let
    75     val n = length cs;
    76     fun dest 0 _ = []
    77       | dest 1 t = [t]
    78       | dest k (_ $ t $ u) = t :: dest (k - 1) u
    79       | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
    80   in cs ~~ dest n tm end;
    81 
    82 fun extract_fixes NONE prop = (strip_params prop, [])
    83   | extract_fixes (SOME outline) prop =
    84       chop (length (Logic.strip_params outline)) (strip_params prop);
    85 
    86 fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    87   | extract_assumes qual (SOME outline) prop =
    88       let val (hyps, prems) =
    89         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
    90       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
    91 
    92 fun extract_case is_open thy (case_outline, raw_prop) name concls =
    93   let
    94     val rename = if is_open then I else (apfst Name.internal);
    95 
    96     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
    97     val len = length props;
    98     val nested = is_some case_outline andalso len > 1;
    99 
   100     fun extract prop =
   101       let
   102         val (fixes1, fixes2) = extract_fixes case_outline prop
   103           |> apfst (map rename);
   104         val abs_fixes = abs (fixes1 @ fixes2);
   105         fun abs_fixes1 t =
   106           if not nested then abs_fixes t
   107           else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
   108 
   109         val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop
   110           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
   111 
   112         val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
   113         val binds =
   114           (case_conclN, concl) :: dest_binops concls concl
   115           |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
   116       in
   117        ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
   118         ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
   119       end;
   120 
   121     val cases = map extract props;
   122 
   123     fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
   124       Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
   125     fun inner_case (_, ((fixes2, assumes2), binds)) =
   126       Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
   127     fun nested_case ((fixes1, assumes1), _) =
   128       Case {fixes = fixes1, assumes = assumes1, binds = [],
   129         cases = map string_of_int (1 upto len) ~~ map inner_case cases};
   130   in
   131     if len = 0 then NONE
   132     else if len = 1 then SOME (common_case (hd cases))
   133     else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
   134     else SOME (nested_case (hd cases))
   135   end;
   136 
   137 fun make is_open rule_struct (thy, prop) cases =
   138   let
   139     val n = length cases;
   140     val nprems = Logic.count_prems prop;
   141     fun add_case (name, concls) (cs, i) =
   142       ((case try (fn () =>
   143           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
   144         NONE => (name, NONE)
   145       | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
   146   in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
   147 
   148 in
   149 
   150 fun make_common is_open = make is_open NONE;
   151 fun make_nested is_open rule_struct = make is_open (SOME rule_struct);
   152 fun make_simple is_open (thy, prop) name = [(name, extract_case is_open thy (NONE, prop) "" [])];
   153 
   154 fun apply args =
   155   let
   156     fun appl (Case {fixes, assumes, binds, cases}) =
   157       let
   158         val assumes' = map (apsnd (map (app args))) assumes;
   159         val binds' = map (apsnd (Option.map (app args))) binds;
   160         val cases' = map (apsnd appl) cases;
   161       in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end;
   162   in appl end;
   163 
   164 end;
   165 
   166 
   167 
   168 (** tactics with cases **)
   169 
   170 type cases_tactic = thm -> (cases * thm) Seq.seq;
   171 
   172 fun CASES cases tac st = Seq.map (pair cases) (tac st);
   173 fun NO_CASES tac = CASES [] tac;
   174 
   175 fun SUBGOAL_CASES tac i st =
   176   (case try Logic.nth_prem (i, Thm.prop_of st) of
   177     SOME goal => tac (goal, i) st
   178   | NONE => Seq.empty);
   179 
   180 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
   181   st |> tac1 i |> Seq.maps (fn (cases, st') =>
   182     CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st');
   183 
   184 
   185 
   186 (** consume facts **)
   187 
   188 local
   189 
   190 fun unfold_prems n defs th =
   191   if null defs then th
   192   else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th;
   193 
   194 fun unfold_prems_concls defs th =
   195   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   196   else
   197     Drule.fconv_rule
   198       (Drule.concl_conv ~1 (Conjunction.conv ~1
   199         (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
   200 
   201 in
   202 
   203 fun consume defs facts ((xx, n), th) =
   204   let val m = Int.min (length facts, n) in
   205     th
   206     |> unfold_prems n defs
   207     |> unfold_prems_concls defs
   208     |> Drule.multi_resolve (Library.take (m, facts))
   209     |> Seq.map (pair (xx, (n - m, Library.drop (m, facts))))
   210   end;
   211 
   212 end;
   213 
   214 val consumes_tagN = "consumes";
   215 
   216 fun lookup_consumes th =
   217   let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in
   218     (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
   219       NONE => NONE
   220     | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
   221     | _ => err ())
   222   end;
   223 
   224 fun get_consumes th = the_default 0 (lookup_consumes th);
   225 
   226 fun put_consumes NONE th = th
   227   | put_consumes (SOME n) th = th
   228       |> PureThy.untag_rule consumes_tagN
   229       |> PureThy.tag_rule
   230         (consumes_tagN, [Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n)]);
   231 
   232 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
   233 
   234 val save_consumes = put_consumes o lookup_consumes;
   235 
   236 fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
   237 
   238 fun consumes_default n x =
   239   if is_some (lookup_consumes (#2 x)) then x else consumes n x;
   240 
   241 
   242 
   243 (** case names **)
   244 
   245 val case_names_tagN = "case_names";
   246 
   247 fun add_case_names NONE = I
   248   | add_case_names (SOME names) =
   249       PureThy.untag_rule case_names_tagN
   250       #> PureThy.tag_rule (case_names_tagN, names);
   251 
   252 fun lookup_case_names th = AList.lookup (op =) (Thm.get_tags th) case_names_tagN;
   253 
   254 val save_case_names = add_case_names o lookup_case_names;
   255 val name = add_case_names o SOME;
   256 fun case_names ss = Thm.rule_attribute (K (name ss));
   257 
   258 
   259 
   260 (** case conclusions **)
   261 
   262 val case_concl_tagN = "case_conclusion";
   263 
   264 fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
   265   | is_case_concl _ _ = false;
   266 
   267 fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
   268   filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
   269 
   270 fun get_case_concls th name =
   271   (case find_first (is_case_concl name) (Thm.get_tags th) of
   272     SOME (_, _ :: cs) => cs
   273   | _ => []);
   274 
   275 fun save_case_concls th =
   276   let val concls = Thm.get_tags th |> map_filter
   277     (fn (a, b :: cs) =>
   278       if a = case_concl_tagN then SOME (b, cs) else NONE
   279     | _ => NONE)
   280   in fold add_case_concl concls end;
   281 
   282 fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
   283 
   284 
   285 
   286 (** case declarations **)
   287 
   288 (* access hints *)
   289 
   290 fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
   291 
   292 fun get th =
   293   let
   294     val n = get_consumes th;
   295     val cases =
   296       (case lookup_case_names th of
   297         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
   298       | SOME names => map (fn name => (name, get_case_concls th name)) names);
   299   in (cases, n) end;
   300 
   301 
   302 (* params *)
   303 
   304 fun rename_params xss th =
   305   th
   306   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   307   |> save th;
   308 
   309 fun params xss = Thm.rule_attribute (K (rename_params xss));
   310 
   311 
   312 
   313 (** mutual_rule **)
   314 
   315 local
   316 
   317 fun equal_cterms ts us =
   318   list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us) = EQUAL;
   319 
   320 fun prep_rule n th =
   321   let
   322     val th' = Thm.permute_prems 0 n th;
   323     val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th');
   324     val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   325   in (prems, (n, th'')) end;
   326 
   327 in
   328 
   329 fun mutual_rule _ [] = NONE
   330   | mutual_rule _ [th] = SOME ([0], th)
   331   | mutual_rule ctxt (ths as th :: _) =
   332       let
   333         val ((_, ths'), ctxt') = Variable.import true ths ctxt;
   334         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
   335         val (ns, rls) = split_list (map #2 rules);
   336       in
   337         if not (forall (equal_cterms prems o #1) rules) then NONE
   338         else
   339           SOME (ns,
   340             rls
   341             |> foldr1 (uncurry Conjunction.intr)
   342             |> Drule.implies_intr_list prems
   343             |> singleton (Variable.export ctxt' ctxt)
   344             |> save th
   345             |> put_consumes (SOME 0))
   346       end;
   347 
   348 end;
   349 
   350 fun strict_mutual_rule ctxt ths =
   351   (case mutual_rule ctxt ths of
   352     NONE => error "Failed to join given rules into one mutual rule"
   353   | SOME res => res);
   354 
   355 end;
   356 
   357 structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
   358 open BasicRuleCases;