# HG changeset patch
# User huffman
# Date 1118713820 -7200
# Node ID c6f5ade2960820c26cf21c6e3738fb3ccf743d25
# Parent  a9dec19693488ae4df4a600425eec55b70ada224
moved continuity simproc to a separate file

diff -r a9dec1969348 -r c6f5ade29608 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Tue Jun 14 03:35:15 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Tue Jun 14 03:50:20 2005 +0200
@@ -9,6 +9,7 @@
 
 theory Cfun
 imports TypedefPcpo
+files ("cont_proc.ML")
 begin
 
 defaultsort cpo
@@ -201,7 +202,7 @@
 apply (simp add: monofun_Rep_CFun2)
 done
 
-text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"}: uses MF2 lemmas from Cont.thy *}
+text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *}
 
 lemma ex_lub_cfun: "[| chain(F); chain(Y) |] ==> 
                 lub(range(%j. lub(range(%i. F(j)$(Y i))))) = 
@@ -269,33 +270,13 @@
 apply (simp add: p2 cont2cont_CF1L_rev)
 done
 
-text {* cont2cont tactic *}
+text {* continuity simplification procedure *}
 
 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.
-*}
-
-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];
-*}
+use "cont_proc.ML";
+setup ContProc.setup;
 
 (*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
 (*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
diff -r a9dec1969348 -r c6f5ade29608 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue Jun 14 03:35:15 2005 +0200
+++ b/src/HOLCF/IsaMakefile	Tue Jun 14 03:50:20 2005 +0200
@@ -35,7 +35,7 @@
   ROOT.ML Sprod.ML Sprod.thy \
   Ssum.ML Ssum.thy \
   Tr.ML Tr.thy TypedefPcpo.thy Up.ML \
-  Up.thy adm_tac.ML cont_consts.ML fixrec_package.ML \
+  Up.thy adm_tac.ML cont_consts.ML cont_proc.ML fixrec_package.ML \
   domain/axioms.ML domain/extender.ML domain/interface.ML \
   domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML \
   ex/Stream.thy document/root.tex
diff -r a9dec1969348 -r c6f5ade29608 src/HOLCF/cont_proc.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/cont_proc.ML	Tue Jun 14 03:50:20 2005 +0200
@@ -0,0 +1,102 @@
+(*  Title:      HOLCF/cont_proc.ML
+    ID:         $Id$
+    Author:     Brian Huffman
+*)
+
+signature CONT_PROC =
+sig
+  val is_lcf_term: term -> bool
+  val cont_thms: term -> thm list
+  val cont_proc: theory -> simproc
+  val setup: (theory -> theory) list
+end;
+
+structure ContProc: CONT_PROC =
+struct
+
+(** theory context references **)
+
+val cont_K = thm "cont_const";
+val cont_I = thm "cont_id";
+val cont_A = thm "cont2cont_Rep_CFun";
+val cont_L = thm "cont2cont_LAM";
+val cont_R = thm "cont_Rep_CFun2";
+
+(* checks whether a term is written entirely in the LCF sublanguage *)
+fun is_lcf_term (Const("Cfun.Rep_CFun",_) $ t $ u) = is_lcf_term t andalso is_lcf_term u
+  | is_lcf_term (Const("Cfun.Abs_CFun",_) $ Abs (_,_,t)) = is_lcf_term t
+  | is_lcf_term (_ $ _) = false
+  | is_lcf_term (Abs _) = false
+  | is_lcf_term _ = true; (* Const, Free, Var, and Bound are OK *)
+
+(*
+  efficiently generates a cont thm for every LAM abstraction in a term,
+  using forward proof and reusing common subgoals
+*)
+local
+  fun var 0 = [SOME cont_I]
+    | var n = NONE :: var (n-1);
+
+  fun k NONE     = cont_K
+    | k (SOME x) = x;
+
+  fun ap NONE NONE = NONE
+    | ap x    y    = SOME (k y RS (k x RS cont_A));
+
+  fun zip []      []      = []
+    | zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
+    | zip (x::xs) []      = (ap x    NONE) :: zip xs []
+    | zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
+
+  fun lam [] = ([], cont_K)
+    | lam (x::ys) = let
+        (* should use "standard" for thms that are used multiple times *)
+        (* it seems to allow for sharing in explicit proof objects *)
+        val x' = standard (k x);
+        val Lx = x' RS cont_L;
+        in (map (fn y => SOME (k y RS Lx)) ys, x') end;
+
+  (* first list: cont thm for each dangling bound variable *)
+  (* second list: cont thm for each LAM *)
+  fun cont_thms1 (Const _ $ f $ t) = let
+        val (cs1,ls1) = cont_thms1 f;
+        val (cs2,ls2) = cont_thms1 t;
+        in (zip cs1 cs2, ls1 @ ls2) end
+    | cont_thms1 (Const _ $ Abs (_,_,t)) = let
+        val (cs,ls) = cont_thms1 t;
+        val (cs',l) = lam cs;
+        in (cs',l::ls) end
+    | cont_thms1 (Bound n) = (var n, [])
+    | cont_thms1 _ = ([],[]);
+in
+  (* precondition: is_lcf_term t = true *)
+  fun cont_thms t = snd (cont_thms1 t);
+end;
+
+(*
+  Given the term "cont f", the procedure tries to construct the
+  theorem "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.
+*)
+
+local
+  fun solve_cont sg _ (t as Const("Cont.cont",_) $ f) =
+    let
+      val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
+      val tr = instantiate' [] [SOME (cterm_of sg t)] Eq_TrueI;
+      val f' = Const("Cfun.Abs_CFun",dummyT) $ f;
+      val tac = if is_lcf_term f'
+        then rtac (hd (cont_thms f')) 1
+        else REPEAT_ALL_NEW (resolve_tac rules) 1;
+    in Option.map fst (Seq.pull (tac tr)) end
+    | solve_cont sg _ _ = NONE;
+in
+  fun cont_proc thy = Simplifier.simproc (Theory.sign_of thy)
+        "cont_proc" ["cont f"] solve_cont;
+end;
+
+val setup =
+  [fn thy => Simplifier.change_simpset_of (op addsimprocs) [cont_proc thy] thy];
+
+end;