moved 'coinduction' proof method to 'HOL'
authorblanchet
Wed Nov 20 20:45:20 2013 +0100 (2013-11-20)
changeset 545405d7006e9205e
parent 54539 bbab2ebda234
child 54541 13933f920a5d
moved 'coinduction' proof method to 'HOL'
src/HOL/BNF/BNF.thy
src/HOL/BNF/Coinduction.thy
src/HOL/BNF/README.html
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/BNF/Tools/coinduction.ML
src/HOL/Coinduction.thy
src/HOL/Main.thy
src/HOL/Tools/coinduction.ML
src/HOL/Tools/ctr_sugar_util.ML
     1.1 --- a/src/HOL/BNF/BNF.thy	Wed Nov 20 20:18:53 2013 +0100
     1.2 +++ b/src/HOL/BNF/BNF.thy	Wed Nov 20 20:45:20 2013 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  header {* Bounded Natural Functors for (Co)datatypes *}
     1.5  
     1.6  theory BNF
     1.7 -imports Countable_Set_Type BNF_LFP BNF_GFP Coinduction
     1.8 +imports Countable_Set_Type BNF_LFP BNF_GFP
     1.9  begin
    1.10  
    1.11  hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
     2.1 --- a/src/HOL/BNF/Coinduction.thy	Wed Nov 20 20:18:53 2013 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,19 +0,0 @@
     2.4 -(*  Title:      HOL/BNF/Coinduction.thy
     2.5 -    Author:     Johannes Hölzl, TU Muenchen
     2.6 -    Author:     Dmitriy Traytel, TU Muenchen
     2.7 -    Copyright   2013
     2.8 -
     2.9 -Coinduction method that avoids some boilerplate compared to coinduct.
    2.10 -*)
    2.11 -
    2.12 -header {* Coinduction Method *}
    2.13 -
    2.14 -theory Coinduction
    2.15 -imports BNF_Util
    2.16 -begin
    2.17 -
    2.18 -ML_file "Tools/coinduction.ML"
    2.19 -
    2.20 -setup Coinduction.setup
    2.21 -
    2.22 -end
     3.1 --- a/src/HOL/BNF/README.html	Wed Nov 20 20:18:53 2013 +0100
     3.2 +++ b/src/HOL/BNF/README.html	Wed Nov 20 20:45:20 2013 +0100
     3.3 @@ -37,9 +37,10 @@
     3.4  The key notion underlying the package is that of a <i>bounded natural functor</i>
     3.5  (<i>BNF</i>)&mdash;an enriched type constructor satisfying specific properties
     3.6  preserved by interesting categorical operations (composition, least fixed point,
     3.7 -and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt>
     3.8 -files register various basic types, notably for sums, products, function spaces,
     3.9 -finite sets, multisets, and countable sets. Custom BNFs can be registered as well.
    3.10 +and greatest fixed point). The <tt>Basic_BNFs.thy</tt>, <tt>More_BNFs.thy</tt>,
    3.11 +and <tt>Countable_Set_Type.thy</tt> files register various basic types, notably
    3.12 +for sums, products, function spaces, finite sets, multisets, and countable sets.
    3.13 +Custom BNFs can be registered as well.
    3.14  
    3.15  <p>
    3.16  <b>Warning:</b> The package is under development. Please contact any nonempty
     4.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Nov 20 20:18:53 2013 +0100
     4.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Nov 20 20:45:20 2013 +0100
     4.3 @@ -132,7 +132,6 @@
     4.4    val no_refl: thm list -> thm list
     4.5    val no_reflexive: thm list -> thm list
     4.6  
     4.7 -  val cterm_instantiate_pos: cterm option list -> thm -> thm
     4.8    val fold_thms: Proof.context -> thm list -> thm -> thm
     4.9  
    4.10    val parse_binding_colon: binding parser
    4.11 @@ -140,14 +139,6 @@
    4.12  
    4.13    val typedef: binding * (string * sort) list * mixfix -> term ->
    4.14      (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
    4.15 -
    4.16 -  val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    4.17 -  val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
    4.18 -    tactic
    4.19 -  val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
    4.20 -  val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
    4.21 -  val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
    4.22 -  val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
    4.23  end;
    4.24  
    4.25  structure BNF_Util : BNF_UTIL =
    4.26 @@ -276,25 +267,6 @@
    4.27      ((name, Typedef.transform_info phi info), lthy)
    4.28    end;
    4.29  
    4.30 -(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
    4.31 -fun WRAP gen_before gen_after xs core_tac =
    4.32 -  fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
    4.33 -
    4.34 -fun WRAP' gen_before gen_after xs core_tac =
    4.35 -  fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
    4.36 -
    4.37 -fun CONJ_WRAP_GEN conj_tac gen_tac xs =
    4.38 -  let val (butlast, last) = split_last xs;
    4.39 -  in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
    4.40 -
    4.41 -fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
    4.42 -  let val (butlast, last) = split_last xs;
    4.43 -  in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
    4.44 -
    4.45 -(*not eta-converted because of monotype restriction*)
    4.46 -fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
    4.47 -fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
    4.48 -
    4.49  
    4.50  
    4.51  (* Term construction *)
    4.52 @@ -600,17 +572,6 @@
    4.53  val no_refl = filter_out is_refl;
    4.54  val no_reflexive = filter_out Thm.is_reflexive;
    4.55  
    4.56 -fun cterm_instantiate_pos cts thm =
    4.57 -  let
    4.58 -    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
    4.59 -    val vars = Term.add_vars (prop_of thm) [];
    4.60 -    val vars' = rev (drop (length vars - length cts) vars);
    4.61 -    val ps = map_filter (fn (_, NONE) => NONE
    4.62 -      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
    4.63 -  in
    4.64 -    Drule.cterm_instantiate ps thm
    4.65 -  end;
    4.66 -
    4.67  fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
    4.68  
    4.69  end;
     5.1 --- a/src/HOL/BNF/Tools/coinduction.ML	Wed Nov 20 20:18:53 2013 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,159 +0,0 @@
     5.4 -(*  Title:      HOL/BNF/Tools/coinduction.ML
     5.5 -    Author:     Johannes Hölzl, TU Muenchen
     5.6 -    Author:     Dmitriy Traytel, TU Muenchen
     5.7 -    Copyright   2013
     5.8 -
     5.9 -Coinduction method that avoids some boilerplate compared to coinduct.
    5.10 -*)
    5.11 -
    5.12 -signature COINDUCTION =
    5.13 -sig
    5.14 -  val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
    5.15 -  val setup: theory -> theory
    5.16 -end;
    5.17 -
    5.18 -structure Coinduction : COINDUCTION =
    5.19 -struct
    5.20 -
    5.21 -open BNF_Util
    5.22 -open BNF_Tactics
    5.23 -
    5.24 -fun filter_in_out _ [] = ([], [])
    5.25 -  | filter_in_out P (x :: xs) = (let
    5.26 -      val (ins, outs) = filter_in_out P xs;
    5.27 -    in
    5.28 -      if P x then (x :: ins, outs) else (ins, x :: outs)
    5.29 -    end);
    5.30 -
    5.31 -fun ALLGOALS_SKIP skip tac st =
    5.32 -  let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
    5.33 -  in doall (nprems_of st) st  end;
    5.34 -
    5.35 -fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
    5.36 -  st |> (tac1 i THEN (fn st' =>
    5.37 -    Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
    5.38 -
    5.39 -fun DELETE_PREMS_AFTER skip tac i st =
    5.40 -  let
    5.41 -    val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
    5.42 -  in
    5.43 -    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
    5.44 -  end;
    5.45 -
    5.46 -fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
    5.47 -  let
    5.48 -    val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
    5.49 -    fun find_coinduct t = 
    5.50 -      Induct.find_coinductP ctxt t @
    5.51 -      (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
    5.52 -    val raw_thm = case opt_raw_thm
    5.53 -      of SOME raw_thm => raw_thm
    5.54 -       | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
    5.55 -    val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
    5.56 -    val cases = Rule_Cases.get raw_thm |> fst
    5.57 -  in
    5.58 -    NO_CASES (HEADGOAL (
    5.59 -      Object_Logic.rulify_tac THEN'
    5.60 -      Method.insert_tac prems THEN'
    5.61 -      Object_Logic.atomize_prems_tac THEN'
    5.62 -      DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
    5.63 -        let
    5.64 -          val vars = raw_vars @ map (term_of o snd) params;
    5.65 -          val names_ctxt = ctxt
    5.66 -            |> fold Variable.declare_names vars
    5.67 -            |> fold Variable.declare_thm (raw_thm :: prems);
    5.68 -          val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    5.69 -          val (rhoTs, rhots) = Thm.match (thm_concl, concl)
    5.70 -            |>> map (pairself typ_of)
    5.71 -            ||> map (pairself term_of);
    5.72 -          val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
    5.73 -            |> map (subst_atomic_types rhoTs);
    5.74 -          val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
    5.75 -          val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
    5.76 -            |>> (fn names => Variable.variant_fixes names names_ctxt) ;
    5.77 -          val eqs =
    5.78 -            map3 (fn name => fn T => fn (_, rhs) =>
    5.79 -              HOLogic.mk_eq (Free (name, T), rhs))
    5.80 -            names Ts raw_eqs;
    5.81 -          val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
    5.82 -            |> try (Library.foldr1 HOLogic.mk_conj)
    5.83 -            |> the_default @{term True}
    5.84 -            |> list_exists_free vars
    5.85 -            |> Term.map_abs_vars (Variable.revert_fixed ctxt)
    5.86 -            |> fold_rev Term.absfree (names ~~ Ts)
    5.87 -            |> certify ctxt;
    5.88 -          val thm = cterm_instantiate_pos [SOME phi] raw_thm;
    5.89 -          val e = length eqs;
    5.90 -          val p = length prems;
    5.91 -        in
    5.92 -          HEADGOAL (EVERY' [rtac thm,
    5.93 -            EVERY' (map (fn var =>
    5.94 -              rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
    5.95 -            if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
    5.96 -            else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
    5.97 -            K (ALLGOALS_SKIP skip
    5.98 -               (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
    5.99 -               DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
   5.100 -                 (case prems of
   5.101 -                   [] => all_tac
   5.102 -                 | inv::case_prems =>
   5.103 -                     let
   5.104 -                       val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
   5.105 -                       val inv_thms = init @ [last];
   5.106 -                       val eqs = take e inv_thms;
   5.107 -                       fun is_local_var t = 
   5.108 -                         member (fn (t, (_, t')) => t aconv (term_of t')) params t;
   5.109 -                        val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
   5.110 -                        val assms = assms' @ drop e inv_thms
   5.111 -                      in
   5.112 -                        HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
   5.113 -                        unfold_thms_tac ctxt eqs
   5.114 -                      end)) ctxt)))])
   5.115 -        end) ctxt) THEN'
   5.116 -      K (prune_params_tac))) st
   5.117 -    |> Seq.maps (fn (_, st) =>
   5.118 -      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
   5.119 -  end;
   5.120 -
   5.121 -local
   5.122 -
   5.123 -val ruleN = "rule"
   5.124 -val arbitraryN = "arbitrary"
   5.125 -fun single_rule [rule] = rule
   5.126 -  | single_rule _ = error "Single rule expected";
   5.127 -
   5.128 -fun named_rule k arg get =
   5.129 -  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
   5.130 -    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
   5.131 -      (case get (Context.proof_of context) name of SOME x => x
   5.132 -      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   5.133 -
   5.134 -fun rule get_type get_pred =
   5.135 -  named_rule Induct.typeN (Args.type_name false) get_type ||
   5.136 -  named_rule Induct.predN (Args.const false) get_pred ||
   5.137 -  named_rule Induct.setN (Args.const false) get_pred ||
   5.138 -  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   5.139 -
   5.140 -val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
   5.141 -
   5.142 -fun unless_more_args scan = Scan.unless (Scan.lift
   5.143 -  ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
   5.144 -    Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
   5.145 -
   5.146 -val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   5.147 -  Scan.repeat1 (unless_more_args Args.term)) [];
   5.148 -
   5.149 -in
   5.150 -
   5.151 -val setup =
   5.152 -  Method.setup @{binding coinduction}
   5.153 -    (arbitrary -- Scan.option coinduct_rule >>
   5.154 -      (fn (arbitrary, opt_rule) => fn ctxt =>
   5.155 -        RAW_METHOD_CASES (fn facts =>
   5.156 -          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
   5.157 -    "coinduction on types or predicates/sets";
   5.158 -
   5.159 -end;
   5.160 -
   5.161 -end;
   5.162 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Coinduction.thy	Wed Nov 20 20:45:20 2013 +0100
     6.3 @@ -0,0 +1,19 @@
     6.4 +(*  Title:      HOL/Coinduction.thy
     6.5 +    Author:     Johannes Hölzl, TU Muenchen
     6.6 +    Author:     Dmitriy Traytel, TU Muenchen
     6.7 +    Copyright   2013
     6.8 +
     6.9 +Coinduction method that avoids some boilerplate compared to coinduct.
    6.10 +*)
    6.11 +
    6.12 +header {* Coinduction Method *}
    6.13 +
    6.14 +theory Coinduction
    6.15 +imports Inductive
    6.16 +begin
    6.17 +
    6.18 +ML_file "Tools/coinduction.ML"
    6.19 +
    6.20 +setup Coinduction.setup
    6.21 +
    6.22 +end
     7.1 --- a/src/HOL/Main.thy	Wed Nov 20 20:18:53 2013 +0100
     7.2 +++ b/src/HOL/Main.thy	Wed Nov 20 20:45:20 2013 +0100
     7.3 @@ -1,7 +1,7 @@
     7.4  header {* Main HOL *}
     7.5  
     7.6  theory Main
     7.7 -imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix
     7.8 +imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction
     7.9  begin
    7.10  
    7.11  text {*
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Nov 20 20:45:20 2013 +0100
     8.3 @@ -0,0 +1,159 @@
     8.4 +(*  Title:      HOL/Tools/coinduction.ML
     8.5 +    Author:     Johannes Hölzl, TU Muenchen
     8.6 +    Author:     Dmitriy Traytel, TU Muenchen
     8.7 +    Copyright   2013
     8.8 +
     8.9 +Coinduction method that avoids some boilerplate compared to coinduct.
    8.10 +*)
    8.11 +
    8.12 +signature COINDUCTION =
    8.13 +sig
    8.14 +  val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
    8.15 +  val setup: theory -> theory
    8.16 +end;
    8.17 +
    8.18 +structure Coinduction : COINDUCTION =
    8.19 +struct
    8.20 +
    8.21 +open Ctr_Sugar_Util
    8.22 +open Ctr_Sugar_General_Tactics
    8.23 +
    8.24 +fun filter_in_out _ [] = ([], [])
    8.25 +  | filter_in_out P (x :: xs) = (let
    8.26 +      val (ins, outs) = filter_in_out P xs;
    8.27 +    in
    8.28 +      if P x then (x :: ins, outs) else (ins, x :: outs)
    8.29 +    end);
    8.30 +
    8.31 +fun ALLGOALS_SKIP skip tac st =
    8.32 +  let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
    8.33 +  in doall (nprems_of st) st  end;
    8.34 +
    8.35 +fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
    8.36 +  st |> (tac1 i THEN (fn st' =>
    8.37 +    Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
    8.38 +
    8.39 +fun DELETE_PREMS_AFTER skip tac i st =
    8.40 +  let
    8.41 +    val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
    8.42 +  in
    8.43 +    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
    8.44 +  end;
    8.45 +
    8.46 +fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
    8.47 +  let
    8.48 +    val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
    8.49 +    fun find_coinduct t = 
    8.50 +      Induct.find_coinductP ctxt t @
    8.51 +      (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
    8.52 +    val raw_thm = case opt_raw_thm
    8.53 +      of SOME raw_thm => raw_thm
    8.54 +       | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
    8.55 +    val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
    8.56 +    val cases = Rule_Cases.get raw_thm |> fst
    8.57 +  in
    8.58 +    NO_CASES (HEADGOAL (
    8.59 +      Object_Logic.rulify_tac THEN'
    8.60 +      Method.insert_tac prems THEN'
    8.61 +      Object_Logic.atomize_prems_tac THEN'
    8.62 +      DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
    8.63 +        let
    8.64 +          val vars = raw_vars @ map (term_of o snd) params;
    8.65 +          val names_ctxt = ctxt
    8.66 +            |> fold Variable.declare_names vars
    8.67 +            |> fold Variable.declare_thm (raw_thm :: prems);
    8.68 +          val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    8.69 +          val (rhoTs, rhots) = Thm.match (thm_concl, concl)
    8.70 +            |>> map (pairself typ_of)
    8.71 +            ||> map (pairself term_of);
    8.72 +          val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
    8.73 +            |> map (subst_atomic_types rhoTs);
    8.74 +          val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
    8.75 +          val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
    8.76 +            |>> (fn names => Variable.variant_fixes names names_ctxt) ;
    8.77 +          val eqs =
    8.78 +            map3 (fn name => fn T => fn (_, rhs) =>
    8.79 +              HOLogic.mk_eq (Free (name, T), rhs))
    8.80 +            names Ts raw_eqs;
    8.81 +          val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
    8.82 +            |> try (Library.foldr1 HOLogic.mk_conj)
    8.83 +            |> the_default @{term True}
    8.84 +            |> list_exists_free vars
    8.85 +            |> Term.map_abs_vars (Variable.revert_fixed ctxt)
    8.86 +            |> fold_rev Term.absfree (names ~~ Ts)
    8.87 +            |> certify ctxt;
    8.88 +          val thm = cterm_instantiate_pos [SOME phi] raw_thm;
    8.89 +          val e = length eqs;
    8.90 +          val p = length prems;
    8.91 +        in
    8.92 +          HEADGOAL (EVERY' [rtac thm,
    8.93 +            EVERY' (map (fn var =>
    8.94 +              rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
    8.95 +            if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
    8.96 +            else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
    8.97 +            K (ALLGOALS_SKIP skip
    8.98 +               (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
    8.99 +               DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
   8.100 +                 (case prems of
   8.101 +                   [] => all_tac
   8.102 +                 | inv::case_prems =>
   8.103 +                     let
   8.104 +                       val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
   8.105 +                       val inv_thms = init @ [last];
   8.106 +                       val eqs = take e inv_thms;
   8.107 +                       fun is_local_var t = 
   8.108 +                         member (fn (t, (_, t')) => t aconv (term_of t')) params t;
   8.109 +                        val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
   8.110 +                        val assms = assms' @ drop e inv_thms
   8.111 +                      in
   8.112 +                        HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
   8.113 +                        unfold_thms_tac ctxt eqs
   8.114 +                      end)) ctxt)))])
   8.115 +        end) ctxt) THEN'
   8.116 +      K (prune_params_tac))) st
   8.117 +    |> Seq.maps (fn (_, st) =>
   8.118 +      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
   8.119 +  end;
   8.120 +
   8.121 +local
   8.122 +
   8.123 +val ruleN = "rule"
   8.124 +val arbitraryN = "arbitrary"
   8.125 +fun single_rule [rule] = rule
   8.126 +  | single_rule _ = error "Single rule expected";
   8.127 +
   8.128 +fun named_rule k arg get =
   8.129 +  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
   8.130 +    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
   8.131 +      (case get (Context.proof_of context) name of SOME x => x
   8.132 +      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   8.133 +
   8.134 +fun rule get_type get_pred =
   8.135 +  named_rule Induct.typeN (Args.type_name false) get_type ||
   8.136 +  named_rule Induct.predN (Args.const false) get_pred ||
   8.137 +  named_rule Induct.setN (Args.const false) get_pred ||
   8.138 +  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   8.139 +
   8.140 +val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
   8.141 +
   8.142 +fun unless_more_args scan = Scan.unless (Scan.lift
   8.143 +  ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
   8.144 +    Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
   8.145 +
   8.146 +val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   8.147 +  Scan.repeat1 (unless_more_args Args.term)) [];
   8.148 +
   8.149 +in
   8.150 +
   8.151 +val setup =
   8.152 +  Method.setup @{binding coinduction}
   8.153 +    (arbitrary -- Scan.option coinduct_rule >>
   8.154 +      (fn (arbitrary, opt_rule) => fn ctxt =>
   8.155 +        RAW_METHOD_CASES (fn facts =>
   8.156 +          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
   8.157 +    "coinduction on types or predicates/sets";
   8.158 +
   8.159 +end;
   8.160 +
   8.161 +end;
   8.162 +
     9.1 --- a/src/HOL/Tools/ctr_sugar_util.ML	Wed Nov 20 20:18:53 2013 +0100
     9.2 +++ b/src/HOL/Tools/ctr_sugar_util.ML	Wed Nov 20 20:45:20 2013 +0100
     9.3 @@ -56,6 +56,7 @@
     9.4  
     9.5    val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
     9.6  
     9.7 +  val cterm_instantiate_pos: cterm option list -> thm -> thm
     9.8    val unfold_thms: Proof.context -> thm list -> thm -> thm
     9.9  
    9.10    val certifyT: Proof.context -> typ -> ctyp
    9.11 @@ -66,6 +67,14 @@
    9.12    val parse_binding: binding parser
    9.13  
    9.14    val ss_only: thm list -> Proof.context -> Proof.context
    9.15 +
    9.16 +  val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    9.17 +  val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
    9.18 +    tactic
    9.19 +  val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
    9.20 +  val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
    9.21 +  val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
    9.22 +  val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
    9.23  end;
    9.24  
    9.25  structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
    9.26 @@ -186,6 +195,17 @@
    9.27      Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
    9.28    end;
    9.29  
    9.30 +fun cterm_instantiate_pos cts thm =
    9.31 +  let
    9.32 +    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
    9.33 +    val vars = Term.add_vars (prop_of thm) [];
    9.34 +    val vars' = rev (drop (length vars - length cts) vars);
    9.35 +    val ps = map_filter (fn (_, NONE) => NONE
    9.36 +      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
    9.37 +  in
    9.38 +    Drule.cterm_instantiate ps thm
    9.39 +  end;
    9.40 +
    9.41  fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
    9.42  
    9.43  (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
    9.44 @@ -202,4 +222,23 @@
    9.45  
    9.46  fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
    9.47  
    9.48 +(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
    9.49 +fun WRAP gen_before gen_after xs core_tac =
    9.50 +  fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
    9.51 +
    9.52 +fun WRAP' gen_before gen_after xs core_tac =
    9.53 +  fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
    9.54 +
    9.55 +fun CONJ_WRAP_GEN conj_tac gen_tac xs =
    9.56 +  let val (butlast, last) = split_last xs;
    9.57 +  in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
    9.58 +
    9.59 +fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
    9.60 +  let val (butlast, last) = split_last xs;
    9.61 +  in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
    9.62 +
    9.63 +(*not eta-converted because of monotype restriction*)
    9.64 +fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
    9.65 +fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
    9.66 +
    9.67  end;