src/Pure/Isar/rule_cases.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 36354 bbd742107f56
permissions -rw-r--r--
modernized structure Object_Logic;
     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: theory * term -> (string * string list) list -> cases
    29   val make_nested: 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 get_constraints: thm -> int
    38   val constraints: int -> attribute
    39   val name: string list -> thm -> thm
    40   val case_names: string list -> attribute
    41   val case_conclusion: string * string list -> attribute
    42   val is_inner_rule: thm -> bool
    43   val inner_rule: attribute
    44   val save: thm -> thm -> thm
    45   val get: thm -> (string * string list) list * int
    46   val rename_params: string list list -> thm -> thm
    47   val params: string list list -> attribute
    48   val internalize_params: thm -> thm
    49   val mutual_rule: Proof.context -> thm list -> (int list * thm) option
    50   val strict_mutual_rule: Proof.context -> thm list -> int list * thm
    51 end;
    52 
    53 structure Rule_Cases: RULE_CASES =
    54 struct
    55 
    56 (** cases **)
    57 
    58 datatype T = Case of
    59  {fixes: (string * typ) list,
    60   assumes: (string * term list) list,
    61   binds: (indexname * term option) list,
    62   cases: (string * T) list};
    63 
    64 type cases = (string * T option) list;
    65 
    66 val case_conclN = "case";
    67 val case_hypsN = "hyps";
    68 val case_premsN = "prems";
    69 
    70 val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
    71 
    72 local
    73 
    74 fun abs xs t = Term.list_abs (xs, t);
    75 fun app us t = Term.betapplys (t, us);
    76 
    77 fun dest_binops cs tm =
    78   let
    79     val n = length cs;
    80     fun dest 0 _ = []
    81       | dest 1 t = [t]
    82       | dest k (_ $ t $ u) = t :: dest (k - 1) u
    83       | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
    84   in cs ~~ dest n tm end;
    85 
    86 fun extract_fixes NONE prop = (strip_params prop, [])
    87   | extract_fixes (SOME outline) prop =
    88       chop (length (Logic.strip_params outline)) (strip_params prop);
    89 
    90 fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    91   | extract_assumes qual (SOME outline) prop =
    92       let val (hyps, prems) =
    93         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
    94       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
    95 
    96 fun extract_case thy (case_outline, raw_prop) name concls =
    97   let
    98     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
    99     val len = length props;
   100     val nested = is_some case_outline andalso len > 1;
   101 
   102     fun extract prop =
   103       let
   104         val (fixes1, fixes2) = extract_fixes case_outline prop;
   105         val abs_fixes = abs (fixes1 @ fixes2);
   106         fun abs_fixes1 t =
   107           if not nested then abs_fixes t
   108           else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
   109 
   110         val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
   111           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
   112 
   113         val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
   114         val binds =
   115           (case_conclN, concl) :: dest_binops concls concl
   116           |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
   117       in
   118        ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
   119         ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
   120       end;
   121 
   122     val cases = map extract props;
   123 
   124     fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
   125       Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
   126     fun inner_case (_, ((fixes2, assumes2), binds)) =
   127       Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
   128     fun nested_case ((fixes1, assumes1), _) =
   129       Case {fixes = fixes1, assumes = assumes1, binds = [],
   130         cases = map string_of_int (1 upto len) ~~ map inner_case cases};
   131   in
   132     if len = 0 then NONE
   133     else if len = 1 then SOME (common_case (hd cases))
   134     else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
   135     else SOME (nested_case (hd cases))
   136   end;
   137 
   138 fun make rule_struct (thy, prop) cases =
   139   let
   140     val n = length cases;
   141     val nprems = Logic.count_prems prop;
   142     fun add_case (name, concls) (cs, i) =
   143       ((case try (fn () =>
   144           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
   145         NONE => (name, NONE)
   146       | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1);
   147   in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
   148 
   149 in
   150 
   151 val make_common = make NONE;
   152 fun make_nested rule_struct = make (SOME rule_struct);
   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 Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.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     Conv.fconv_rule
   198       (Conv.concl_conv ~1 (Conjunction.convs
   199         (Conv.prems_conv ~1 (MetaSimplifier.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 (take m facts)
   209     |> Seq.map (pair (xx, (n - m, drop m facts)))
   210   end;
   211 
   212 end;
   213 
   214 val consumes_tagN = "consumes";
   215 
   216 fun lookup_consumes th =
   217   (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
   218     NONE => NONE
   219   | SOME s =>
   220       (case Lexicon.read_nat s of SOME n => SOME n
   221       | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
   222 
   223 fun get_consumes th = the_default 0 (lookup_consumes th);
   224 
   225 fun put_consumes NONE th = th
   226   | put_consumes (SOME n) th = th
   227       |> Thm.untag_rule consumes_tagN
   228       |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
   229 
   230 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
   231 
   232 val save_consumes = put_consumes o lookup_consumes;
   233 
   234 fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
   235 
   236 fun consumes_default n x =
   237   if is_some (lookup_consumes (#2 x)) then x else consumes n x;
   238 
   239 
   240 
   241 (** equality constraints **)
   242 
   243 val constraints_tagN = "constraints";
   244 
   245 fun lookup_constraints th =
   246   (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
   247     NONE => NONE
   248   | SOME s =>
   249       (case Lexicon.read_nat s of SOME n => SOME n
   250       | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
   251 
   252 fun get_constraints th = the_default 0 (lookup_constraints th);
   253 
   254 fun put_constraints NONE th = th
   255   | put_constraints (SOME n) th = th
   256       |> Thm.untag_rule constraints_tagN
   257       |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
   258 
   259 val save_constraints = put_constraints o lookup_constraints;
   260 
   261 fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
   262 
   263 
   264 
   265 (** case names **)
   266 
   267 val implode_args = space_implode ";";
   268 val explode_args = space_explode ";";
   269 
   270 val case_names_tagN = "case_names";
   271 
   272 fun add_case_names NONE = I
   273   | add_case_names (SOME names) =
   274       Thm.untag_rule case_names_tagN
   275       #> Thm.tag_rule (case_names_tagN, implode_args names);
   276 
   277 fun lookup_case_names th =
   278   AList.lookup (op =) (Thm.get_tags th) case_names_tagN
   279   |> Option.map explode_args;
   280 
   281 val save_case_names = add_case_names o lookup_case_names;
   282 val name = add_case_names o SOME;
   283 fun case_names ss = Thm.rule_attribute (K (name ss));
   284 
   285 
   286 
   287 (** case conclusions **)
   288 
   289 val case_concl_tagN = "case_conclusion";
   290 
   291 fun get_case_concl name (a, b) =
   292   if a = case_concl_tagN then
   293     (case explode_args b of c :: cs => if c = name then SOME cs else NONE)
   294   else NONE;
   295 
   296 fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
   297   filter_out (is_some o get_case_concl name) tags @
   298     [(case_concl_tagN, implode_args (name :: cs))]);
   299 
   300 fun get_case_concls th name =
   301   these (get_first (get_case_concl name) (Thm.get_tags th));
   302 
   303 fun save_case_concls th =
   304   let val concls = Thm.get_tags th |> map_filter
   305     (fn (a, b) =>
   306       if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
   307       else NONE)
   308   in fold add_case_concl concls end;
   309 
   310 fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
   311 
   312 
   313 
   314 (** inner rule **)
   315 
   316 val inner_rule_tagN = "inner_rule";
   317 
   318 fun is_inner_rule th =
   319   AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
   320 
   321 fun put_inner_rule inner =
   322   Thm.untag_rule inner_rule_tagN
   323   #> inner ? Thm.tag_rule (inner_rule_tagN, "");
   324 
   325 val save_inner_rule = put_inner_rule o is_inner_rule;
   326 
   327 val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
   328 
   329 
   330 
   331 (** case declarations **)
   332 
   333 (* access hints *)
   334 
   335 fun save th =
   336   save_consumes th #>
   337   save_constraints th #>
   338   save_case_names th #>
   339   save_case_concls th #>
   340   save_inner_rule th;
   341 
   342 fun get th =
   343   let
   344     val n = get_consumes th;
   345     val cases =
   346       (case lookup_case_names th of
   347         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
   348       | SOME names => map (fn name => (name, get_case_concls th name)) names);
   349   in (cases, n) end;
   350 
   351 
   352 (* params *)
   353 
   354 fun rename_params xss th =
   355   th
   356   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   357   |> save th;
   358 
   359 fun params xss = Thm.rule_attribute (K (rename_params xss));
   360 
   361 
   362 (* internalize parameter names *)
   363 
   364 fun internalize_params rule =
   365   let
   366     fun rename prem =
   367       let val xs =
   368         map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
   369       in Logic.list_rename_params (xs, prem) end;
   370     fun rename_prems prop =
   371       let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
   372       in Logic.list_implies (map rename As, C) end;
   373   in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
   374 
   375 
   376 
   377 (** mutual_rule **)
   378 
   379 local
   380 
   381 fun equal_cterms ts us =
   382   is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
   383 
   384 fun prep_rule n th =
   385   let
   386     val th' = Thm.permute_prems 0 n th;
   387     val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th');
   388     val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   389   in (prems, (n, th'')) end;
   390 
   391 in
   392 
   393 fun mutual_rule _ [] = NONE
   394   | mutual_rule _ [th] = SOME ([0], th)
   395   | mutual_rule ctxt (ths as th :: _) =
   396       let
   397         val ((_, ths'), ctxt') = Variable.import true ths ctxt;
   398         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
   399         val (ns, rls) = split_list (map #2 rules);
   400       in
   401         if not (forall (equal_cterms prems o #1) rules) then NONE
   402         else
   403           SOME (ns,
   404             rls
   405             |> Conjunction.intr_balanced
   406             |> Drule.implies_intr_list prems
   407             |> singleton (Variable.export ctxt' ctxt)
   408             |> save th
   409             |> put_consumes (SOME 0))
   410       end;
   411 
   412 end;
   413 
   414 fun strict_mutual_rule ctxt ths =
   415   (case mutual_rule ctxt ths of
   416     NONE => error "Failed to join given rules into one mutual rule"
   417   | SOME res => res);
   418 
   419 end;
   420 
   421 structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
   422 open Basic_Rule_Cases;