# HG changeset patch
# User huffman
# Date 1116883927 -7200
# Node ID 58186c507750fde987293777afb7874a4d8a2985
# Parent  b8ba6727712fd4d77df1b18f8c6acd7f3addb8a2
moved continuity simproc to Cfun.thy

diff -r b8ba6727712f -r 58186c507750 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon May 23 23:24:38 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Mon May 23 23:32:07 2005 +0200
@@ -436,10 +436,31 @@
 
 text {* cont2cont tactic *}
 
-lemmas cont_lemmas1 = cont_const cont_id cont_Rep_CFun2
-                    cont2cont_Rep_CFun cont2cont_LAM
+lemmas cont_lemmas1 =
+  cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
+
+text {*
+  Continuity simproc by Brian Huffman.
+  Given the term @{term "cont f"}, the procedure tries to
+  construct the theorem @{prop "cont f == True"}. If this
+  theorem cannot be completely solved by the introduction
+  rules, then the procedure returns a conditional rewrite
+  rule with the unsolved subgoals as premises.
+*}
 
-declare cont_lemmas1 [simp]
+ML_setup {*
+local
+  val rules = thms "cont_lemmas1";
+  fun solve_cont sg _ t =
+    let val tr = instantiate' [] [SOME (cterm_of sg t)] Eq_TrueI;
+        val tac = REPEAT_ALL_NEW (resolve_tac rules) 1;
+    in Option.map fst (Seq.pull (tac tr)) end;
+in
+  val cont_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
+        "continuity" ["cont f"] solve_cont;
+end;
+Addsimprocs [cont_proc];
+*}
 
 text {* HINT: @{text cont_tac} is now installed in simplifier in Lift.ML ! *}
 
@@ -455,11 +476,6 @@
 
 declare beta_cfun [simp]
 
-text {* use @{text cont_tac} as autotac. *}
-
-text {* HINT: @{text cont_tac} is now installed in simplifier in Lift.ML ! *}
-(*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
-
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
 lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)