src/HOL/Tools/coinduction.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59970 e9f73d87d904
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
     1 (*  Title:      HOL/Tools/coinduction.ML
     2     Author:     Johannes Hölzl, TU Muenchen
     3     Author:     Dmitriy Traytel, TU Muenchen
     4     Copyright   2013
     5 
     6 Coinduction method that avoids some boilerplate compared to coinduct.
     7 *)
     8 
     9 signature COINDUCTION =
    10 sig
    11   val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
    12 end;
    13 
    14 structure Coinduction : COINDUCTION =
    15 struct
    16 
    17 fun filter_in_out _ [] = ([], [])
    18   | filter_in_out P (x :: xs) =
    19       let
    20         val (ins, outs) = filter_in_out P xs;
    21       in
    22         if P x then (x :: ins, outs) else (ins, x :: outs)
    23       end;
    24 
    25 fun ALLGOALS_SKIP skip tac st =
    26   let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
    27   in doall (Thm.nprems_of st) st  end;
    28 
    29 fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
    30   st |> (tac1 i THEN (fn st' =>
    31     Seq.INTERVAL tac2 (i + skip) (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
    32 
    33 fun DELETE_PREMS_AFTER skip tac i st =
    34   let
    35     val n = nth (Thm.prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
    36   in
    37     (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
    38   end;
    39 
    40 fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
    41   let
    42     val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
    43     fun find_coinduct t =
    44       Induct.find_coinductP ctxt t @
    45       (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
    46     val raw_thm =
    47       (case opt_raw_thm of
    48         SOME raw_thm => raw_thm
    49       | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
    50     val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
    51     val cases = Rule_Cases.get raw_thm |> fst
    52   in
    53     HEADGOAL (
    54       Object_Logic.rulify_tac ctxt THEN'
    55       Method.insert_tac prems THEN'
    56       Object_Logic.atomize_prems_tac ctxt THEN'
    57       DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
    58         let
    59           val vars = raw_vars @ map (Thm.term_of o snd) params;
    60           val names_ctxt = ctxt
    61             |> fold Variable.declare_names vars
    62             |> fold Variable.declare_thm (raw_thm :: prems);
    63           val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    64           val (rhoTs, rhots) = Thm.match (thm_concl, concl)
    65             |>> map (apply2 Thm.typ_of)
    66             ||> map (apply2 Thm.term_of);
    67           val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
    68             |> map (subst_atomic_types rhoTs);
    69           val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
    70           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
    71             |>> (fn names => Variable.variant_fixes names names_ctxt) ;
    72           val eqs =
    73             @{map 3} (fn name => fn T => fn (_, rhs) =>
    74               HOLogic.mk_eq (Free (name, T), rhs))
    75             names Ts raw_eqs;
    76           val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
    77             |> try (Library.foldr1 HOLogic.mk_conj)
    78             |> the_default @{term True}
    79             |> Ctr_Sugar_Util.list_exists_free vars
    80             |> Term.map_abs_vars (Variable.revert_fixed ctxt)
    81             |> fold_rev Term.absfree (names ~~ Ts)
    82             |> Thm.cterm_of ctxt;
    83           val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
    84           val e = length eqs;
    85           val p = length prems;
    86         in
    87           HEADGOAL (EVERY' [resolve_tac ctxt [thm],
    88             EVERY' (map (fn var =>
    89               resolve_tac ctxt
    90                 [Ctr_Sugar_Util.cterm_instantiate_pos
    91                   [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
    92             if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
    93             else
    94               REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
    95               Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
    96             K (ALLGOALS_SKIP skip
    97                (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
    98                DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
    99                  (case prems of
   100                    [] => all_tac
   101                  | inv::case_prems =>
   102                      let
   103                        val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
   104                        val inv_thms = init @ [last];
   105                        val eqs = take e inv_thms;
   106                        fun is_local_var t =
   107                          member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
   108                         val (eqs, assms') =
   109                           filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
   110                         val assms = assms' @ drop e inv_thms
   111                       in
   112                         HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
   113                         Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
   114                       end)) ctxt)))])
   115         end) ctxt) THEN'
   116       K (prune_params_tac ctxt))
   117     #> Seq.maps (fn st =>
   118       CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
   119   end));
   120 
   121 local
   122 
   123 val ruleN = "rule"
   124 val arbitraryN = "arbitrary"
   125 fun single_rule [rule] = rule
   126   | single_rule _ = error "Single rule expected";
   127 
   128 fun named_rule k arg get =
   129   Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
   130     (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
   131       (case get (Context.proof_of context) name of SOME x => x
   132       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   133 
   134 fun rule get_type get_pred =
   135   named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
   136   named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
   137   named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
   138   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   139 
   140 val coinduct_rule =
   141   rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
   142 
   143 fun unless_more_args scan = Scan.unless (Scan.lift
   144   ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
   145     Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
   146 
   147 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   148   Scan.repeat1 (unless_more_args Args.term)) [];
   149 
   150 in
   151 
   152 val _ =
   153   Theory.setup
   154     (Method.setup @{binding coinduction}
   155       (arbitrary -- Scan.option coinduct_rule >>
   156         (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
   157           Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
   158       "coinduction on types or predicates/sets");
   159 
   160 end;
   161 
   162 end;
   163