# HG changeset patch
# User huffman
# Date 1240321454 25200
# Node ID 182fa14e1844ad7e472d0dbb1de489a5159076f9
# Parent  e3bbc2c4c58147226bf6360423b0b3cd60179cae# Parent  a3d2128cac92bc2fe013023627aab2ac88d80b26
merged

diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Domain.thy	Tue Apr 21 06:44:14 2009 -0700
@@ -6,6 +6,14 @@
 
 theory Domain
 imports Ssum Sprod Up One Tr Fixrec
+uses
+  ("Tools/cont_consts.ML")
+  ("Tools/cont_proc.ML")
+  ("Tools/domain/domain_library.ML")
+  ("Tools/domain/domain_syntax.ML")
+  ("Tools/domain/domain_axioms.ML")
+  ("Tools/domain/domain_theorems.ML")
+  ("Tools/domain/domain_extender.ML")
 begin
 
 defaultsort pcpo
@@ -193,4 +201,24 @@
 
 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
 
+
+subsection {* Installing the domain package *}
+
+lemmas con_strict_rules =
+  sinl_strict sinr_strict spair_strict1 spair_strict2
+
+lemmas con_defin_rules =
+  sinl_defined sinr_defined spair_defined up_defined ONE_defined
+
+lemmas con_defined_iff_rules =
+  sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
+
+use "Tools/cont_consts.ML"
+use "Tools/cont_proc.ML"
+use "Tools/domain/domain_library.ML"
+use "Tools/domain/domain_syntax.ML"
+use "Tools/domain/domain_axioms.ML"
+use "Tools/domain/domain_theorems.ML"
+use "Tools/domain/domain_extender.ML"
+
 end
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Fixrec.thy	Tue Apr 21 06:44:14 2009 -0700
@@ -475,86 +475,95 @@
 defaultsort pcpo
 
 definition
-  match_UU :: "'a \<rightarrow> unit maybe" where
-  "match_UU = (\<Lambda> x. fail)"
+  match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
+where
+  "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
 
 definition
-  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" where
-  "match_cpair = csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
+  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
+where
+  "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
 
 definition
-  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" where
-  "match_spair = ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
+  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
+where
+  "match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)"
 
 definition
-  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" where
-  "match_sinl = sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
+  match_sinl :: "'a \<oplus> 'b \<rightarrow> ('a \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
+where
+  "match_sinl = (\<Lambda> x k. sscase\<cdot>k\<cdot>(\<Lambda> b. fail)\<cdot>x)"
 
 definition
-  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" where
-  "match_sinr = sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
+  match_sinr :: "'a \<oplus> 'b \<rightarrow> ('b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
+where
+  "match_sinr = (\<Lambda> x k. sscase\<cdot>(\<Lambda> a. fail)\<cdot>k\<cdot>x)"
 
 definition
-  match_up :: "'a::cpo u \<rightarrow> 'a maybe" where
-  "match_up = fup\<cdot>return"
+  match_up :: "'a::cpo u \<rightarrow> ('a \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
+where
+  "match_up = (\<Lambda> x k. fup\<cdot>k\<cdot>x)"
 
 definition
-  match_ONE :: "one \<rightarrow> unit maybe" where
-  "match_ONE = (\<Lambda> ONE. return\<cdot>())"
+  match_ONE :: "one \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
+where
+  "match_ONE = (\<Lambda> ONE k. k)"
+
+definition
+  match_TT :: "tr \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
+where
+  "match_TT = (\<Lambda> x k. If x then k else fail fi)"
  
 definition
-  match_TT :: "tr \<rightarrow> unit maybe" where
-  "match_TT = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
- 
-definition
-  match_FF :: "tr \<rightarrow> unit maybe" where
-  "match_FF = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
+  match_FF :: "tr \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
+where
+  "match_FF = (\<Lambda> x k. If x then fail else k fi)"
 
 lemma match_UU_simps [simp]:
-  "match_UU\<cdot>x = fail"
+  "match_UU\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
 by (simp add: match_UU_def)
 
 lemma match_cpair_simps [simp]:
-  "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
+  "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
 by (simp add: match_cpair_def)
 
 lemma match_spair_simps [simp]:
-  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
-  "match_spair\<cdot>\<bottom> = \<bottom>"
+  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
+  "match_spair\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_spair_def)
 
 lemma match_sinl_simps [simp]:
-  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
-  "match_sinl\<cdot>\<bottom> = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x"
+  "y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail"
+  "match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_sinl_def)
 
 lemma match_sinr_simps [simp]:
