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