src/HOL/Tools/coinduction.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63715 ad2c003782f9
child 67149 e61557884799
permissions -rw-r--r--
tuned;
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@63709
    11
  val coinduction_context_tactic: term list -> thm list option -> thm list -> int -> context_tactic
traytel@63709
    12
  val coinduction_tac: Proof.context -> term list -> thm list option -> thm list -> int -> tactic
traytel@54026
    13
end;
traytel@54026
    14
traytel@54026
    15
structure Coinduction : COINDUCTION =
traytel@54026
    16
struct
traytel@54026
    17
traytel@54026
    18
fun filter_in_out _ [] = ([], [])
wenzelm@58814
    19
  | filter_in_out P (x :: xs) =
wenzelm@58814
    20
      let
wenzelm@58814
    21
        val (ins, outs) = filter_in_out P xs;
wenzelm@58814
    22
      in
wenzelm@58814
    23
        if P x then (x :: ins, outs) else (ins, x :: outs)
wenzelm@58814
    24
      end;
traytel@54026
    25
traytel@54026
    26
fun ALLGOALS_SKIP skip tac st =
traytel@54026
    27
  let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
wenzelm@59582
    28
  in doall (Thm.nprems_of st) st  end;
traytel@54026
    29
traytel@54026
    30
fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
traytel@54026
    31
  st |> (tac1 i THEN (fn st' =>
wenzelm@59582
    32
    Seq.INTERVAL tac2 (i + skip) (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
traytel@54026
    33
traytel@54026
    34
fun DELETE_PREMS_AFTER skip tac i st =
traytel@54026
    35
  let
wenzelm@59582
    36
    val n = nth (Thm.prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
traytel@54026
    37
  in
wenzelm@59498
    38
    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
traytel@54026
    39
  end;
traytel@54026
    40
traytel@63709
    41
fun coinduction_context_tactic raw_vars opt_raw_thms prems =
wenzelm@61841
    42
  CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
wenzelm@61841
    43
    let
wenzelm@61841
    44
      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
wenzelm@61841
    45
      fun find_coinduct t =
wenzelm@61841
    46
        Induct.find_coinductP ctxt t @
wenzelm@61841
    47
        (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []);
traytel@63709
    48
      val raw_thms =
traytel@63709
    49
        (case opt_raw_thms of
traytel@63709
    50
          SOME raw_thms => raw_thms
traytel@63709
    51
        | NONE => goal |> Logic.strip_assums_concl |> find_coinduct);
traytel@63709
    52
      val thy = Proof_Context.theory_of ctxt;
traytel@63715
    53
      val concl = Variable.focus NONE goal ctxt |> fst |> snd |> Logic.strip_imp_concl;
traytel@63709
    54
      val raw_thm = (case find_first (fn thm =>
traytel@63709
    55
            Pattern.matches thy (Thm.concl_of thm, concl)) raw_thms of
traytel@63709
    56
          SOME thm => thm
traytel@63709
    57
        | NONE => error "No matching coinduction rule found")
wenzelm@61841
    58
      val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1;
wenzelm@61841
    59
      val cases = Rule_Cases.get raw_thm |> fst;
wenzelm@61841
    60
    in
wenzelm@61841
    61
      ((Object_Logic.rulify_tac ctxt THEN'
wenzelm@61841
    62
        Method.insert_tac ctxt prems THEN'
wenzelm@61841
    63
        Object_Logic.atomize_prems_tac ctxt THEN'
wenzelm@61841
    64
        DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
wenzelm@61841
    65
          let
wenzelm@61841
    66
            val vars = raw_vars @ map (Thm.term_of o snd) params;
wenzelm@61841
    67
            val names_ctxt = ctxt
wenzelm@61841
    68
              |> fold Variable.declare_names vars
wenzelm@61841
    69
              |> fold Variable.declare_thm (raw_thm :: prems);
wenzelm@61841
    70
            val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
wenzelm@61841
    71
            val (instT, inst) = Thm.match (thm_concl, concl);
wenzelm@61841
    72
            val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
wenzelm@61841
    73
            val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
wenzelm@61841
    74
            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
wenzelm@61841
    75
              |> map (subst_atomic_types rhoTs);
wenzelm@61841
    76
            val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
wenzelm@61841
    77
            val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
wenzelm@61841
    78
              |>> (fn names => Variable.variant_fixes names names_ctxt) ;
wenzelm@61841
    79
            val eqs =
wenzelm@61841
    80
              @{map 3} (fn name => fn T => fn (_, rhs) =>
wenzelm@61841
    81
                HOLogic.mk_eq (Free (name, T), rhs))
wenzelm@61841
    82
              names Ts raw_eqs;
wenzelm@61841
    83
            val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
wenzelm@61841
    84
              |> try (Library.foldr1 HOLogic.mk_conj)
wenzelm@61841
    85
              |> the_default @{term True}
wenzelm@61841
    86
              |> Ctr_Sugar_Util.list_exists_free vars
wenzelm@61841
    87
              |> Term.map_abs_vars (Variable.revert_fixed ctxt)
wenzelm@61841
    88
              |> fold_rev Term.absfree (names ~~ Ts)
wenzelm@61841
    89
              |> Thm.cterm_of ctxt;
wenzelm@61841
    90
            val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
wenzelm@61841
    91
            val e = length eqs;
wenzelm@61841
    92
            val p = length prems;
wenzelm@61841
    93
          in
wenzelm@61841
    94
            HEADGOAL (EVERY' [resolve_tac ctxt [thm],
wenzelm@61841
    95
              EVERY' (map (fn var =>
wenzelm@61841
    96
                resolve_tac ctxt
wenzelm@61841
    97
                  [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
wenzelm@61841
    98
              if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
wenzelm@61841
    99
              else
wenzelm@61841
   100
                REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
wenzelm@61841
   101
                Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
wenzelm@61841
   102
              K (ALLGOALS_SKIP skip
wenzelm@61841
   103
                 (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
wenzelm@61841
   104
                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
wenzelm@61841
   105
                   (case prems of
wenzelm@61841
   106
                     [] => all_tac
wenzelm@61841
   107
                   | inv :: case_prems =>
wenzelm@61841
   108
                       let
wenzelm@61841
   109
                         val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
wenzelm@61841
   110
                         val inv_thms = init @ [last];
wenzelm@61841
   111
                         val eqs = take e inv_thms;
wenzelm@61841
   112
                         fun is_local_var t =
wenzelm@61841
   113
                           member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
wenzelm@61841
   114
                          val (eqs, assms') =
wenzelm@61841
   115
                            filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
wenzelm@61841
   116
                          val assms = assms' @ drop e inv_thms
wenzelm@61841
   117
                        in
wenzelm@61841
   118
                          HEADGOAL (Method.insert_tac ctxt (assms @ case_prems)) THEN
wenzelm@61841
   119
                          Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
wenzelm@61841
   120
                        end)) ctxt)))])
wenzelm@61841
   121
          end) ctxt) THEN'
wenzelm@61841
   122
        K (prune_params_tac ctxt)) i) st
wenzelm@61841
   123
      |> Seq.maps (fn st' =>
wenzelm@61841
   124
        CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
wenzelm@61841
   125
    end);
traytel@54026
   126
wenzelm@61844
   127
fun coinduction_tac ctxt x1 x2 x3 x4 =
wenzelm@61844
   128
  Method.NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
wenzelm@61844
   129
wenzelm@61844
   130
traytel@54026
   131
local
traytel@54026
   132
traytel@54026
   133
val ruleN = "rule"
traytel@54026
   134
val arbitraryN = "arbitrary"
traytel@54026
   135
traytel@54026
   136
fun named_rule k arg get =
traytel@54026
   137
  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
traytel@54026
   138
    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
traytel@54026
   139
      (case get (Context.proof_of context) name of SOME x => x
traytel@54026
   140
      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
traytel@54026
   141
traytel@54026
   142
fun rule get_type get_pred =
wenzelm@55951
   143
  named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
wenzelm@55954
   144
  named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
wenzelm@55954
   145
  named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
traytel@54026
   146
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
traytel@54026
   147
traytel@63709
   148
val coinduct_rules =
traytel@63709
   149
  rule Induct.lookup_coinductT Induct.lookup_coinductP;
traytel@54026
   150
traytel@54026
   151
fun unless_more_args scan = Scan.unless (Scan.lift
traytel@54026
   152
  ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
traytel@54026
   153
    Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
traytel@54026
   154
traytel@54026
   155
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
traytel@54026
   156
  Scan.repeat1 (unless_more_args Args.term)) [];
traytel@54026
   157
traytel@54026
   158
in
traytel@54026
   159
wenzelm@58814
   160
val _ =
wenzelm@58814
   161
  Theory.setup
wenzelm@58814
   162
    (Method.setup @{binding coinduction}
traytel@63709
   163
      (arbitrary -- Scan.option coinduct_rules >>
traytel@63709
   164
        (fn (arbitrary, opt_rules) => fn _ => fn facts =>
traytel@63709
   165
          Seq.DETERM (coinduction_context_tactic arbitrary opt_rules facts 1)))
wenzelm@58814
   166
      "coinduction on types or predicates/sets");
traytel@54026
   167
traytel@54026
   168
end;
traytel@54026
   169
traytel@54026
   170
end;