modernized setup;
authorwenzelm
Wed Oct 29 11:33:29 2014 +0100 (2014-10-29)
changeset 588144c0ad4162cb7
parent 58813 625d04d4fd2a
child 58815 fd3f893a40ea
modernized setup;
tuned whitespace;
src/HOL/Coinduction.thy
src/HOL/Tools/coinduction.ML
     1.1 --- a/src/HOL/Coinduction.thy	Wed Oct 29 11:19:27 2014 +0100
     1.2 +++ b/src/HOL/Coinduction.thy	Wed Oct 29 11:33:29 2014 +0100
     1.3 @@ -14,6 +14,4 @@
     1.4  
     1.5  ML_file "Tools/coinduction.ML"
     1.6  
     1.7 -setup Coinduction.setup
     1.8 -
     1.9  end
     2.1 --- a/src/HOL/Tools/coinduction.ML	Wed Oct 29 11:19:27 2014 +0100
     2.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Oct 29 11:33:29 2014 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  signature COINDUCTION =
     2.5  sig
     2.6    val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
     2.7 -  val setup: theory -> theory
     2.8  end;
     2.9  
    2.10  structure Coinduction : COINDUCTION =
    2.11 @@ -19,11 +18,12 @@
    2.12  open Ctr_Sugar_General_Tactics
    2.13  
    2.14  fun filter_in_out _ [] = ([], [])
    2.15 -  | filter_in_out P (x :: xs) = (let
    2.16 -      val (ins, outs) = filter_in_out P xs;
    2.17 -    in
    2.18 -      if P x then (x :: ins, outs) else (ins, x :: outs)
    2.19 -    end);
    2.20 +  | filter_in_out P (x :: xs) =
    2.21 +      let
    2.22 +        val (ins, outs) = filter_in_out P xs;
    2.23 +      in
    2.24 +        if P x then (x :: ins, outs) else (ins, x :: outs)
    2.25 +      end;
    2.26  
    2.27  fun ALLGOALS_SKIP skip tac st =
    2.28    let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
    2.29 @@ -43,7 +43,7 @@
    2.30  fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
    2.31    let
    2.32      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
    2.33 -    fun find_coinduct t = 
    2.34 +    fun find_coinduct t =
    2.35        Induct.find_coinductP ctxt t @
    2.36        (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
    2.37      val raw_thm =
    2.38 @@ -102,7 +102,7 @@
    2.39                         val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
    2.40                         val inv_thms = init @ [last];
    2.41                         val eqs = take e inv_thms;
    2.42 -                       fun is_local_var t = 
    2.43 +                       fun is_local_var t =
    2.44                           member (fn (t, (_, t')) => t aconv (term_of t')) params t;
    2.45                          val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
    2.46                          val assms = assms' @ drop e inv_thms
    2.47 @@ -146,12 +146,13 @@
    2.48  
    2.49  in
    2.50  
    2.51 -val setup =
    2.52 -  Method.setup @{binding coinduction}
    2.53 -    (arbitrary -- Scan.option coinduct_rule >>
    2.54 -      (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
    2.55 -        Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
    2.56 -    "coinduction on types or predicates/sets";
    2.57 +val _ =
    2.58 +  Theory.setup
    2.59 +    (Method.setup @{binding coinduction}
    2.60 +      (arbitrary -- Scan.option coinduct_rule >>
    2.61 +        (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
    2.62 +          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
    2.63 +      "coinduction on types or predicates/sets");
    2.64  
    2.65  end;
    2.66