author wenzelm Wed, 29 Oct 2014 11:33:29 +0100 changeset 58814 4c0ad4162cb7 parent 58813 625d04d4fd2a child 58815 fd3f893a40ea
modernized setup; tuned whitespace;
 src/HOL/Coinduction.thy file | annotate | diff | comparison | revisions src/HOL/Tools/coinduction.ML file | annotate | diff | comparison | revisions
--- a/src/HOL/Coinduction.thy	Wed Oct 29 11:19:27 2014 +0100
+++ b/src/HOL/Coinduction.thy	Wed Oct 29 11:33:29 2014 +0100
@@ -14,6 +14,4 @@

ML_file "Tools/coinduction.ML"

-setup Coinduction.setup
-
end
--- a/src/HOL/Tools/coinduction.ML	Wed Oct 29 11:19:27 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Wed Oct 29 11:33:29 2014 +0100
@@ -9,7 +9,6 @@
signature COINDUCTION =
sig
val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
-  val setup: theory -> theory
end;

structure Coinduction : COINDUCTION =
@@ -19,11 +18,12 @@
open Ctr_Sugar_General_Tactics

fun filter_in_out _ [] = ([], [])
-  | filter_in_out P (x :: xs) = (let
-      val (ins, outs) = filter_in_out P xs;
-    in
-      if P x then (x :: ins, outs) else (ins, x :: outs)
-    end);
+  | filter_in_out P (x :: xs) =
+      let
+        val (ins, outs) = filter_in_out P xs;
+      in
+        if P x then (x :: ins, outs) else (ins, x :: outs)
+      end;

fun ALLGOALS_SKIP skip tac st =
let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
@@ -43,7 +43,7 @@
fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
let
val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
-    fun find_coinduct t =
+    fun find_coinduct t =
Induct.find_coinductP ctxt t @
(try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
val raw_thm =
@@ -102,7 +102,7 @@
val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
val inv_thms = init @ [last];
val eqs = take e inv_thms;
-                       fun is_local_var t =
+                       fun is_local_var t =
member (fn (t, (_, t')) => t aconv (term_of t')) params t;
val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
val assms = assms' @ drop e inv_thms
@@ -146,12 +146,13 @@

in

-val setup =
-  Method.setup @{binding coinduction}
-    (arbitrary -- Scan.option coinduct_rule >>
-      (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
-        Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
-    "coinduction on types or predicates/sets";
+val _ =
+  Theory.setup
+    (Method.setup @{binding coinduction}
+      (arbitrary -- Scan.option coinduct_rule >>
+        (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
+          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
+      "coinduction on types or predicates/sets");

end;