-  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
-  "match_sinr\<cdot>\<bottom> = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail"
+  "y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y"
+  "match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_sinr_def)
 
 lemma match_up_simps [simp]:
-  "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
-  "match_up\<cdot>\<bottom> = \<bottom>"
+  "match_up\<cdot>(up\<cdot>x)\<cdot>k = k\<cdot>x"
+  "match_up\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_up_def)
 
 lemma match_ONE_simps [simp]:
-  "match_ONE\<cdot>ONE = return\<cdot>()"
-  "match_ONE\<cdot>\<bottom> = \<bottom>"
+  "match_ONE\<cdot>ONE\<cdot>k = k"
+  "match_ONE\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_ONE_def)
 
 lemma match_TT_simps [simp]:
-  "match_TT\<cdot>TT = return\<cdot>()"
-  "match_TT\<cdot>FF = fail"
-  "match_TT\<cdot>\<bottom> = \<bottom>"
+  "match_TT\<cdot>TT\<cdot>k = k"
+  "match_TT\<cdot>FF\<cdot>k = fail"
+  "match_TT\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_TT_def)
 
 lemma match_FF_simps [simp]:
-  "match_FF\<cdot>FF = return\<cdot>()"
-  "match_FF\<cdot>TT = fail"
-  "match_FF\<cdot>\<bottom> = \<bottom>"
+  "match_FF\<cdot>FF\<cdot>k = k"
+  "match_FF\<cdot>TT\<cdot>k = fail"
+  "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_FF_def)
 
 subsection {* Mutual recursion *}
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/HOLCF.thy	Tue Apr 21 06:44:14 2009 -0700
@@ -9,13 +9,6 @@
   Domain ConvexPD Algebraic Universal Sum_Cpo Main
 uses
   "holcf_logic.ML"
-  "Tools/cont_consts.ML"
-  "Tools/cont_proc.ML"
-  "Tools/domain/domain_library.ML"
-  "Tools/domain/domain_syntax.ML"
-  "Tools/domain/domain_axioms.ML"
-  "Tools/domain/domain_theorems.ML"
-  "Tools/domain/domain_extender.ML"
   "Tools/adm_tac.ML"
 begin
 
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Apr 21 06:44:14 2009 -0700
@@ -288,8 +288,7 @@
 
 lemma Cons_not_UU: "a>>s ~= UU"
 apply (subst Consq_def2)
-apply (rule seq.con_rews)
-apply (rule Def_not_UU)
+apply simp
 done
 
 
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/One.thy	Tue Apr 21 06:44:14 2009 -0700
@@ -37,8 +37,8 @@
 lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
 by (induct x rule: one_induct) simp_all
 
-lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
-unfolding ONE_def by simp_all
+lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
+unfolding ONE_def by simp
 
 lemma one_neq_iffs [simp]:
   "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -18,8 +18,6 @@
 
 (* misc utils *)
 
-open HOLCFLogic;
-
 fun first  (x,_,_) = x;
 fun second (_,x,_) = x;
 fun third  (_,_,x) = x;
@@ -66,7 +64,7 @@
             (c2,change_arrow n T,mx   ),
             trans_rules c2 c n mx) end;
 
-fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
+fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
 |   cfun_arity _               = 0;
 
 fun is_contconst (_,_,NoSyn   ) = false
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -60,14 +60,18 @@
 			   (if con'=con then TT else FF) args)) cons))
 	in map ddef cons end;
 
-  val mat_defs = let
-	fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == 
-		 list_ccomb(%%:(dname^"_when"),map 
-			(fn (con',args) => (List.foldr /\#
-			   (if con'=con
-                               then mk_return (mk_ctuple (map (bound_arg args) args))
-                               else mk_fail) args)) cons))
-	in map mdef cons end;
+  val mat_defs =
+    let
+      fun mdef (con,_) =
+        let
+          val k = Bound 0
+          val x = Bound 1
+          fun one_con (con', args') =
+	    if con'=con then k else List.foldr /\# mk_fail args'
+          val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
+          val rhs = /\ "x" (/\ "k" (w ` x))
+        in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
+    in map mdef cons end;
 
   val pat_defs =
     let
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -1,34 +1,15 @@
 (*  Title:      HOLCF/Tools/domain/domain_extender.ML
-    ID:         $Id$
     Author:     David von Oheimb
 
 Theory extender for domain command, including theory syntax.
-
-###TODO: 
-
-this definition
-domain empty = silly empty
-yields
-Exception-
-   TERM
-      ("typ_of_term: bad encoding of type",
-         [Abs ("uu", "_", Const ("NONE", "_"))]) raised
-but this works fine:
-domain Empty = silly Empty
-
-strange syntax errors are produced for:
-domain xx = xx ("x yy")
-domain 'a foo = foo (sel::"'a") 
-and bar = bar ("'a dummy")
-
 *)
 
 signature DOMAIN_EXTENDER =
 sig
-  val add_domain: string * ((bstring * string list) *
+  val add_domain: string * ((bstring * string list * mixfix) *
     (string * mixfix * (bool * string option * string) list) list) list
     -> theory -> theory
-  val add_domain_i: string * ((bstring * string list) *
+  val add_domain_i: string * ((bstring * string list * mixfix) *
     (string * mixfix * (bool * string option * typ) list) list) list
     -> theory -> theory
 end;
@@ -99,16 +80,17 @@
 
 fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
   let
-    val dtnvs = map ((fn (dname,vs) => 
-			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
+    val dtnvs = map ((fn (dname,vs,mx) => 
+			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs, mx))
                    o fst) eqs''';
     val cons''' = map snd eqs''';
-    fun thy_type  (dname,tvars)  = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn);
-    fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
-    val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
+    fun thy_type  (dname,tvars,mx) = (Binding.name (Long_Name.base_name dname), length tvars, mx);
+    fun thy_arity (dname,tvars,mx) = (dname, map (snd o dest_TFree) tvars, pcpoS);
+    val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
 		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
     val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
-    val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
+    val dtnvs' = map (fn (dname,vs,mx) => (dname,vs)) dtnvs;
+    val eqs' = check_and_sort_domain (dtnvs',cons'') thy'';
     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
@@ -148,7 +130,7 @@
 
 val _ = OuterKeyword.keyword "lazy";
 
-val dest_decl =
+val dest_decl : (bool * string option * string) parser =
   P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
     (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
   || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
@@ -156,25 +138,37 @@
   || P.typ >> (fn t => (false,NONE,t));
 
 val cons_decl =
-  P.name -- Scan.repeat dest_decl -- P.opt_mixfix
-  >> (fn ((c, ds), mx) => (c, mx, ds));
+  P.name -- Scan.repeat dest_decl -- P.opt_mixfix;
+
+val type_var' =
+  (P.type_ident ^^ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
+
+val type_args' =
+  type_var' >> single ||
+  P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
+  Scan.succeed [];
+
+val domain_decl =
+  (type_args' -- P.name -- P.opt_infix) --
+  (P.$$$ "=" |-- P.enum1 "|" cons_decl);
 
-val type_var' = (P.type_ident ^^ 
-                 Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
-val type_args' = type_var' >> single ||
-                 P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
- 		 Scan.succeed [];
+val domains_decl =
+  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+  P.and_list1 domain_decl;
 
-val domain_decl = (type_args' -- P.name >> Library.swap) -- 
-                  (P.$$$ "=" |-- P.enum1 "|" cons_decl);
-val domains_decl =
-  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
-  >> (fn (opt_name, doms) =>
-      (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
+fun mk_domain (opt_name : string option, doms : (((string list * bstring) * mixfix) *
+    ((string * (bool * string option * string) list) * mixfix) list) list ) =
+  let
+    val names = map (fn (((_, t), _), _) => t) doms;
+    val specs = map (fn (((vs, t), mx), cons) =>
+      ((t, vs, mx), map (fn ((c, ds), mx) => (c, mx, ds)) cons)) doms;
+    val big_name =
+      case opt_name of NONE => space_implode "_" names | SOME s => s;
+  in add_domain (big_name, specs) end;
 
 val _ =
   OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
-    (domains_decl >> (Toplevel.theory o add_domain));
+    (domains_decl >> (Toplevel.theory o mk_domain));
 
 end;
 
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -34,8 +34,6 @@
 
 structure Domain_Library = struct
 
-open HOLCFLogic;
-
 exception Impossible of string;
 fun Imposs msg = raise Impossible ("Domain:"^msg);
 
@@ -72,7 +70,7 @@
       | index_vnames([],occupied) = [];
 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
 
-fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
+fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
 
 (* ----- constructor list handling ----- *)
@@ -99,6 +97,17 @@
 (* ----- support for type and mixfix expressions ----- *)
 
 infixr 5 -->;
+fun mk_uT T = Type(@{type_name "u"}, [T]);
+fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+val oneT = @{typ one};
+val trT = @{typ tr};
+
+infixr 6 ->>;
+val op ->> = mk_cfunT;
+
+fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
 
 (* ----- support for term expressions ----- *)
 
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/domain/domain_syntax.ML
--- a/src/HOLCF/Tools/domain/domain_syntax.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -46,12 +46,14 @@
 			(* strictly speaking, these constants have one argument,
 			   but the mixfix (without arguments) is introduced only
 			   to generate parse rules for non-alphanumeric names*)
-  fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
+  fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
+			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
+  fun mk_matT (a,bs,c)  = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+  fun mat (con,s,args)  = (mat_name_ con,
+                           mk_matT(dtype, map third args, freetvar "t" 1),
 			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
   fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
   fun sel (_   ,_,args) = List.mapPartial sel1 args;
-  fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
-			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
   fun mk_patT (a,b)     = a ->> mk_maybeT b;
   fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
   fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -314,8 +314,8 @@
 local
   fun mat_strict (con, _) =
     let
-      val goal = mk_trp (strict (%%:(mat_name con)));
-      val tacs = [rtac when_strict 1];
+      val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
+      val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
     in pg axs_mat_def goal (K tacs) end;
 
   val _ = trace " Proving mat_stricts...";
@@ -323,10 +323,10 @@
 
   fun one_mat c (con, args) =
     let
-      val lhs = %%:(mat_name c) ` con_app con args;
+      val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
       val rhs =
         if con = c
-        then mk_return (mk_ctuple (map %# args))
+        then list_ccomb (%:"rhs", map %# args)
         else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
@@ -374,30 +374,32 @@
 end;
 
 local
-  val rev_contrapos = @{thm rev_contrapos};
   fun con_strict (con, args) = 
     let
+      val rules = abs_strict :: @{thms con_strict_rules};
       fun one_strict vn =
         let
           fun f arg = if vname arg = vn then UU else %# arg;
           val goal = mk_trp (con_app2 con f args === UU);
-          val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
+          val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
         in pg con_appls goal (K tacs) end;
     in map one_strict (nonlazy args) end;
 
   fun con_defin (con, args) =
     let
-      val concl = mk_trp (defined (con_app con args));
-      val goal = lift_defined %: (nonlazy args, concl);
-      fun tacs ctxt = [
-        rtac @{thm rev_contrapos} 1,
-        eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
-        asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
-    in pg [] goal tacs end;
+      fun iff_disj (t, []) = HOLogic.mk_not t
+        | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
+      val lhs = con_app con args === UU;
+      val rhss = map (fn x => %:x === UU) (nonlazy args);
+      val goal = mk_trp (iff_disj (lhs, rhss));
+      val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
+      val rules = rule1 :: @{thms con_defined_iff_rules};
+      val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+    in pg con_appls goal (K tacs) end;
 in
   val _ = trace " Proving con_stricts...";
   val con_stricts = maps con_strict cons;
-  val _ = trace " Proving pat_defins...";
+  val _ = trace " Proving con_defins...";
   val con_defins = map con_defin cons;
   val con_rews = con_stricts @ con_defins;
 end;
@@ -488,7 +490,6 @@
 end;
 
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-val rev_contrapos = @{thm rev_contrapos};
 
 val _ = trace " Proving dist_les...";
 val distincts_le =
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -36,6 +36,8 @@
 
 infixr 6 ->>; val (op ->>) = cfunT;
 
+fun cfunsT (Ts, U) = foldr cfunT U Ts;
+
 fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
 
@@ -57,7 +59,9 @@
   | tupleT [T] = T
   | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
 
-fun matchT T = body_cfun T ->> maybeT (tupleT (binder_cfun T));
+fun matchT (T, U) =
+  body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
+
 
 (*************************************************************************)
 (***************************** building terms ****************************)
@@ -240,10 +244,10 @@
         fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
-        val m = Const(match_name c, matchT T);
-        val k = lambda_ctuple vs rhs;
+        val m = Const(match_name c, matchT (T, fastype_of rhs));
+        val k = big_lambdas vs rhs;
       in
-        (mk_bind (m`v, k), v, n::taken)
+        (m`v`k, v, n::taken)
       end
   | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
   | _ => fixrec_err "pre_build: invalid pattern";
diff -r e3bbc2c4c581 -r 182fa14e1844 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOLCF/ex/Stream.thy	Tue Apr 21 06:44:14 2009 -0700
@@ -64,10 +64,10 @@
 section "scons"
 
 lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
-by (auto, erule contrapos_pp, simp)
+by simp
 
 lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
-by auto
+by simp
 
 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)"
 by (auto,insert stream.exhaust [of x],auto)
@@ -382,7 +382,6 @@
 
 lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
  apply (rule stream.casedist [of x], auto)
-    apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
    apply (simp add: zero_inat_def)
   apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
  apply (case_tac "#s") apply (simp_all add: iSuc_Fin)