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