merged

--- a/src/HOL/NSA/Examples/NSPrimes.thy	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Thu May 20 16:25:22 2010 +0200
@@ -13,9 +13,7 @@
 text{*These can be used to derive an alternative proof of the infinitude of
 primes by considering a property of nonstandard sets.*}
 
-definition
-  hdvd  :: "[hypnat, hypnat] => bool"       (infixl "hdvd" 50) where
-  [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
+declare dvd_def [transfer_refold]
 
 definition
   starprime :: "hypnat set" where
@@ -49,14 +47,14 @@
 
 
 (* Goldblatt: Exercise 5.11(2) - p. 57 *)
-lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)"
+lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
 by (transfer, rule dvd_by_all)
 
 lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
 
 (* Goldblatt: Exercise 5.11(2) - p. 57 *)
 lemma hypnat_dvd_all_hypnat_of_nat:
-     "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)"
+     "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) dvd N)"
 apply (cut_tac hdvd_by_all)
 apply (drule_tac x = whn in spec, auto)
 apply (rule exI, auto)
@@ -70,7 +68,7 @@
 
 (* Goldblatt: Exercise 5.11(3a) - p 57  *)
 lemma starprime:
-  "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}"
+  "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
 by (transfer, auto simp add: prime_def)
 
 lemma prime_two:  "prime 2"
@@ -88,13 +86,11 @@
 apply (rule_tac x = n in exI, auto)
 apply (drule conjI [THEN not_prime_ex_mk], auto)
 apply (drule_tac x = m in spec, auto)
-apply (rule_tac x = ka in exI)
-apply (auto intro: dvd_mult2)
 done
 
 (* Goldblatt Exercise 5.11(3b) - p 57  *)
 lemma hyperprime_factor_exists [rule_format]:
-  "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
+  "!!n. 1 < n ==> (\<exists>k \<in> starprime. k dvd n)"
 by (transfer, simp add: prime_factor_exists)
 
 (* Goldblatt Exercise 3.10(1) - p. 29 *)
@@ -257,14 +253,14 @@
 
 subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
 
-lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)"
+lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
 apply auto
 apply (rule_tac x = 2 in bexI)
 apply (transfer, auto)
 done
 declare lemma_not_dvd_hypnat_one [simp]
 
-lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1"
+lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n dvd 1"
 apply (cut_tac lemma_not_dvd_hypnat_one)
 apply (auto simp del: lemma_not_dvd_hypnat_one)
 done
@@ -314,13 +310,13 @@
 by (cut_tac hypnat_of_nat_one_not_prime, simp)
 declare hypnat_one_not_prime [simp]
 
-lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
-by (transfer, rule dvd_diff)
+lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)"
+by (transfer, rule dvd_diff_nat)
 
 lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1"
 by (unfold dvd_def, auto)
 
-lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1"
+lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
 by (transfer, rule dvd_one_eq_one)
 
 theorem not_finite_prime: "~ finite {p. prime p}"

--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu May 20 16:25:22 2010 +0200
@@ -13,7 +13,7 @@
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
 code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
-ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
+ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
 
@@ -42,7 +42,7 @@
 
 thm max_of_my_SucP.equation
 
-ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_max_natP} *}
+ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_max_natP} *}
 
 values "{x. max_of_my_SucP x 6}"
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu May 20 16:25:22 2010 +0200
@@ -74,7 +74,8 @@
   end
 
 fun preprocess_strong_conn_constnames options gr ts thy =
-  if forall (fn (Const (c, _)) => Predicate_Compile_Core.is_registered thy c) ts then
+  if forall (fn (Const (c, _)) =>
+      Predicate_Compile_Core.is_registered (ProofContext.init_global thy) c) ts then
     thy
   else
     let

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 20 16:25:22 2010 +0200
@@ -18,27 +18,29 @@
     -> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
   val register_predicate : (string * thm list * thm) -> theory -> theory
   val register_intros : string * thm list -> theory -> theory
-  val is_registered : theory -> string -> bool
-  val function_name_of : compilation -> theory -> string -> mode -> string
+  val is_registered : Proof.context -> string -> bool
+  val function_name_of : compilation -> Proof.context -> string -> mode -> string
   val predfun_intro_of: Proof.context -> string -> mode -> thm
   val predfun_elim_of: Proof.context -> string -> mode -> thm
-  val all_preds_of : theory -> string list
-  val modes_of: compilation -> theory -> string -> mode list
-  val all_modes_of : compilation -> theory -> (string * mode list) list
-  val all_random_modes_of : theory -> (string * mode list) list
-  val intros_of : theory -> string -> thm list
+  val all_preds_of : Proof.context -> string list
+  val modes_of: compilation -> Proof.context -> string -> mode list
+  val all_modes_of : compilation -> Proof.context -> (string * mode list) list
+  val all_random_modes_of : Proof.context -> (string * mode list) list
+  val intros_of : Proof.context -> string -> thm list
   val add_intro : thm -> theory -> theory
   val set_elim : thm -> theory -> theory
   val register_alternative_function : string -> mode -> string -> theory -> theory
