src/Pure/Isar/rule_cases.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20289 ba7a7c56bed5
child 21395 f34ac19659ae
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     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, 0);
   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.tags_of_thm 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 fun consumes_default n x =
   238   if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
   239 
   240 
   241 
   242 (** case names **)
   243 
   244 val case_names_tagN = "case_names";
   245 
   246 fun add_case_names NONE = I
   247   | add_case_names (SOME names) =
   248       PureThy.untag_rule case_names_tagN
   249       #> PureThy.tag_rule (case_names_tagN, names);
   250 
   251 fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN;
   252 
   253 val save_case_names = add_case_names o lookup_case_names;
   254 val name = add_case_names o SOME;
   255 fun case_names ss = Thm.rule_attribute (K (name ss));
   256 
   257 
   258 
   259 (** case conclusions **)
   260 
   261 val case_concl_tagN = "case_conclusion";
   262 
   263 fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
   264   | is_case_concl _ _ = false;
   265 
   266 fun add_case_concl (name, cs) = PureThy.map_tags (fn tags =>
   267   filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
   268 
   269 fun get_case_concls th name =
   270   (case find_first (is_case_concl name) (Thm.tags_of_thm th) of
   271     SOME (_, _ :: cs) => cs
   272   | _ => []);
   273 
   274 fun save_case_concls th =
   275   let val concls = Thm.tags_of_thm th |> map_filter
   276     (fn (a, b :: cs) =>
   277       if a = case_concl_tagN then SOME (b, cs) else NONE
   278     | _ => NONE)
   279   in fold add_case_concl concls end;
   280 
   281 fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
   282 
   283 
   284 
   285 (** case declarations **)
   286 
   287 (* access hints *)
   288 
   289 fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
   290 
   291 fun get th =
   292   let
   293     val n = get_consumes th;
   294     val cases =
   295       (case lookup_case_names th of
   296         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
   297       | SOME names => map (fn name => (name, get_case_concls th name)) names);
   298   in (cases, n) end;
   299 
   300 
   301 (* params *)
   302 
   303 fun rename_params xss th =
   304   th
   305   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   306   |> save th;
   307 
   308 fun params xss = Thm.rule_attribute (K (rename_params xss));
   309 
   310 
   311 
   312 (** mutual_rule **)
   313 
   314 local
   315 
   316 fun equal_cterms ts us =
   317   list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us) = EQUAL;
   318 
   319 fun prep_rule n th =
   320   let
   321     val th' = Thm.permute_prems 0 n th;
   322     val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th');
   323     val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   324   in (prems, (n, th'')) end;
   325 
   326 in
   327 
   328 fun mutual_rule _ [] = NONE
   329   | mutual_rule _ [th] = SOME ([0], th)
   330   | mutual_rule ctxt (ths as th :: _) =
   331       let
   332         val ((_, ths'), ctxt') = Variable.import true ths ctxt;
   333         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
   334         val (ns, rls) = split_list (map #2 rules);
   335       in
   336         if not (forall (equal_cterms prems o #1) rules) then NONE
   337         else
   338           SOME (ns,
   339             rls
   340             |> foldr1 (uncurry Conjunction.intr)
   341             |> Drule.implies_intr_list prems
   342             |> singleton (Variable.export ctxt' ctxt)
   343             |> save th
   344             |> put_consumes (SOME 0))
   345       end;
   346 
   347 end;
   348 
   349 fun strict_mutual_rule ctxt ths =
   350   (case mutual_rule ctxt ths of
   351     NONE => error "Failed to join given rules into one mutual rule"
   352   | SOME res => res);
   353 
   354 end;
   355 
   356 structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
   357 open BasicRuleCases;