src/Pure/Isar/rule_cases.ML
author haftmann
Tue Nov 24 17:28:25 2009 +0100 (2009-11-24)
changeset 33955 fff6f11b1f09
parent 33368 b1cf34f1855c
child 33957 e9afca2118d4
permissions -rw-r--r--
curried take/drop
     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 is_inner_rule: thm -> bool
    41   val inner_rule: attribute
    42   val save: thm -> thm -> thm
    43   val get: thm -> (string * string list) list * int
    44   val rename_params: string list list -> thm -> thm
    45   val params: string list list -> attribute
    46   val mutual_rule: Proof.context -> thm list -> (int list * thm) option
    47   val strict_mutual_rule: Proof.context -> thm list -> int list * thm
    48 end;
    49 
    50 structure Rule_Cases: RULE_CASES =
    51 struct
    52 
    53 (** cases **)
    54 
    55 datatype T = Case of
    56  {fixes: (string * typ) list,
    57   assumes: (string * term list) list,
    58   binds: (indexname * term option) list,
    59   cases: (string * T) list};
    60 
    61 type cases = (string * T option) list;
    62 
    63 val case_conclN = "case";
    64 val case_hypsN = "hyps";
    65 val case_premsN = "prems";
    66 
    67 val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
    68 
    69 local
    70 
    71 fun abs xs t = Term.list_abs (xs, t);
    72 fun app us t = Term.betapplys (t, us);
    73 
    74 fun dest_binops cs tm =
    75   let
    76     val n = length cs;
    77     fun dest 0 _ = []
    78       | dest 1 t = [t]
    79       | dest k (_ $ t $ u) = t :: dest (k - 1) u
    80       | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
    81   in cs ~~ dest n tm end;
    82 
    83 fun extract_fixes NONE prop = (strip_params prop, [])
    84   | extract_fixes (SOME outline) prop =
    85       chop (length (Logic.strip_params outline)) (strip_params prop);
    86 
    87 fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    88   | extract_assumes qual (SOME outline) prop =
    89       let val (hyps, prems) =
    90         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
    91       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
    92 
    93 fun extract_case is_open thy (case_outline, raw_prop) name concls =
    94   let
    95     val rename = if is_open then I else apfst (Name.internal o Name.clean);
    96 
    97     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
    98     val len = length props;
    99     val nested = is_some case_outline andalso len > 1;
   100 
   101     fun extract prop =
   102       let
   103         val (fixes1, fixes2) = extract_fixes case_outline prop
   104           |> apfst (map rename);
   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 = ObjectLogic.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 is_open 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 is_open thy p name concls)) :: cs, i - 1);
   147   in fold_rev add_case ((uncurry drop) (n - nprems, cases)) ([], n) |> #1 end;
   148 
   149 in
   150 
   151 fun make_common is_open = make is_open NONE;
   152 fun make_nested is_open rule_struct = make is_open (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 ((uncurry take) (m, facts))
   209     |> Seq.map (pair (xx, (n - m, (uncurry 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 (** case names **)
   242 
   243 val implode_args = space_implode ";";
   244 val explode_args = space_explode ";";
   245 
   246 val case_names_tagN = "case_names";
   247 
   248 fun add_case_names NONE = I
   249   | add_case_names (SOME names) =
   250       Thm.untag_rule case_names_tagN
   251       #> Thm.tag_rule (case_names_tagN, implode_args names);
   252 
   253 fun lookup_case_names th =
   254   AList.lookup (op =) (Thm.get_tags th) case_names_tagN
   255   |> Option.map explode_args;
   256 
   257 val save_case_names = add_case_names o lookup_case_names;
   258 val name = add_case_names o SOME;
   259 fun case_names ss = Thm.rule_attribute (K (name ss));
   260 
   261 
   262 
   263 (** case conclusions **)
   264 
   265 val case_concl_tagN = "case_conclusion";
   266 
   267 fun get_case_concl name (a, b) =
   268   if a = case_concl_tagN then
   269     (case explode_args b of c :: cs => if c = name then SOME cs else NONE)
   270   else NONE;
   271 
   272 fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
   273   filter_out (is_some o get_case_concl name) tags @
   274     [(case_concl_tagN, implode_args (name :: cs))]);
   275 
   276 fun get_case_concls th name =
   277   these (get_first (get_case_concl name) (Thm.get_tags th));
   278 
   279 fun save_case_concls th =
   280   let val concls = Thm.get_tags th |> map_filter
   281     (fn (a, b) =>
   282       if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
   283       else NONE)
   284   in fold add_case_concl concls end;
   285 
   286 fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
   287 
   288 
   289 
   290 (** inner rule **)
   291 
   292 val inner_rule_tagN = "inner_rule";
   293 
   294 fun is_inner_rule th =
   295   AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
   296 
   297 fun put_inner_rule inner =
   298   Thm.untag_rule inner_rule_tagN
   299   #> inner ? Thm.tag_rule (inner_rule_tagN, "");
   300 
   301 val save_inner_rule = put_inner_rule o is_inner_rule;
   302 
   303 val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
   304 
   305 
   306 
   307 (** case declarations **)
   308 
   309 (* access hints *)
   310 
   311 fun save th =
   312   save_consumes th #>
   313   save_case_names th #>
   314   save_case_concls th #>
   315   save_inner_rule th;
   316 
   317 fun get th =
   318   let
   319     val n = get_consumes th;
   320     val cases =
   321       (case lookup_case_names th of
   322         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
   323       | SOME names => map (fn name => (name, get_case_concls th name)) names);
   324   in (cases, n) end;
   325 
   326 
   327 (* params *)
   328 
   329 fun rename_params xss th =
   330   th
   331   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   332   |> save th;
   333 
   334 fun params xss = Thm.rule_attribute (K (rename_params xss));
   335 
   336 
   337 
   338 (** mutual_rule **)
   339 
   340 local
   341 
   342 fun equal_cterms ts us =
   343   is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
   344 
   345 fun prep_rule n th =
   346   let
   347     val th' = Thm.permute_prems 0 n th;
   348     val prems = (uncurry take) (Thm.nprems_of th' - n, Drule.cprems_of th');
   349     val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   350   in (prems, (n, th'')) end;
   351 
   352 in
   353 
   354 fun mutual_rule _ [] = NONE
   355   | mutual_rule _ [th] = SOME ([0], th)
   356   | mutual_rule ctxt (ths as th :: _) =
   357       let
   358         val ((_, ths'), ctxt') = Variable.import true ths ctxt;
   359         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
   360         val (ns, rls) = split_list (map #2 rules);
   361       in
   362         if not (forall (equal_cterms prems o #1) rules) then NONE
   363         else
   364           SOME (ns,
   365             rls
   366             |> Conjunction.intr_balanced
   367             |> Drule.implies_intr_list prems
   368             |> singleton (Variable.export ctxt' ctxt)
   369             |> save th
   370             |> put_consumes (SOME 0))
   371       end;
   372 
   373 end;
   374 
   375 fun strict_mutual_rule ctxt ths =
   376   (case mutual_rule ctxt ths of
   377     NONE => error "Failed to join given rules into one mutual rule"
   378   | SOME res => res);
   379 
   380 end;
   381 
   382 structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
   383 open Basic_Rule_Cases;