-  val alternative_compilation_of : theory -> string -> mode ->
+  val alternative_compilation_of_global : theory -> string -> mode ->
+    (compilation_funs -> typ -> term) option
+  val alternative_compilation_of : Proof.context -> string -> mode ->
     (compilation_funs -> typ -> term) option
   val functional_compilation : string -> mode -> compilation_funs -> typ -> term
   val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
   val force_modes_and_compilations : string ->
     (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
   val preprocess_intro : theory -> thm -> thm
-  val print_stored_rules : theory -> unit
-  val print_all_modes : compilation -> theory -> unit
+  val print_stored_rules : Proof.context -> unit
+  val print_all_modes : compilation -> Proof.context -> unit
   val mk_casesrule : Proof.context -> term -> thm list -> term
   val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
   val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
@@ -228,77 +230,81 @@
 
 (* queries *)
 
-fun lookup_pred_data thy name =
-  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
+fun lookup_pred_data ctxt name =
+  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
 
-fun the_pred_data thy name = case lookup_pred_data thy name
+fun the_pred_data ctxt name = case lookup_pred_data ctxt name
  of NONE => error ("No such predicate " ^ quote name)  
   | SOME data => data;
 
 val is_registered = is_some oo lookup_pred_data
 
-val all_preds_of = Graph.keys o PredData.get
+val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
 
-fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy
+val intros_of = #intros oo the_pred_data
 
-fun the_elim_of thy name = case #elim (the_pred_data thy name)
+fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
  of NONE => error ("No elimination rule for predicate " ^ quote name)
-  | SOME thm => Thm.transfer thy thm
+  | SOME thm => thm
   
-val has_elim = is_some o #elim oo the_pred_data;
+val has_elim = is_some o #elim oo the_pred_data
 
-fun function_names_of compilation thy name =
-  case AList.lookup (op =) (#function_names (the_pred_data thy name)) compilation of
+fun function_names_of compilation ctxt name =
+  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
     NONE => error ("No " ^ string_of_compilation compilation
       ^ "functions defined for predicate " ^ quote name)
   | SOME fun_names => fun_names
 
-fun function_name_of compilation thy name mode =
+fun function_name_of compilation ctxt name mode =
   case AList.lookup eq_mode
-    (function_names_of compilation thy name) mode of
+    (function_names_of compilation ctxt name) mode of
     NONE => error ("No " ^ string_of_compilation compilation
       ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
   | SOME function_name => function_name
 
-fun modes_of compilation thy name = map fst (function_names_of compilation thy name)
+fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
 
-fun all_modes_of compilation thy =
-  map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
-    (all_preds_of thy)
+fun all_modes_of compilation ctxt =
+  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
+    (all_preds_of ctxt)
 
 val all_random_modes_of = all_modes_of Random
 
-fun defined_functions compilation thy name =
-  AList.defined (op =) (#function_names (the_pred_data thy name)) compilation
+fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
+    NONE => false
+  | SOME data => AList.defined (op =) (#function_names data) compilation
 
-fun lookup_predfun_data thy name mode =
+fun needs_random ctxt s m =
+  member (op =) (#needs_random (the_pred_data ctxt s)) m
+
+fun lookup_predfun_data ctxt name mode =
   Option.map rep_predfun_data
-    (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode)
+    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
 
-fun the_predfun_data thy name mode =
-  case lookup_predfun_data thy name mode of
+fun the_predfun_data ctxt name mode =
+  case lookup_predfun_data ctxt name mode of
     NONE => error ("No function defined for mode " ^ string_of_mode mode ^
       " of predicate " ^ name)
   | SOME data => data;
 
-val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of
+val predfun_definition_of = #definition ooo the_predfun_data
 
-val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of
+val predfun_intro_of = #intro ooo the_predfun_data
 
-val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of
+val predfun_elim_of = #elim ooo the_predfun_data
 
-val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of
+val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
 
 (* diagnostic display functions *)
 
-fun print_modes options thy modes =
+fun print_modes options modes =
   if show_modes options then
     tracing ("Inferred modes:\n" ^
       cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
         (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
   else ()
 
-fun print_pred_mode_table string_of_entry thy pred_mode_table =
+fun print_pred_mode_table string_of_entry pred_mode_table =
   let
     fun print_mode pred ((pol, mode), entry) =  "mode : " ^ string_of_mode mode
       ^ string_of_entry pred mode entry
@@ -307,35 +313,35 @@
     val _ = tracing (cat_lines (map print_pred pred_mode_table))
   in () end;
 
-fun string_of_prem thy (Prem t) =
-    (Syntax.string_of_term_global thy t) ^ "(premise)"
-  | string_of_prem thy (Negprem t) =
-    (Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)"
-  | string_of_prem thy (Sidecond t) =
-    (Syntax.string_of_term_global thy t) ^ "(sidecondition)"
-  | string_of_prem thy _ = raise Fail "string_of_prem: unexpected input"
+fun string_of_prem ctxt (Prem t) =
+    (Syntax.string_of_term ctxt t) ^ "(premise)"
+  | string_of_prem ctxt (Negprem t) =
+    (Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"
+  | string_of_prem ctxt (Sidecond t) =
+    (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
+  | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
 
-fun string_of_clause thy pred (ts, prems) =
+fun string_of_clause ctxt pred (ts, prems) =
   (space_implode " --> "
-  (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " "
-   ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
+  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
+   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
 
-fun print_compiled_terms options thy =
+fun print_compiled_terms options ctxt =
   if show_compilation options then
-    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
+    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
   else K ()
 
-fun print_stored_rules thy =
+fun print_stored_rules ctxt =
   let
-    val preds = (Graph.keys o PredData.get) thy
+    val preds = Graph.keys (PredData.get (ProofContext.theory_of ctxt))
     fun print pred () = let
       val _ = writeln ("predicate: " ^ pred)
       val _ = writeln ("introrules: ")
-      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
-        (rev (intros_of thy pred)) ()
+      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
+        (rev (intros_of ctxt pred)) ()
     in
-      if (has_elim thy pred) then
-        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
+      if (has_elim ctxt pred) then
+        writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred))
       else
         writeln ("no elimrule defined")
     end
@@ -343,7 +349,7 @@
     fold print preds ()
   end;
 
-fun print_all_modes compilation thy =
+fun print_all_modes compilation ctxt =
   let
     val _ = writeln ("Inferred modes:")
     fun print (pred, modes) u =
@@ -352,7 +358,7 @@
         val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
       in u end
   in
-    fold print (all_modes_of compilation thy) ()
+    fold print (all_modes_of compilation ctxt) ()
   end
 
 (* validity checks *)
@@ -575,12 +581,12 @@
       (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
     (Thm.transfer thy rule)
 
-fun preprocess_elim thy elimrule =
+fun preprocess_elim ctxt elimrule =
   let
     fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
      | replace_eqs t = t
-    val ctxt = ProofContext.init_global thy
+    val thy = ProofContext.theory_of ctxt
     val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
     val prems = Thm.prems_of elimrule
     val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
@@ -607,21 +613,21 @@
 
 val no_compilation = ([], ([], []))
 
-fun fetch_pred_data thy name =
-  case try (Inductive.the_inductive (ProofContext.init_global thy)) name of
+fun fetch_pred_data ctxt name =
+  case try (Inductive.the_inductive ctxt) name of
     SOME (info as (_, result)) => 
       let
         fun is_intro_of intro =
           let
             val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
-          in (fst (dest_Const const) = name) end;      
+          in (fst (dest_Const const) = name) end;
+        val thy = ProofContext.theory_of ctxt
         val intros =
           (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
         val index = find_index (fn s => s = name) (#names (fst info))
         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index
         val nparams = length (Inductive.params_of (#raw_induct result))
-        val ctxt = ProofContext.init_global thy
         val elim_t = mk_casesrule ctxt pred intros
         val elim =
           prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
@@ -635,16 +641,16 @@
     val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
-fun is_inductive_predicate thy name =
-  is_some (try (Inductive.the_inductive (ProofContext.init_global thy)) name)
+fun is_inductive_predicate ctxt name =
+  is_some (try (Inductive.the_inductive ctxt) name)
 
-fun depending_preds_of thy (key, value) =
+fun depending_preds_of ctxt (key, value) =
   let
     val intros = (#intros o rep_pred_data) value
   in
     fold Term.add_const_names (map Thm.prop_of intros) []
       |> filter (fn c => (not (c = key)) andalso
-        (is_inductive_predicate thy c orelse is_registered thy c))
+        (is_inductive_predicate ctxt c orelse is_registered ctxt c))
   end;
 
 fun add_intro thm thy =
@@ -667,7 +673,7 @@
 fun register_predicate (constname, pre_intros, pre_elim) thy =
   let
     val intros = map (preprocess_intro thy) pre_intros
-    val elim = preprocess_elim thy pre_elim
+    val elim = preprocess_elim (ProofContext.init_global thy) pre_elim
   in
     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
       PredData.map
@@ -725,9 +731,13 @@
       (mode * (compilation_funs -> typ -> term)) list -> bool));
 );
 
-fun alternative_compilation_of thy pred_name mode =
+fun alternative_compilation_of_global thy pred_name mode =
   AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
 
+fun alternative_compilation_of ctxt pred_name mode =
+  AList.lookup eq_mode
+    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
+
 fun force_modes_and_compilations pred_name compilations =
   let
     (* thm refl is a dummy thm *)
@@ -1157,10 +1167,10 @@
     in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 *)
 
-fun is_possible_output thy vs t =
+fun is_possible_output ctxt vs t =
   forall
     (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
-      (non_invertible_subterms (ProofContext.init_global thy) t)
+      (non_invertible_subterms ctxt t)
   andalso
     (forall (is_eqT o snd)
       (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
@@ -1176,7 +1186,7 @@
       []
   end
 
-fun is_constructable thy vs t = forall (member (op =) vs) (term_vs t)
+fun is_constructable vs t = forall (member (op =) vs) (term_vs t)
 
 fun missing_vars vs t = subtract (op =) vs (term_vs t)
 
@@ -1196,11 +1206,11 @@
       SOME ms => SOME (map (fn m => (Context m , [])) ms)
     | NONE => NONE)
 
-fun derivations_of (thy : theory) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
+fun derivations_of (ctxt : Proof.context) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
     map_product
       (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
-        (derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2)
-  | derivations_of thy modes vs t (m as Fun _) =
+        (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
+  | derivations_of ctxt modes vs t (m as Fun _) =
     (*let
       val (p, args) = strip_comb t
     in
@@ -1216,37 +1226,37 @@
         end) ms
       | NONE => (if is_all_input mode then [(Context mode, [])] else []))
     end*)
-    (case try (all_derivations_of thy modes vs) t  of
+    (case try (all_derivations_of ctxt modes vs) t  of
       SOME derivs =>
         filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
     | NONE => (if is_all_input m then [(Context m, [])] else []))
-  | derivations_of thy modes vs t m =
+  | derivations_of ctxt modes vs t m =
     if eq_mode (m, Input) then
       [(Term Input, missing_vars vs t)]
     else if eq_mode (m, Output) then
-      (if is_possible_output thy vs t then [(Term Output, [])] else [])
+      (if is_possible_output ctxt vs t then [(Term Output, [])] else [])
     else []
-and all_derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) =
+and all_derivations_of ctxt modes vs (Const ("Pair", _) $ t1 $ t2) =
   let
-    val derivs1 = all_derivations_of thy modes vs t1
-    val derivs2 = all_derivations_of thy modes vs t2
+    val derivs1 = all_derivations_of ctxt modes vs t1
+    val derivs2 = all_derivations_of ctxt modes vs t2
   in
     map_product
       (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
         derivs1 derivs2
   end
-  | all_derivations_of thy modes vs (t1 $ t2) =
+  | all_derivations_of ctxt modes vs (t1 $ t2) =
   let
-    val derivs1 = all_derivations_of thy modes vs t1
+    val derivs1 = all_derivations_of ctxt modes vs t1
   in
     maps (fn (d1, mvars1) =>
       case mode_of d1 of
         Fun (m', _) => map (fn (d2, mvars2) =>
-          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m')
+          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of ctxt modes vs t2 m')
         | _ => raise Fail "Something went wrong") derivs1
   end
-  | all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
-  | all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
+  | all_derivations_of _ modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
+  | all_derivations_of _ modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
   | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of"
 
 fun rev_option_ord ord (NONE, NONE) = EQUAL
@@ -1287,7 +1297,7 @@
       EQUAL => lexl_ord ords' (x, x')
     | ord => ord
 
-fun deriv_ord' thy pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   let
     (* prefer functional modes if it is a function *)
     fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
@@ -1295,7 +1305,7 @@
         fun is_functional t mode =
           case try (fst o dest_Const o fst o strip_comb) t of
             NONE => false
-          | SOME c => is_some (alternative_compilation_of thy c mode)
+          | SOME c => is_some (alternative_compilation_of ctxt c mode)
       in
         case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
           (true, true) => EQUAL
@@ -1325,7 +1335,7 @@
     ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
   end
 
-fun deriv_ord thy pol pred modes t = deriv_ord' thy pol pred modes t t
+fun deriv_ord ctxt pol pred modes t = deriv_ord' ctxt pol pred modes t t
 
 fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
   rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
@@ -1334,25 +1344,25 @@
   tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
     commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
 
-fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pred
+fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   pol (modes, (pos_modes, neg_modes)) vs ps =
   let
     fun choose_mode_of_prem (Prem t) = partial_hd
-        (sort (deriv_ord thy pol pred modes t) (all_derivations_of thy pos_modes vs t))
+        (sort (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t))
       | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
       | choose_mode_of_prem (Negprem t) = partial_hd
-          (sort (deriv_ord thy (not pol) pred modes t)
+          (sort (deriv_ord ctxt (not pol) pred modes t)
           (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
-             (all_derivations_of thy neg_modes vs t)))
-      | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
+             (all_derivations_of ctxt neg_modes vs t)))
+      | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem ctxt p)
   in
     if #reorder_premises mode_analysis_options then
-      partial_hd (sort (premise_ord thy pol pred modes) (ps ~~ map choose_mode_of_prem ps))
+      partial_hd (sort (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps))
     else
       SOME (hd ps, choose_mode_of_prem (hd ps))
   end
 
-fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy pred param_vs (modes :
+fun check_mode_clause' (mode_analysis_options : mode_analysis_options) ctxt pred param_vs (modes :
   (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   let
     val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
@@ -1367,7 +1377,7 @@
           val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
         in (modes, modes) end
     val (in_ts, out_ts) = split_mode mode ts
-    val in_vs = maps (vars_of_destructable_term (ProofContext.init_global thy)) in_ts
+    val in_vs = maps (vars_of_destructable_term ctxt) in_ts
     val out_vs = terms_vs out_ts
     fun known_vs_after p vs = (case p of
         Prem t => union (op =) vs (term_vs t)
@@ -1377,7 +1387,7 @@
     fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
       | check_mode_prems acc_ps rnd vs ps =
         (case
-          (select_mode_prem mode_analysis_options thy pred pol (modes', (pos_modes', neg_modes')) vs ps) of
+          (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of
           SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
             (known_vs_after p vs) (filter_out (equal p) ps)
         | SOME (p, SOME (deriv, missing_vars)) =>
@@ -1393,7 +1403,7 @@
     case check_mode_prems [] false in_vs ps of
       NONE => NONE
     | SOME (acc_ps, vs, rnd) =>
-      if forall (is_constructable thy vs) (in_ts @ out_ts) then
+      if forall (is_constructable vs) (in_ts @ out_ts) then
         SOME (ts, rev acc_ps, rnd)
       else
         if #use_random mode_analysis_options andalso pol then
@@ -1473,11 +1483,12 @@
 
 fun infer_modes mode_analysis_options options compilation preds all_modes param_vs clauses thy =
   let
+    val ctxt = ProofContext.init_global thy  
     val collect_errors = false
     fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
-    fun needs_random s (false, m) = ((false, m), false)
-      | needs_random s (true, m) = ((true, m), member (op =) (#needs_random (the_pred_data thy s)) m)
-    fun add_polarity_and_random_bit s b ms = map (fn m => needs_random s (b, m)) ms
+    fun add_needs_random s (false, m) = ((false, m), false)
+      | add_needs_random s (true, m) = ((true, m), needs_random ctxt s m)
+    fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
     val prednames = map fst preds
     (* extramodes contains all modes of all constants, should we only use the necessary ones
        - what is the impact on performance? *)
@@ -1492,15 +1503,13 @@
       if #infer_pos_and_neg_modes mode_analysis_options then
         let
           val pos_extra_modes =
-            map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+            map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
             relevant_prednames
-            (* all_modes_of compilation thy *)
             |> filter_out (fn (name, _) => member (op =) prednames name)
           val neg_extra_modes =
           map_filter (fn name => Option.map (pair name)
-            (try (modes_of (negative_compilation_of compilation) thy) name))
+            (try (modes_of (negative_compilation_of compilation) ctxt) name))
             relevant_prednames
-          (*all_modes_of (negative_compilation_of compilation) thy*)
             |> filter_out (fn (name, _) => member (op =) prednames name)
         in
           map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
@@ -1509,9 +1518,8 @@
         end
       else
         map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
-          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
             relevant_prednames
-          (*all_modes_of compilation thy*)
           |> filter_out (fn (name, _) => member (op =) prednames name))
     val _ = print_extra_modes options extra_modes
     val start_modes =
@@ -1521,7 +1529,7 @@
       else
         map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
     fun iteration modes = map
-      (check_modes_pred' mode_analysis_options options thy param_vs clauses
+      (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
         (modes @ extra_modes)) modes
     val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
       Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
@@ -1532,7 +1540,7 @@
           in (modes', errors @ flat new_errors) end) (start_modes, [])
         else
           (fixp (fn modes => map fst (iteration modes)) start_modes, []))
-    val moded_clauses = map (get_modes_pred' mode_analysis_options thy param_vs clauses
+    val moded_clauses = map (get_modes_pred' mode_analysis_options ctxt param_vs clauses
       (modes @ extra_modes)) modes
     val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
       set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
@@ -1671,11 +1679,11 @@
         (t, Term Input) => SOME t
       | (t, Term Output) => NONE
       | (Const (name, T), Context mode) =>
-        (case alternative_compilation_of (ProofContext.theory_of ctxt) name mode of
+        (case alternative_compilation_of ctxt name mode of
           SOME alt_comp => SOME (alt_comp compfuns T)
         | NONE =>
           SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
-            (ProofContext.theory_of ctxt) name mode,
+            ctxt name mode,
             Comp_Mod.funT_of compilation_modifiers mode T)))
       | (Free (s, T), Context m) =>
         SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
@@ -1813,7 +1821,7 @@
 
 (** switch detection analysis **)
 
-fun find_switch_test thy (i, is) (ts, prems) =
+fun find_switch_test ctxt (i, is) (ts, prems) =
   let
     val t = nth_pair is (nth ts i)
     val T = fastype_of t
@@ -1821,7 +1829,7 @@
     case T of
       TFree _ => NONE
     | Type (Tcon, _) =>
-      (case Datatype_Data.get_constrs thy Tcon of
+      (case Datatype_Data.get_constrs (ProofContext.theory_of ctxt) Tcon of
         NONE => NONE
       | SOME cs =>
         (case strip_comb t of
@@ -1830,11 +1838,11 @@
         | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
   end
 
-fun partition_clause thy pos moded_clauses =
+fun partition_clause ctxt pos moded_clauses =
   let
     fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
     fun find_switch_test' moded_clause (cases, left) =
-      case find_switch_test thy pos moded_clause of
+      case find_switch_test ctxt pos moded_clause of
         SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
       | NONE => (cases, moded_clause :: left)
   in
@@ -1844,12 +1852,12 @@
 datatype switch_tree =
   Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree
 
-fun mk_switch_tree thy mode moded_clauses =
+fun mk_switch_tree ctxt mode moded_clauses =
   let
     fun select_best_switch moded_clauses input_position best_switch =
       let
         val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd)))
-        val partition = partition_clause thy input_position moded_clauses
+        val partition = partition_clause ctxt input_position moded_clauses
         val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
       in
         case ord (switch, best_switch) of LESS => best_switch
@@ -1937,9 +1945,8 @@
 
 (* compilation of predicates *)
 
-fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
+fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
   let
-    val ctxt = ProofContext.init_global thy
     val compilation_modifiers = if pol then compilation_modifiers else
       negative_comp_modifiers_of compilation_modifiers
     val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
@@ -1967,7 +1974,7 @@
       if detect_switches options then
         the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
           (compile_switch compilation_modifiers ctxt all_vs param_vs additional_arguments
-            mode in_ts' outTs (mk_switch_tree thy mode moded_cls))
+            mode in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
       else
         let
           val cl_ts =
@@ -1983,7 +1990,7 @@
         end
     val fun_const =
       Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
-      (ProofContext.theory_of ctxt) s mode, funT)
+      ctxt s mode, funT)
   in
     HOLogic.mk_Trueprop
       (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -2044,7 +2051,7 @@
       (Free (x, T), x :: names)
     end
 
-fun create_intro_elim_rule mode defthm mode_id funT pred thy =
+fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
   let
     val funtrm = Const (mode_id, funT)
     val Ts = binder_types (fastype_of pred)
@@ -2072,11 +2079,11 @@
     val simprules = [defthm, @{thm eval_pred},
       @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
     val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
-    val introthm = Goal.prove (ProofContext.init_global thy)
+    val introthm = Goal.prove ctxt
       (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
     val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
     val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
-    val elimthm = Goal.prove (ProofContext.init_global thy)
+    val elimthm = Goal.prove ctxt
       (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
     val opt_neg_introthm =
       if is_all_input mode then
@@ -2090,7 +2097,7 @@
             Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
               (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
             THEN rtac @{thm Predicate.singleI} 1
-        in SOME (Goal.prove (ProofContext.init_global thy) (argnames @ hoarg_names') []
+        in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
             neg_introtrm (fn _ => tac))
         end
       else NONE
@@ -2131,8 +2138,9 @@
         val ([definition], thy') = thy |>
           Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
           PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+        val ctxt' = ProofContext.init_global thy'
         val rules as ((intro, elim), _) =
-          create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
+          create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
         in thy'
           |> set_function_name Pred name mode mode_cname
           |> add_predfun_data name mode (definition, rules)
@@ -2301,10 +2309,9 @@
 
 fun prove_sidecond ctxt t =
   let
-    val thy = ProofContext.theory_of ctxt
     fun preds_of t nameTs = case strip_comb t of 
       (f as Const (name, T), args) =>
-        if is_registered thy name then (name, T) :: nameTs
+        if is_registered ctxt name then (name, T) :: nameTs
           else fold preds_of args nameTs
       | _ => nameTs
     val preds = preds_of t []
@@ -2402,10 +2409,9 @@
 
 fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
   let
-    val thy = ProofContext.theory_of ctxt
     val T = the (AList.lookup (op =) preds pred)
     val nargs = length (binder_types T)
-    val pred_case_rule = the_elim_of thy pred
+    val pred_case_rule = the_elim_of ctxt pred
   in
     REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
     THEN print_tac options "before applying elim rule"
@@ -2495,7 +2501,7 @@
 fun prove_sidecond2 options ctxt t = let
   fun preds_of t nameTs = case strip_comb t of 
     (f as Const (name, T), args) =>
-      if is_registered (ProofContext.theory_of ctxt) name then (name, T) :: nameTs
+      if is_registered ctxt name then (name, T) :: nameTs
         else fold preds_of args nameTs
     | _ => nameTs
   val preds = preds_of t []
@@ -2512,7 +2518,7 @@
   
 fun prove_clause2 options ctxt pred mode (ts, ps) i =
   let
-    val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1)
+    val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
     val (in_ts, clause_out_ts) = split_mode mode ts;
     fun prove_prems2 out_ts [] =
       print_tac options "before prove_match2 - last call:"
@@ -2635,8 +2641,8 @@
   map (fn (pred, modes) =>
     (pred, map (fn (mode, value) => value) modes)) preds_modes_table
 
-fun compile_preds options comp_modifiers thy all_vs param_vs preds moded_clauses =
-  map_preds_modes (fn pred => compile_pred options comp_modifiers thy all_vs param_vs pred
+fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
+  map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
       (the (AList.lookup (op =) preds pred))) moded_clauses
 
 fun prove options thy clauses preds moded_clauses compiled_terms =
@@ -2649,25 +2655,25 @@
     compiled_terms
 
 (* preparation of introduction rules into special datastructures *)
-fun dest_prem thy params t =
+fun dest_prem ctxt params t =
   (case strip_comb t of
     (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
-  | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of
+  | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem ctxt params t of
       Prem t => Negprem t
     | Negprem _ => error ("Double negation not allowed in premise: " ^
-        Syntax.string_of_term_global thy (c $ t)) 
+        Syntax.string_of_term ctxt (c $ t)) 
     | Sidecond t => Sidecond (c $ t))
   | (c as Const (s, _), ts) =>
-    if is_registered thy s then Prem t else Sidecond t
+    if is_registered ctxt s then Prem t else Sidecond t
   | _ => Sidecond t)
 
 fun prepare_intrs options compilation thy prednames intros =
   let
+    val ctxt = ProofContext.init_global thy
     val intrs = map prop_of intros
     val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
     val (preds, intrs) = unify_consts thy preds intrs
-    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
-      (ProofContext.init_global thy)
+    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] ctxt
     val preds = map dest_Const preds
     val all_vs = terms_vs intrs
     val all_modes = 
@@ -2698,7 +2704,7 @@
     fun add_clause intr clauses =
       let
         val (Const (name, T), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
-        val prems = map (dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
+        val prems = map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
       in
         AList.update op = (name, these (AList.lookup op = clauses name) @
           [(ts, prems)]) clauses
@@ -2755,20 +2761,19 @@
 
 (* create code equation *)
 
-fun add_code_equations thy preds result_thmss =
+fun add_code_equations ctxt preds result_thmss =
   let
-    val ctxt = ProofContext.init_global thy
     fun add_code_equation (predname, T) (pred, result_thms) =
       let
         val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
       in
-        if member (op =) (modes_of Pred thy predname) full_mode then
+        if member (op =) (modes_of Pred ctxt predname) full_mode then
           let
             val Ts = binder_types T
             val arg_names = Name.variant_list []
               (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
             val args = map2 (curry Free) arg_names Ts
-            val predfun = Const (function_name_of Pred thy predname full_mode,
+            val predfun = Const (function_name_of Pred ctxt predname full_mode,
               Ts ---> PredicateCompFuns.mk_predT @{typ unit})
             val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
@@ -2794,7 +2799,7 @@
   define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
   prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
     -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
-  add_code_equations : theory -> (string * typ) list
+  add_code_equations : Proof.context -> (string * typ) list
     -> (string * thm list) list -> (string * thm list) list,
   comp_modifiers : Comp_Mod.comp_modifiers,
   use_random : bool,
@@ -2805,6 +2810,7 @@
   let
     fun dest_steps (Steps s) = s
     val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
+    val ctxt = ProofContext.init_global thy
     val _ = print_step options
       ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
         ^ ") for predicates " ^ commas prednames ^ "...")
@@ -2812,35 +2818,36 @@
       (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
     val _ =
       if show_intermediate_results options then
-        tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+        tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
       else ()
     val (preds, all_vs, param_vs, all_modes, clauses) =
-      prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
+      prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
     val _ = print_step options "Infering modes..."
     val ((moded_clauses, errors), thy') =
-      Output.cond_timeit true "Infering modes"
+      Output.cond_timeit (!Quickcheck.timing) "Infering modes"
       (fn _ => infer_modes mode_analysis_options
         options compilation preds all_modes param_vs clauses thy)
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes preds options modes
     (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
-    val _ = print_modes options thy' modes
+    val _ = print_modes options modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =
       Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
       (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
       |> Theory.checkpoint)
+    val ctxt'' = ProofContext.init_global thy''
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
       Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
         compile_preds options
-          (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses)
-    val _ = print_compiled_terms options thy'' compiled_terms
+          (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
+    val _ = print_compiled_terms options ctxt'' compiled_terms
     val _ = print_step options "Proving equations..."
     val result_thms =
       Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
       #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
-    val result_thms' = #add_code_equations (dest_steps steps) thy'' preds
+    val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
       (maps_modes result_thms)
     val qname = #qname (dest_steps steps)
     val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
@@ -2873,8 +2880,9 @@
   let
     fun dest_steps (Steps s) = s
     val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
+    val ctxt = ProofContext.init_global thy
     val thy' = thy
-      |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names)
+      |> PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names)
       |> Theory.checkpoint;
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -2882,7 +2890,7 @@
     
     val thy'' = fold_rev
       (fn preds => fn thy =>
-        if not (forall (defined thy) preds) then
+        if not (forall (defined (ProofContext.init_global thy)) preds) then
           let
             val mode_analysis_options = {use_random = #use_random (dest_steps steps),
               reorder_premises =
@@ -3025,15 +3033,17 @@
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
+    val ctxt = ProofContext.init_global thy
     val lthy' = Local_Theory.theory (PredData.map
-        (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
+        (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
     val thy' = ProofContext.theory_of lthy'
-    val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
+    val ctxt' = ProofContext.init_global thy'
+    val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
     fun mk_cases const =
       let
         val T = Sign.the_const_type thy const
         val pred = Const (const, T)
-        val intros = intros_of thy' const
+        val intros = intros_of ctxt' const
       in mk_casesrule lthy' pred intros end  
     val cases_rules = map mk_cases preds
     val cases =
@@ -3083,11 +3093,11 @@
       (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
-fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
+fun analyze_compr ctxt compfuns param_user_modes (compilation, arguments) t_compr =
   let
     val all_modes_of = all_modes_of compilation
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
-      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
+      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
     val (body, Ts, fp) = HOLogic.strip_psplits split;
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
@@ -3098,9 +3108,9 @@
     val (pred as Const (name, T), all_args) =
       case strip_comb body of
         (Const (name, T), all_args) => (Const (name, T), all_args)
-      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term_global thy head)
+      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
   in
-    if defined_functions compilation thy name then
+    if defined_functions compilation ctxt name then
       let
         fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
           | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
@@ -3123,9 +3133,13 @@
                   instance_of (m1, Input) andalso instance_of (m2, Input)
               | instance_of (Pair (m1, m2), Output) =
                   instance_of (m1, Output) andalso instance_of (m2, Output)
+              | instance_of (Input, Pair (m1, m2)) =
+                  instance_of (Input, m1) andalso instance_of (Input, m2)
+              | instance_of (Output, Pair (m1, m2)) =
+                  instance_of (Output, m1) andalso instance_of (Output, m2)
               | instance_of _ = false
           in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end
-        val derivs = all_derivations_of thy (all_modes_of thy) [] body
+        val derivs = all_derivations_of ctxt (all_modes_of ctxt) [] body
           |> filter (fn (d, missing_vars) =>
             let
               val (p_mode :: modes) = collect_context_modes d
@@ -3137,10 +3151,10 @@
           |> map fst
         val deriv = case derivs of
             [] => error ("No mode possible for comprehension "
-                    ^ Syntax.string_of_term_global thy t_compr)
+                    ^ Syntax.string_of_term ctxt t_compr)
           | [d] => d
           | d :: _ :: _ => (warning ("Multiple modes possible for comprehension "
-                    ^ Syntax.string_of_term_global thy t_compr); d);
+                    ^ Syntax.string_of_term ctxt t_compr); d);
         val (_, outargs) = split_mode (head_mode_of deriv) all_args
         val additional_arguments =
           case compilation of
@@ -3164,7 +3178,7 @@
           | DSeq => dseq_comp_modifiers
           | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
           | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
-        val t_pred = compile_expr comp_modifiers (ProofContext.init_global thy)
+        val t_pred = compile_expr comp_modifiers ctxt
           (body, deriv) additional_arguments;
         val T_pred = dest_predT compfuns (fastype_of t_pred)
         val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
@@ -3175,7 +3189,7 @@
       error "Evaluation with values is not possible because compilation with code_pred was not invoked"
   end
 
-fun eval thy stats param_user_modes (options as (compilation, arguments)) k t_compr =
+fun eval ctxt stats param_user_modes (options as (compilation, arguments)) k t_compr =
   let
     fun count xs x =
       let
@@ -3190,7 +3204,7 @@
       | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
       | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
       | _ => PredicateCompFuns.compfuns
-    val t = analyze_compr thy compfuns param_user_modes options t_compr;
+    val t = analyze_compr ctxt compfuns param_user_modes options t_compr;
     val T = dest_predT compfuns (fastype_of t);
     val t' =
       if stats andalso compilation = New_Pos_Random_DSeq then
@@ -3199,6 +3213,7 @@
             @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
       else
         mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
+    val thy = ProofContext.theory_of ctxt
     val (ts, statistics) =
       case compilation of
        (* Random =>
@@ -3250,8 +3265,7 @@
 
 fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
   let
-    val thy = ProofContext.theory_of ctxt
-    val ((T, ts), statistics) = eval thy stats param_user_modes comp_options k t_compr
+    val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
     val cont = Free ("...", setT)

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu May 20 16:25:22 2010 +0200
@@ -253,8 +253,9 @@
 
 fun obtain_specification_graph options thy t =
   let
+    val ctxt = ProofContext.init_global thy
     fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
-    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c
+    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c
     fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
     fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
     fun defiants_of specs =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu May 20 16:25:22 2010 +0200
@@ -216,12 +216,13 @@
     (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
     val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
     val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
-    val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname
+    val ctxt4 = ProofContext.init_global thy4
+    val modes = Predicate_Compile_Core.modes_of compilation ctxt4 full_constname
     val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
     val prog =
       if member eq_mode modes output_mode then
         let
-          val name = Predicate_Compile_Core.function_name_of compilation thy4
+          val name = Predicate_Compile_Core.function_name_of compilation ctxt4
             full_constname output_mode
           val T = 
             case compilation of

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu May 20 16:25:22 2010 +0200
@@ -181,7 +181,7 @@
                     if member (op =) ((map fst specs) @ black_list) pred_name then
                       thy
                     else
-                      (case try (Predicate_Compile_Core.intros_of thy) pred_name of
+                      (case try (Predicate_Compile_Core.intros_of (ProofContext.init_global thy)) pred_name of
                         NONE => thy
                       | SOME [] => thy
                       | SOME intros =>

--- a/src/HOLCF/Fixrec.thy	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOLCF/Fixrec.thy	Thu May 20 16:25:22 2010 +0200
@@ -65,30 +65,6 @@
     == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
 
 
-subsubsection {* Monadic bind operator *}
-
-definition
-  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
-  "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
-
-text {* monad laws *}
-
-lemma bind_strict [simp]: "bind\<cdot>\<bottom>\<cdot>f = \<bottom>"
-by (simp add: bind_def)
-
-lemma bind_fail [simp]: "bind\<cdot>fail\<cdot>f = fail"
-by (simp add: bind_def)
-
-lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a"
-by (simp add: bind_def)
-
-lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m"
-by (rule_tac p=m in maybeE, simp_all)
-
-lemma bind_assoc:
- "bind\<cdot>(bind\<cdot>m\<cdot>k)\<cdot>h = bind\<cdot>m\<cdot>(\<Lambda> a. bind\<cdot>(k\<cdot>a)\<cdot>h)"
-by (rule_tac p=m in maybeE, simp_all)
-
 subsubsection {* Run operator *}
 
 definition
@@ -169,7 +145,7 @@
 
 definition
   branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
-  "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
+  "branch p \<equiv> \<Lambda> r x. maybe_when\<cdot>fail\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
 
 lemma branch_rews:
   "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
@@ -277,7 +253,7 @@
 definition
   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
   "cpair_pat p1 p2 = (\<Lambda>(x, y).
-    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>(a, b))))"
+    maybe_when\<cdot>fail\<cdot>(\<Lambda> a. maybe_when\<cdot>fail\<cdot>(\<Lambda> b. return\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
 
 definition
   spair_pat ::
@@ -425,7 +401,7 @@
 
 definition
   as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
-  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>(x, a)))"
+  "as_pat p = (\<Lambda> x. maybe_when\<cdot>fail\<cdot>(\<Lambda> a. return\<cdot>(x, a))\<cdot>(p\<cdot>x))"
 
 definition
   lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
@@ -608,7 +584,7 @@
       (@{const_name UU}, @{const_name match_UU}) ]
 *}
 
-hide_const (open) return bind fail run cases
+hide_const (open) return fail run cases
 
 lemmas [fixrec_simp] =
   run_strict run_fail run_return

--- a/src/HOLCF/IsaMakefile	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOLCF/IsaMakefile	Thu May 20 16:25:22 2010 +0200
@@ -7,6 +7,7 @@
 default: HOLCF
 images: HOLCF IOA
 test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \
+  HOLCF-Tutorial \
       IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex
 all: images test
 
@@ -78,6 +79,19 @@
 	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
 
 
+## HOLCF-Tutorial
+
+HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
+
+$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
+  Tutorial/Domain_ex.thy \
+  Tutorial/Fixrec_ex.thy \
+  Tutorial/New_Domain.thy \
+  Tutorial/document/root.tex \
+  Tutorial/ROOT.ML
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
+
+
 ## HOLCF-IMP
 
 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
@@ -95,15 +109,12 @@
   ../HOL/Library/Nat_Infinity.thy \
   ex/Dagstuhl.thy \
   ex/Dnat.thy \
-  ex/Domain_ex.thy \
   ex/Domain_Proofs.thy \
   ex/Fix2.thy \
-  ex/Fixrec_ex.thy \
   ex/Focus_ex.thy \
   ex/Hoare.thy \
   ex/Letrec.thy \
   ex/Loop.thy \
-  ex/New_Domain.thy \
   ex/Powerdomain_ex.thy \
   ex/Stream.thy \
   ex/Strict_Fun.thy \
@@ -201,4 +212,4 @@
 	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
 	  $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
 	  $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz	\
-	  $(LOG)/IOA-ex.gz
+	  $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz

--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu May 20 16:25:22 2010 +0200
@@ -952,7 +952,7 @@
           val (fun1, fun2, taken) = pat_lhs (pat, args);
           val defs = @{thm branch_def} :: pat_defs;
           val goal = mk_trp (mk_strict fun1);
-          val rules = @{thm Fixrec.bind_strict} :: case_rews;
+          val rules = @{thms maybe_when_rews} @ case_rews;
           val tacs = [simp_tac (beta_ss addsimps rules) 1];
         in prove thy defs goal (K tacs) end;
       fun pat_apps (i, (pat, (con, args))) =
@@ -967,7 +967,7 @@
               val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
               val goal = Logic.list_implies (assms, concl);
               val defs = @{thm branch_def} :: pat_defs;
-              val rules = @{thms bind_fail left_unit} @ case_rews;
+              val rules = @{thms maybe_when_rews} @ case_rews;
               val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
             in prove thy defs goal (K tacs) end;
         in map_index pat_app spec end;

--- a/src/HOLCF/Tools/fixrec.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Thu May 20 16:25:22 2010 +0200
@@ -125,10 +125,20 @@
     val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
     val functional = lambda_tuple lhss (mk_tuple rhss);
     val fixpoint = mk_fix (mk_cabs functional);
-    
+
     val cont_thm =
-      Goal.prove lthy [] [] (mk_trp (mk_cont functional))
-        (K (simp_tac (simpset_of lthy) 1));
+      let
+        val prop = mk_trp (mk_cont functional);
+        fun err () = error (
+          "Continuity proof failed; please check that cont2cont rules\n" ^
+          "are configured for all non-HOLCF constants.\n" ^
+          "The error occurred for the goal statement:\n" ^
+          Syntax.string_of_term lthy prop);
+        fun check th = case Thm.nprems_of th of 0 => all_tac th | n => err ();
+        val tac = simp_tac (simpset_of lthy) 1 THEN check;
+      in
+        Goal.prove lthy [] [] prop (K tac)
+      end;
 
     fun one_def (l as Free(n,_)) r =
           let val b = Long_Name.base_name n

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/Domain_ex.thy	Thu May 20 16:25:22 2010 +0200
@@ -0,0 +1,211 @@
+(*  Title:      HOLCF/ex/Domain_ex.thy
+    Author:     Brian Huffman
+*)
+
+header {* Domain package examples *}
+
+theory Domain_ex
+imports HOLCF
+begin
+
+text {* Domain constructors are strict by default. *}
+
+domain d1 = d1a | d1b "d1" "d1"
+
+lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
+
+text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
+
+domain d2 = d2a | d2b (lazy "d2")
+
+lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
+
+text {* Strict and lazy arguments may be mixed arbitrarily. *}
+
+domain d3 = d3a | d3b (lazy "d2") "d2"
+
+lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
+
+text {* Selectors can be used with strict or lazy constructor arguments. *}
+
+domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
+
+lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
+
+text {* Mixfix declarations can be given for data constructors. *}
+
+domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
+
+lemma "d5a \<noteq> x :#: y :#: z" by simp
+
+text {* Mixfix declarations can also be given for type constructors. *}
+
+domain ('a, 'b) lazypair (infixl ":*:" 25) =
+  lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
+
+lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
+by (rule allI, case_tac p, simp_all)
+
+text {* Non-recursive constructor arguments can have arbitrary types. *}
+
+domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
+
+text {*
+  Indirect recusion is allowed for sums, products, lifting, and the
+  continuous function space.  However, the domain package does not
+  generate an induction rule in terms of the constructors.
+*}
+
+domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
+  -- "Indirect recursion detected, skipping proofs of (co)induction rules"
+
+text {* Note that @{text d7.induct} is absent. *}
+
+text {*
+  Indirect recursion is also allowed using previously-defined datatypes.
+*}
+
+domain 'a slist = SNil | SCons 'a "'a slist"
+
+domain 'a stree = STip | SBranch "'a stree slist"
+
+text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
+
+domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
+
+text {* Non-regular recursion is not allowed. *}
+(*
+domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
+  -- "illegal direct recursion with different arguments"
+domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
+  -- "illegal direct recursion with different arguments"
+*)
+
+text {*
+  Mutually-recursive datatypes must have all the same type arguments,
+  not necessarily in the same order.
+*}
+
+domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
+   and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
+
+text {* Induction rules for flat datatypes have no admissibility side-condition. *}
+
+domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
+
+lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
+by (rule flattree.induct) -- "no admissibility requirement"
+
+text {* Trivial datatypes will produce a warning message. *}
+
+domain triv = Triv triv triv
+  -- "domain @{text Domain_ex.triv} is empty!"
+
+lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
+
+text {* Lazy constructor arguments may have unpointed types. *}
+
+domain natlist = nnil | ncons (lazy "nat discr") natlist
+
+text {* Class constraints may be given for type parameters on the LHS. *}
+
+domain ('a::cpo) box = Box (lazy 'a)
+
+
+subsection {* Generated constants and theorems *}
+
+domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
+
+lemmas tree_abs_defined_iff =
+  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
+
+text {* Rules about ismorphism *}
+term tree_rep
+term tree_abs
+thm tree.rep_iso
+thm tree.abs_iso
+thm tree.iso_rews
+
+text {* Rules about constructors *}
+term Leaf
+term Node
+thm Leaf_def Node_def
+thm tree.nchotomy
+thm tree.exhaust
+thm tree.compacts
+thm tree.con_rews
+thm tree.dist_les
+thm tree.dist_eqs
+thm tree.inverts
+thm tree.injects
+
+text {* Rules about case combinator *}
+term tree_when
+thm tree.tree_when_def
+thm tree.when_rews
+
+text {* Rules about selectors *}
+term left
+term right
+thm tree.sel_rews
+
+text {* Rules about discriminators *}
+term is_Leaf
+term is_Node
+thm tree.dis_rews
+
+text {* Rules about pattern match combinators *}
+term Leaf_pat
+term Node_pat
+thm tree.pat_rews
+
+text {* Rules about monadic pattern match combinators *}
+term match_Leaf
+term match_Node
+thm tree.match_rews
+
+text {* Rules about take function *}
+term tree_take
+thm tree.take_def
+thm tree.take_0
+thm tree.take_Suc
+thm tree.take_rews
+thm tree.chain_take
+thm tree.take_take
+thm tree.deflation_take
+thm tree.take_below
+thm tree.take_lemma
+thm tree.lub_take
+thm tree.reach
+thm tree.finite_induct
+
+text {* Rules about finiteness predicate *}
+term tree_finite
+thm tree.finite_def
+thm tree.finite (* only generated for flat datatypes *)
+
+text {* Rules about bisimulation predicate *}
+term tree_bisim
+thm tree.bisim_def
+thm tree.coinduct
+
+text {* Induction rule *}
+thm tree.induct
+
+
+subsection {* Known bugs *}
+
+text {* Declaring a mixfix with spaces causes some strange parse errors. *}
+(*
+domain xx = xx ("x y")
+  -- "Inner syntax error: unexpected end of input"
+*)
+
+text {*
+  Non-cpo type parameters currently do not work.
+*}
+(*
+domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
+*)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/Fixrec_ex.thy	Thu May 20 16:25:22 2010 +0200
@@ -0,0 +1,246 @@
+(*  Title:      HOLCF/ex/Fixrec_ex.thy
+    Author:     Brian Huffman
+*)
+
+header {* Fixrec package examples *}
+
+theory Fixrec_ex
+imports HOLCF
+begin
+
+subsection {* Basic @{text fixrec} examples *}
+
+text {*
+  Fixrec patterns can mention any constructor defined by the domain
+  package, as well as any of the following built-in constructors:
+  Pair, spair, sinl, sinr, up, ONE, TT, FF.
+*}
+
+text {* Typical usage is with lazy constructors. *}
+
+fixrec down :: "'a u \<rightarrow> 'a"
+where "down\<cdot>(up\<cdot>x) = x"
+
+text {* With strict constructors, rewrite rules may require side conditions. *}
+
+fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
+where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
+
+text {* Lifting can turn a strict constructor into a lazy one. *}
+
+fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
+where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
+
+text {* Fixrec also works with the HOL pair constructor. *}
+
+fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
+where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
+
+
+subsection {* Examples using @{text fixrec_simp} *}
+
+text {* A type of lazy lists. *}
+
+domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
+
+text {* A zip function for lazy lists. *}
+
+text {* Notice that the patterns are not exhaustive. *}
+
+fixrec
+  lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
+where
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+| "lzip\<cdot>lNil\<cdot>lNil = lNil"
+
+text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
+text {* Note that pattern matching is done in left-to-right order. *}
+
+lemma lzip_stricts [simp]:
+  "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
+  "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp+
+
+text {* @{text fixrec_simp} can also produce rules for missing cases. *}
+
+lemma lzip_undefs [simp]:
+  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
+by fixrec_simp+
+
+
+subsection {* Pattern matching with bottoms *}
+
+text {*
+  As an alternative to using @{text fixrec_simp}, it is also possible
+  to use bottom as a constructor pattern.  When using a bottom
+  pattern, the right-hand-side must also be bottom; otherwise, @{text
+  fixrec} will not be able to prove the equation.
+*}
+
+fixrec
+  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
+where
+  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
+| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
+
+text {*
+  If the function is already strict in that argument, then the bottom
+  pattern does not change the meaning of the function.  For example,
+  in the definition of @{term from_sinr_up}, the first equation is
+  actually redundant, and could have been proven separately by
+  @{text fixrec_simp}.
+*}
+
+text {*
+  A bottom pattern can also be used to make a function strict in a
+  certain argument, similar to a bang-pattern in Haskell.
+*}
+
+fixrec
+  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
+where
+  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
+| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
+
+
+subsection {* Skipping proofs of rewrite rules *}
+
+text {* Another zip function for lazy lists. *}
+
+text {*
+  Notice that this version has overlapping patterns.
+  The second equation cannot be proved as a theorem
+  because it only applies when the first pattern fails.
+*}
+
+fixrec (permissive)
+  lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
+where
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+| "lzip2\<cdot>xs\<cdot>ys = lNil"
+
+text {*
+  Usually fixrec tries to prove all equations as theorems.
+  The "permissive" option overrides this behavior, so fixrec
+  does not produce any simp rules.
+*}
+
+text {* Simp rules can be generated later using @{text fixrec_simp}. *}
+
+lemma lzip2_simps [simp]:
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
+  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
+  "lzip2\<cdot>lNil\<cdot>lNil = lNil"
+by fixrec_simp+
+
+lemma lzip2_stricts [simp]:
+  "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp+
+
+
+subsection {* Mutual recursion with @{text fixrec} *}
+
+text {* Tree and forest types. *}
+
+domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
+and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
+
+text {*
+  To define mutually recursive functions, give multiple type signatures
+  separated by the keyword @{text "and"}.
+*}
+
+fixrec
+  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
+and
+  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
+where
+  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
+| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
+| "map_forest\<cdot>f\<cdot>Empty = Empty"
+| "ts \<noteq> \<bottom> \<Longrightarrow>
+    map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
+
+lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+(*
+  Theorems generated:
+  @{text map_tree_def}  @{thm map_tree_def}
+  @{text map_forest_def}  @{thm map_forest_def}
+  @{text map_tree.unfold}  @{thm map_tree.unfold}
+  @{text map_forest.unfold}  @{thm map_forest.unfold}
+  @{text map_tree.simps}  @{thm map_tree.simps}
+  @{text map_forest.simps}  @{thm map_forest.simps}
+  @{text map_tree_map_forest.induct}  @{thm map_tree_map_forest.induct}
+*)
+
+
+subsection {* Looping simp rules *}
+
+text {*
+  The defining equations of a fixrec definition are declared as simp
+  rules by default.  In some cases, especially for constants with no
+  arguments or functions with variable patterns, the defining
+  equations may cause the simplifier to loop.  In these cases it will
+  be necessary to use a @{text "[simp del]"} declaration.
+*}
+
+fixrec
+  repeat :: "'a \<rightarrow> 'a llist"
+where
+  [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
+
+text {*
+  We can derive other non-looping simp rules for @{const repeat} by
+  using the @{text subst} method with the @{text repeat.simps} rule.
+*}
+
+lemma repeat_simps [simp]:
+  "repeat\<cdot>x \<noteq> \<bottom>"
+  "repeat\<cdot>x \<noteq> lNil"
+  "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
+by (subst repeat.simps, simp)+
+
+lemma llist_when_repeat [simp]:
+  "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
+by (subst repeat.simps, simp)
+
+text {*
+  For mutually-recursive constants, looping might only occur if all
+  equations are in the simpset at the same time.  In such cases it may
+  only be necessary to declare @{text "[simp del]"} on one equation.
+*}
+
+fixrec
+  inf_tree :: "'a tree" and inf_forest :: "'a forest"
+where
+  [simp del]: "inf_tree = Branch\<cdot>inf_forest"
+| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
+
+
+subsection {* Using @{text fixrec} inside locales *}
+
+locale test =
+  fixes foo :: "'a \<rightarrow> 'a"
+  assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
+begin
+
+fixrec
+  bar :: "'a u \<rightarrow> 'a"
+where
+  "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
+
+lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+end
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/New_Domain.thy	Thu May 20 16:25:22 2010 +0200
@@ -0,0 +1,92 @@
+(*  Title:      HOLCF/ex/New_Domain.thy
+    Author:     Brian Huffman
+*)
+
+header {* Definitional domain package *}
+
+theory New_Domain
+imports HOLCF
+begin
+
+text {*
+  The definitional domain package only works with representable domains,
+  i.e. types in class @{text rep}.
+*}
+
+default_sort rep
+
+text {*
+  Provided that @{text rep} is the default sort, the @{text new_domain}
+  package should work with any type definition supported by the old
+  domain package.
+*}
+
+new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+
+text {*
+  The difference is that the new domain package is completely
+  definitional, and does not generate any axioms.  The following type
+  and constant definitions are not produced by the old domain package.
+*}
+
+thm type_definition_llist
+thm llist_abs_def llist_rep_def
+
+text {*
+  The new domain package also adds support for indirect recursion with
+  user-defined datatypes.  This definition of a tree datatype uses
+  indirect recursion through the lazy list type constructor.
+*}
+
+new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+
+text {*
+  For indirect-recursive definitions, the domain package is not able to
+  generate a high-level induction rule.  (It produces a warning
+  message instead.)  The low-level reach lemma (now proved as a
+  theorem, no longer generated as an axiom) can be used to derive
+  other induction rules.
+*}
+
+thm ltree.reach
+
+text {*
+  The definition of the take function uses map functions associated with
+  each type constructor involved in the definition.  A map function
+  for the lazy list type has been generated by the new domain package.
+*}
+
+thm ltree.take_rews
+thm llist_map_def
+
+lemma ltree_induct:
+  fixes P :: "'a ltree \<Rightarrow> bool"
+  assumes adm: "adm P"
+  assumes bot: "P \<bottom>"
+  assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
+  assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
+  shows "P x"
+proof -
+  have "P (\<Squnion>i. ltree_take i\<cdot>x)"
+  using adm
+  proof (rule admD)
+    fix i
+    show "P (ltree_take i\<cdot>x)"
+    proof (induct i arbitrary: x)
+      case (0 x)
+      show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
+    next
+      case (Suc n x)
+      show "P (ltree_take (Suc n)\<cdot>x)"
+        apply (cases x)
+        apply (simp add: bot)
+        apply (simp add: Leaf)
+        apply (simp add: Branch Suc)
+        done
+    qed
+  qed (simp add: ltree.chain_take)
+  thus ?thesis
+    by (simp add: ltree.reach)
+qed
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/ROOT.ML	Thu May 20 16:25:22 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["Domain_ex", "Fixrec_ex", "New_Domain"];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/document/root.tex	Thu May 20 16:25:22 2010 +0200
@@ -0,0 +1,29 @@
+
+% HOLCF/document/root.tex
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage[latin1]{inputenc}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+%\isabellestyle{it}
+\pagestyle{myheadings}
+
+\begin{document}
+
+\title{Isabelle/HOLCF Tutorial}
+\maketitle
+
+\tableofcontents
+
+%\newpage
+
+%\renewcommand{\isamarkupheader}[1]%
+%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\end{document}

--- a/src/HOLCF/ex/Domain_ex.thy	Thu May 20 16:22:50 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,210 +0,0 @@
-(*  Title:      HOLCF/ex/Domain_ex.thy
-    Author:     Brian Huffman
-*)
-
-header {* Domain package examples *}
-
-theory Domain_ex
-imports HOLCF
-begin
-
-text {* Domain constructors are strict by default. *}
-
-domain d1 = d1a | d1b "d1" "d1"
-
-lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
-
-text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
-
-domain d2 = d2a | d2b (lazy "d2")
-
-lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
-
-text {* Strict and lazy arguments may be mixed arbitrarily. *}
-
-domain d3 = d3a | d3b (lazy "d2") "d2"
-
-lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
-
-text {* Selectors can be used with strict or lazy constructor arguments. *}
-
-domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
-
-lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
-
-text {* Mixfix declarations can be given for data constructors. *}
-
-domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
-
-lemma "d5a \<noteq> x :#: y :#: z" by simp
-
-text {* Mixfix declarations can also be given for type constructors. *}
-
-domain ('a, 'b) lazypair (infixl ":*:" 25) =
-  lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
-
-lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
-by (rule allI, case_tac p, simp_all)
-
-text {* Non-recursive constructor arguments can have arbitrary types. *}
-
-domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
-
-text {*
-  Indirect recusion is allowed for sums, products, lifting, and the
-  continuous function space.  However, the domain package does not
-  generate an induction rule in terms of the constructors.
-*}
-
-domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
-  -- "Indirect recursion detected, skipping proofs of (co)induction rules"
-(* d7.induct is absent *)
-
-text {*
-  Indirect recursion is also allowed using previously-defined datatypes.
-*}
-
-domain 'a slist = SNil | SCons 'a "'a slist"
-
-domain 'a stree = STip | SBranch "'a stree slist"
-
-text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
-
-domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
-
-text {* Non-regular recursion is not allowed. *}
-(*
-domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
-  -- "illegal direct recursion with different arguments"
-domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
-  -- "illegal direct recursion with different arguments"
-*)
-
-text {*
-  Mutually-recursive datatypes must have all the same type arguments,
-  not necessarily in the same order.
-*}
-
-domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
-   and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
-
-text {* Induction rules for flat datatypes have no admissibility side-condition. *}
-
-domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
-
-lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
-by (rule flattree.induct) -- "no admissibility requirement"
-
-text {* Trivial datatypes will produce a warning message. *}
-
-domain triv = Triv triv triv
-  -- "domain Domain_ex.triv is empty!"
-
-lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
-
-text {* Lazy constructor arguments may have unpointed types. *}
-
-domain natlist = nnil | ncons (lazy "nat discr") natlist
-
-text {* Class constraints may be given for type parameters on the LHS. *}
-
-domain ('a::cpo) box = Box (lazy 'a)
-
-
-subsection {* Generated constants and theorems *}
-
-domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
-
-lemmas tree_abs_defined_iff =
-  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
-
-text {* Rules about ismorphism *}
-term tree_rep
-term tree_abs
-thm tree.rep_iso
-thm tree.abs_iso
-thm tree.iso_rews
-
-text {* Rules about constructors *}
-term Leaf
-term Node
-thm Leaf_def Node_def
-thm tree.nchotomy
-thm tree.exhaust
-thm tree.compacts
-thm tree.con_rews
-thm tree.dist_les
-thm tree.dist_eqs
-thm tree.inverts
-thm tree.injects
-
-text {* Rules about case combinator *}
-term tree_when
-thm tree.tree_when_def
-thm tree.when_rews
-
-text {* Rules about selectors *}
-term left
-term right
-thm tree.sel_rews
-
-text {* Rules about discriminators *}
-term is_Leaf
-term is_Node
-thm tree.dis_rews
-
-text {* Rules about pattern match combinators *}
-term Leaf_pat
-term Node_pat
-thm tree.pat_rews
-
-text {* Rules about monadic pattern match combinators *}
-term match_Leaf
-term match_Node
-thm tree.match_rews
-
-text {* Rules about take function *}
-term tree_take
-thm tree.take_def
-thm tree.take_0
-thm tree.take_Suc
-thm tree.take_rews
-thm tree.chain_take
-thm tree.take_take
-thm tree.deflation_take
-thm tree.take_below
-thm tree.take_lemma
-thm tree.lub_take
-thm tree.reach
-thm tree.finite_induct
-
-text {* Rules about finiteness predicate *}
-term tree_finite
-thm tree.finite_def
-thm tree.finite (* only generated for flat datatypes *)
-
-text {* Rules about bisimulation predicate *}
-term tree_bisim
-thm tree.bisim_def
-thm tree.coinduct
-
-text {* Induction rule *}
-thm tree.induct
-
-
-subsection {* Known bugs *}
-
-text {* Declaring a mixfix with spaces causes some strange parse errors. *}
-(*
-domain xx = xx ("x y")
-  -- "Inner syntax error: unexpected end of input"
-*)
-
-text {*
-  Non-cpo type parameters currently do not work.
-*}
-(*
-domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
-*)
-
-end

--- a/src/HOLCF/ex/Fixrec_ex.thy	Thu May 20 16:22:50 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,203 +0,0 @@
-(*  Title:      HOLCF/ex/Fixrec_ex.thy
-    Author:     Brian Huffman
-*)
-
-header {* Fixrec package examples *}
-
-theory Fixrec_ex
-imports HOLCF
-begin
-
-subsection {* Basic @{text fixrec} examples *}
-
-text {*
-  Fixrec patterns can mention any constructor defined by the domain
-  package, as well as any of the following built-in constructors:
-  Pair, spair, sinl, sinr, up, ONE, TT, FF.
-*}
-
-text {* Typical usage is with lazy constructors. *}
-
-fixrec down :: "'a u \<rightarrow> 'a"
-where "down\<cdot>(up\<cdot>x) = x"
-
-text {* With strict constructors, rewrite rules may require side conditions. *}
-
-fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
-where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
-
-text {* Lifting can turn a strict constructor into a lazy one. *}
-
-fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
-where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
-
-text {* Fixrec also works with the HOL pair constructor. *}
-
-fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
-where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
-
-
-subsection {* Examples using @{text fixrec_simp} *}
-
-text {* A type of lazy lists. *}
-
-domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
-
-text {* A zip function for lazy lists. *}
-
-text {* Notice that the patterns are not exhaustive. *}
-
-fixrec
-  lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
-where
-  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-| "lzip\<cdot>lNil\<cdot>lNil = lNil"
-
-text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
-text {* Note that pattern matching is done in left-to-right order. *}
-
-lemma lzip_stricts [simp]:
-  "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
-  "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
-  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp+
-
-text {* @{text fixrec_simp} can also produce rules for missing cases. *}
-
-lemma lzip_undefs [simp]:
-  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
-  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
-by fixrec_simp+
-
-
-subsection {* Pattern matching with bottoms *}
-
-text {*
-  As an alternative to using @{text fixrec_simp}, it is also possible
-  to use bottom as a constructor pattern.  When using a bottom
-  pattern, the right-hand-side must also be bottom; otherwise, @{text
-  fixrec} will not be able to prove the equation.
-*}
-
-fixrec
-  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
-where
-  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
-| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
-
-text {*
-  If the function is already strict in that argument, then the bottom
-  pattern does not change the meaning of the function.  For example,
-  in the definition of @{term from_sinr_up}, the first equation is
-  actually redundant, and could have been proven separately by
-  @{text fixrec_simp}.
-*}
-
-text {*
-  A bottom pattern can also be used to make a function strict in a
-  certain argument, similar to a bang-pattern in Haskell.
-*}
-
-fixrec
-  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
-where
-  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
-| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
-
-
-subsection {* Skipping proofs of rewrite rules *}
-
-text {* Another zip function for lazy lists. *}
-
-text {*
-  Notice that this version has overlapping patterns.
-  The second equation cannot be proved as a theorem
-  because it only applies when the first pattern fails.
-*}
-
-fixrec (permissive)
-  lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
-where
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-| "lzip2\<cdot>xs\<cdot>ys = lNil"
-
-text {*
-  Usually fixrec tries to prove all equations as theorems.
-  The "permissive" option overrides this behavior, so fixrec
-  does not produce any simp rules.
-*}
-
-text {* Simp rules can be generated later using @{text fixrec_simp}. *}
-
-lemma lzip2_simps [simp]:
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
-  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
-  "lzip2\<cdot>lNil\<cdot>lNil = lNil"
-by fixrec_simp+
-
-lemma lzip2_stricts [simp]:
-  "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp+
-
-
-subsection {* Mutual recursion with @{text fixrec} *}
-
-text {* Tree and forest types. *}
-
-domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
-and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
-
-text {*
-  To define mutually recursive functions, give multiple type signatures
-  separated by the keyword @{text "and"}.
-*}
-
-fixrec
-  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
-and
-  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
-where
-  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
-| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
-| "map_forest\<cdot>f\<cdot>Empty = Empty"
-| "ts \<noteq> \<bottom> \<Longrightarrow>
-    map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
-
-lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp
-
-lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp
-
-text {*
-  Theorems generated:
-  @{text map_tree_def}  @{thm map_tree_def}
-  @{text map_forest_def}  @{thm map_forest_def}
-  @{text map_tree.unfold}  @{thm map_tree.unfold}
-  @{text map_forest.unfold}  @{thm map_forest.unfold}
-  @{text map_tree.simps}  @{thm map_tree.simps}
-  @{text map_forest.simps}  @{thm map_forest.simps}
-  @{text map_tree_map_forest.induct}  @{thm map_tree_map_forest.induct}
-*}
-
-
-subsection {* Using @{text fixrec} inside locales *}
-
-locale test =
-  fixes foo :: "'a \<rightarrow> 'a"
-  assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
-begin
-
-fixrec
-  bar :: "'a u \<rightarrow> 'a"
-where
-  "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
-
-lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp
-
-end
-
-end

--- a/src/HOLCF/ex/New_Domain.thy	Thu May 20 16:22:50 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-(*  Title:      HOLCF/ex/New_Domain.thy
-    Author:     Brian Huffman
-*)
-
-header {* Definitional domain package *}
-
-theory New_Domain
-imports HOLCF
-begin
-
-text {*
-  The definitional domain package only works with representable domains,
-  i.e. types in class @{text rep}.
-*}
-
-default_sort rep
-
-text {*
-  Provided that @{text rep} is the default sort, the @{text new_domain}
-  package should work with any type definition supported by the old
-  domain package.
-*}
-
-new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
-
-text {*
-  The difference is that the new domain package is completely
-  definitional, and does not generate any axioms.  The following type
-  and constant definitions are not produced by the old domain package.
-*}
-
-thm type_definition_llist
-thm llist_abs_def llist_rep_def
-
-text {*
-  The new domain package also adds support for indirect recursion with
-  user-defined datatypes.  This definition of a tree datatype uses
-  indirect recursion through the lazy list type constructor.
-*}
-
-new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
-
-text {*
-  For indirect-recursive definitions, the domain package is not able to
-  generate a high-level induction rule.  (It produces a warning
-  message instead.)  The low-level reach lemma (now proved as a
-  theorem, no longer generated as an axiom) can be used to derive
-  other induction rules.
-*}
-
-thm ltree.reach
-
-text {*
-  The definition of the take function uses map functions associated with
-  each type constructor involved in the definition.  A map function
-  for the lazy list type has been generated by the new domain package.
-*}
-
-thm ltree.take_rews
-thm llist_map_def
-
-lemma ltree_induct:
-  fixes P :: "'a ltree \<Rightarrow> bool"
-  assumes adm: "adm P"
-  assumes bot: "P \<bottom>"
-  assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
-  assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
-  shows "P x"
-proof -
-  have "P (\<Squnion>i. ltree_take i\<cdot>x)"
-  using adm
-  proof (rule admD)
-    fix i
-    show "P (ltree_take i\<cdot>x)"
-    proof (induct i arbitrary: x)
-      case (0 x)
-      show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
-    next
-      case (Suc n x)
-      show "P (ltree_take (Suc n)\<cdot>x)"
-        apply (cases x)
-        apply (simp add: bot)
-        apply (simp add: Leaf)
-        apply (simp add: Branch Suc)
-        done
-    qed
-  qed (simp add: ltree.chain_take)
-  thus ?thesis
-    by (simp add: ltree.reach)
-qed
-
-end

--- a/src/HOLCF/ex/ROOT.ML	Thu May 20 16:22:50 2010 +0200
+++ b/src/HOLCF/ex/ROOT.ML	Thu May 20 16:25:22 2010 +0200
@@ -4,7 +4,6 @@
 *)
 
 use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
-  "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
+  "Loop", "Powerdomain_ex", "Domain_Proofs",
   "Letrec",
-  "Strict_Fun",
-  "New_Domain"];
+  "Strict_Fun"];