src/Pure/Isar/rule_cases.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 45375 7fe19930dfc9
child 45525 59561859c452
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
     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: (binding * typ) list,
    24     assumes: (string * term list) list,
    25     binds: (indexname * term option) list,
    26     cases: (string * T) list}
    27   val case_hypsN: string
    28   val strip_params: term -> (string * typ) list
    29   val make_common: theory * term ->
    30     ((string * string list) * string list) list -> cases
    31   val make_nested: term -> theory * term ->
    32     ((string * string list) * string list) list -> cases
    33   val apply: term list -> T -> T
    34   val consume: thm list -> thm list -> ('a * int) * thm ->
    35     (('a * (int * thm list)) * thm) Seq.seq
    36   val get_consumes: thm -> int
    37   val put_consumes: int option -> thm -> thm
    38   val add_consumes: int -> thm -> thm
    39   val default_consumes: int -> thm -> thm
    40   val consumes: int -> attribute
    41   val get_constraints: thm -> int
    42   val constraints: int -> attribute
    43   val name: string list -> thm -> thm
    44   val case_names: string list -> attribute
    45   val cases_hyp_names: string list -> string list list -> attribute
    46   val case_conclusion: string * string list -> attribute
    47   val is_inner_rule: thm -> bool
    48   val inner_rule: attribute
    49   val save: thm -> thm -> thm
    50   val get: thm -> ((string * string list) * string list) list * int
    51   val rename_params: string list list -> thm -> thm
    52   val params: string list list -> attribute
    53   val internalize_params: thm -> thm
    54   val mutual_rule: Proof.context -> thm list -> (int list * thm) option
    55   val strict_mutual_rule: Proof.context -> thm list -> int list * thm
    56 end;
    57 
    58 structure Rule_Cases: RULE_CASES =
    59 struct
    60 
    61 (** cases **)
    62 
    63 datatype T = Case of
    64  {fixes: (binding * typ) list,
    65   assumes: (string * term list) list,
    66   binds: (indexname * term option) list,
    67   cases: (string * T) list};
    68 
    69 type cases = (string * T option) list;
    70 
    71 val case_conclN = "case";
    72 val case_hypsN = "hyps";
    73 val case_premsN = "prems";
    74 
    75 val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
    76 
    77 local
    78 
    79 fun abs xs t = Term.list_abs (xs, t);
    80 fun app us t = Term.betapplys (t, us);
    81 
    82 fun dest_binops cs tm =
    83   let
    84     val n = length cs;
    85     fun dest 0 _ = []
    86       | dest 1 t = [t]
    87       | dest k (_ $ t $ u) = t :: dest (k - 1) u
    88       | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
    89   in cs ~~ dest n tm end;
    90 
    91 fun extract_fixes NONE prop = (strip_params prop, [])
    92   | extract_fixes (SOME outline) prop =
    93       chop (length (Logic.strip_params outline)) (strip_params prop);
    94 
    95 fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    96   | extract_assumes qual hnames (SOME outline) prop =
    97       let
    98         val (hyps, prems) =
    99           chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
   100         fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps);
   101         val (hyps1,hyps2) = chop (length hnames) hyps;
   102         val pairs1 = if hyps1 = [] then [] else hnames ~~ hyps1;
   103         val pairs = pairs1 @ (map (pair case_hypsN) hyps2);
   104         val named_hyps = map extract (partition_eq (eq_fst op =) pairs)
   105       in (named_hyps, [(qual case_premsN, prems)]) end;
   106 
   107 fun bindings args = map (apfst Binding.name) args;
   108 
   109 fun extract_case thy (case_outline, raw_prop) name hnames concls =
   110   let
   111     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
   112     val len = length props;
   113     val nested = is_some case_outline andalso len > 1;
   114 
   115     fun extract prop =
   116       let
   117         val (fixes1, fixes2) = extract_fixes case_outline prop;
   118         val abs_fixes = abs (fixes1 @ fixes2);
   119         fun abs_fixes1 t =
   120           if not nested then abs_fixes t
   121           else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
   122         val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
   123           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
   124 
   125         val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
   126         val binds =
   127           (case_conclN, concl) :: dest_binops concls concl
   128           |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
   129       in
   130        ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
   131         ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
   132       end;
   133 
   134     val cases = map extract props;
   135 
   136     fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
   137       Case {fixes = bindings (fixes1 @ fixes2),
   138         assumes = assumes1 @ assumes2, binds = binds, cases = []};
   139     fun inner_case (_, ((fixes2, assumes2), binds)) =
   140       Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []};
   141     fun nested_case ((fixes1, assumes1), _) =
   142       Case {fixes = bindings fixes1, assumes = assumes1, binds = [],
   143         cases = map string_of_int (1 upto len) ~~ map inner_case cases};
   144   in
   145     if len = 0 then NONE
   146     else if len = 1 then SOME (common_case (hd cases))
   147     else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
   148     else SOME (nested_case (hd cases))
   149   end;
   150 
   151 fun make rule_struct (thy, prop) cases =
   152   let
   153     val n = length cases;
   154     val nprems = Logic.count_prems prop;
   155     fun add_case ((name, hnames), concls) (cs, i) =
   156       ((case try (fn () =>
   157           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
   158         NONE => (name, NONE)
   159       | SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1);
   160   in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
   161 
   162 in
   163 
   164 val make_common = make NONE;
   165 fun make_nested rule_struct = make (SOME rule_struct);
   166 
   167 fun apply args =
   168   let
   169     fun appl (Case {fixes, assumes, binds, cases}) =
   170       let
   171         val assumes' = map (apsnd (map (app args))) assumes;
   172         val binds' = map (apsnd (Option.map (app args))) binds;
   173         val cases' = map (apsnd appl) cases;
   174       in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end;
   175   in appl end;
   176 
   177 end;
   178 
   179 
   180 
   181 (** tactics with cases **)
   182 
   183 type cases_tactic = thm -> (cases * thm) Seq.seq;
   184 
   185 fun CASES cases tac st = Seq.map (pair cases) (tac st);
   186 fun NO_CASES tac = CASES [] tac;
   187 
   188 fun SUBGOAL_CASES tac i st =
   189   (case try Logic.nth_prem (i, Thm.prop_of st) of
   190     SOME goal => tac (goal, i) st
   191   | NONE => Seq.empty);
   192 
   193 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
   194   st |> tac1 i |> Seq.maps (fn (cases, st') =>
   195     CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st');
   196 
   197 
   198 
   199 (** consume facts **)
   200 
   201 local
   202 
   203 fun unfold_prems n defs th =
   204   if null defs then th
   205   else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
   206 
   207 fun unfold_prems_concls defs th =
   208   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   209   else
   210     Conv.fconv_rule
   211       (Conv.concl_conv ~1 (Conjunction.convs
   212         (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
   213 
   214 in
   215 
   216 fun consume defs facts ((xx, n), th) =
   217   let val m = Int.min (length facts, n) in
   218     th
   219     |> unfold_prems n defs
   220     |> unfold_prems_concls defs
   221     |> Drule.multi_resolve (take m facts)
   222     |> Seq.map (pair (xx, (n - m, drop m facts)))
   223   end;
   224 
   225 end;
   226 
   227 val consumes_tagN = "consumes";
   228 
   229 fun lookup_consumes th =
   230   (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
   231     NONE => NONE
   232   | SOME s =>
   233       (case Lexicon.read_nat s of SOME n => SOME n
   234       | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
   235 
   236 fun get_consumes th = the_default 0 (lookup_consumes th);
   237 
   238 fun put_consumes NONE th = th
   239   | put_consumes (SOME n) th = th
   240       |> Thm.untag_rule consumes_tagN
   241       |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
   242 
   243 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
   244 
   245 fun default_consumes n th =
   246   if is_some (lookup_consumes th) then th else put_consumes (SOME n) th;
   247 
   248 val save_consumes = put_consumes o lookup_consumes;
   249 
   250 fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
   251 
   252 
   253 
   254 (** equality constraints **)
   255 
   256 val constraints_tagN = "constraints";
   257 
   258 fun lookup_constraints th =
   259   (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
   260     NONE => NONE
   261   | SOME s =>
   262       (case Lexicon.read_nat s of SOME n => SOME n
   263       | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
   264 
   265 fun get_constraints th = the_default 0 (lookup_constraints th);
   266 
   267 fun put_constraints NONE th = th
   268   | put_constraints (SOME n) th = th
   269       |> Thm.untag_rule constraints_tagN
   270       |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
   271 
   272 val save_constraints = put_constraints o lookup_constraints;
   273 
   274 fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
   275 
   276 
   277 
   278 (** case names **)
   279 
   280 val implode_args = space_implode ";";
   281 val explode_args = space_explode ";";
   282 
   283 val case_names_tagN = "case_names";
   284 
   285 fun add_case_names NONE = I
   286   | add_case_names (SOME names) =
   287       Thm.untag_rule case_names_tagN
   288       #> Thm.tag_rule (case_names_tagN, implode_args names);
   289 
   290 fun lookup_case_names th =
   291   AList.lookup (op =) (Thm.get_tags th) case_names_tagN
   292   |> Option.map explode_args;
   293 
   294 val save_case_names = add_case_names o lookup_case_names;
   295 val name = add_case_names o SOME;
   296 fun case_names cs = Thm.rule_attribute (K (name cs));
   297 
   298 
   299 
   300 (** hyp names **)
   301 
   302 val implode_hyps = implode_args o map (suffix "," o space_implode ",");
   303 val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
   304 
   305 val cases_hyp_names_tagN = "cases_hyp_names";
   306 
   307 fun add_cases_hyp_names NONE = I
   308   | add_cases_hyp_names (SOME namess) =
   309       Thm.untag_rule cases_hyp_names_tagN
   310       #> Thm.tag_rule (cases_hyp_names_tagN, implode_hyps namess);
   311 
   312 fun lookup_cases_hyp_names th =
   313   AList.lookup (op =) (Thm.get_tags th) cases_hyp_names_tagN
   314   |> Option.map explode_hyps;
   315 
   316 val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
   317 fun cases_hyp_names cs hs =
   318   Thm.rule_attribute (K (name cs #> add_cases_hyp_names (SOME hs)));
   319 
   320 
   321 
   322 (** case conclusions **)
   323 
   324 val case_concl_tagN = "case_conclusion";
   325 
   326 fun get_case_concl name (a, b) =
   327   if a = case_concl_tagN then
   328     (case explode_args b of c :: cs => if c = name then SOME cs else NONE)
   329   else NONE;
   330 
   331 fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
   332   filter_out (is_some o get_case_concl name) tags @
   333     [(case_concl_tagN, implode_args (name :: cs))]);
   334 
   335 fun get_case_concls th name =
   336   these (get_first (get_case_concl name) (Thm.get_tags th));
   337 
   338 fun save_case_concls th =
   339   let val concls = Thm.get_tags th |> map_filter
   340     (fn (a, b) =>
   341       if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
   342       else NONE)
   343   in fold add_case_concl concls end;
   344 
   345 fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
   346 
   347 
   348 
   349 (** inner rule **)
   350 
   351 val inner_rule_tagN = "inner_rule";
   352 
   353 fun is_inner_rule th =
   354   AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
   355 
   356 fun put_inner_rule inner =
   357   Thm.untag_rule inner_rule_tagN
   358   #> inner ? Thm.tag_rule (inner_rule_tagN, "");
   359 
   360 val save_inner_rule = put_inner_rule o is_inner_rule;
   361 
   362 val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
   363 
   364 
   365 
   366 (** case declarations **)
   367 
   368 (* access hints *)
   369 
   370 fun save th =
   371   save_consumes th #>
   372   save_constraints th #>
   373   save_case_names th #>
   374   save_cases_hyp_names th #>
   375   save_case_concls th #>
   376   save_inner_rule th;
   377 
   378 fun get th =
   379   let
   380     val n = get_consumes th;
   381     val cases =
   382       (case lookup_case_names th of
   383         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
   384       | SOME names => map (fn name => (name, get_case_concls th name)) names);
   385     val cases_hyps = (case lookup_cases_hyp_names th of
   386         NONE => replicate (length cases) []
   387       | SOME names => names);
   388     fun regroup ((name,concls),hyps) = ((name,hyps),concls)
   389   in (map regroup (cases ~~ cases_hyps), n) end;
   390 
   391 
   392 (* params *)
   393 
   394 fun rename_params xss th =
   395   th
   396   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   397   |> save th;
   398 
   399 fun params xss = Thm.rule_attribute (K (rename_params xss));
   400 
   401 
   402 (* internalize parameter names *)
   403 
   404 fun internalize_params rule =
   405   let
   406     fun rename prem =
   407       let val xs =
   408         map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
   409       in Logic.list_rename_params xs prem end;
   410     fun rename_prems prop =
   411       let val (As, C) = Logic.strip_horn prop
   412       in Logic.list_implies (map rename As, C) end;
   413   in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
   414 
   415 
   416 
   417 (** mutual_rule **)
   418 
   419 local
   420 
   421 fun equal_cterms ts us =
   422   is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
   423 
   424 fun prep_rule n th =
   425   let
   426     val th' = Thm.permute_prems 0 n th;
   427     val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th');
   428     val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   429   in (prems, (n, th'')) end;
   430 
   431 in
   432 
   433 fun mutual_rule _ [] = NONE
   434   | mutual_rule _ [th] = SOME ([0], th)
   435   | mutual_rule ctxt (ths as th :: _) =
   436       let
   437         val ((_, ths'), ctxt') = Variable.import true ths ctxt;
   438         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
   439         val (ns, rls) = split_list (map #2 rules);
   440       in
   441         if not (forall (equal_cterms prems o #1) rules) then NONE
   442         else
   443           SOME (ns,
   444             rls
   445             |> Conjunction.intr_balanced
   446             |> Drule.implies_intr_list prems
   447             |> singleton (Variable.export ctxt' ctxt)
   448             |> save th
   449             |> put_consumes (SOME 0))
   450       end;
   451 
   452 end;
   453 
   454 fun strict_mutual_rule ctxt ths =
   455   (case mutual_rule ctxt ths of
   456     NONE => error "Failed to join given rules into one mutual rule"
   457   | SOME res => res);
   458 
   459 end;
   460 
   461 structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
   462 open Basic_Rule_Cases;