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