merged
authorhaftmann
Fri Apr 24 21:27:49 2009 +0200 (2009-04-24)
changeset 3097644637646fa17
parent 30975 b2fa60d56735
parent 30922 96d053e00ec0
child 30977 0e8e8903ff4e
merged
     1.1 --- a/src/HOLCF/Domain.thy	Fri Apr 24 18:20:37 2009 +0200
     1.2 +++ b/src/HOLCF/Domain.thy	Fri Apr 24 21:27:49 2009 +0200
     1.3 @@ -6,6 +6,14 @@
     1.4  
     1.5  theory Domain
     1.6  imports Ssum Sprod Up One Tr Fixrec
     1.7 +uses
     1.8 +  ("Tools/cont_consts.ML")
     1.9 +  ("Tools/cont_proc.ML")
    1.10 +  ("Tools/domain/domain_library.ML")
    1.11 +  ("Tools/domain/domain_syntax.ML")
    1.12 +  ("Tools/domain/domain_axioms.ML")
    1.13 +  ("Tools/domain/domain_theorems.ML")
    1.14 +  ("Tools/domain/domain_extender.ML")
    1.15  begin
    1.16  
    1.17  defaultsort pcpo
    1.18 @@ -193,4 +201,24 @@
    1.19  
    1.20  lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
    1.21  
    1.22 +
    1.23 +subsection {* Installing the domain package *}
    1.24 +
    1.25 +lemmas con_strict_rules =
    1.26 +  sinl_strict sinr_strict spair_strict1 spair_strict2
    1.27 +
    1.28 +lemmas con_defin_rules =
    1.29 +  sinl_defined sinr_defined spair_defined up_defined ONE_defined
    1.30 +
    1.31 +lemmas con_defined_iff_rules =
    1.32 +  sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
    1.33 +
    1.34 +use "Tools/cont_consts.ML"
    1.35 +use "Tools/cont_proc.ML"
    1.36 +use "Tools/domain/domain_library.ML"
    1.37 +use "Tools/domain/domain_syntax.ML"
    1.38 +use "Tools/domain/domain_axioms.ML"
    1.39 +use "Tools/domain/domain_theorems.ML"
    1.40 +use "Tools/domain/domain_extender.ML"
    1.41 +
    1.42  end
     2.1 --- a/src/HOLCF/Fixrec.thy	Fri Apr 24 18:20:37 2009 +0200
     2.2 +++ b/src/HOLCF/Fixrec.thy	Fri Apr 24 21:27:49 2009 +0200
     2.3 @@ -475,86 +475,95 @@
     2.4  defaultsort pcpo
     2.5  
     2.6  definition
     2.7 -  match_UU :: "'a \<rightarrow> unit maybe" where
     2.8 -  "match_UU = (\<Lambda> x. fail)"
     2.9 +  match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
    2.10 +where
    2.11 +  "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
    2.12  
    2.13  definition
    2.14 -  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" where
    2.15 -  "match_cpair = csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
    2.16 +  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
    2.17 +where
    2.18 +  "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
    2.19  
    2.20  definition
    2.21 -  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" where
    2.22 -  "match_spair = ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
    2.23 +  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
    2.24 +where
    2.25 +  "match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)"
    2.26  
    2.27  definition
    2.28 -  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" where
    2.29 -  "match_sinl = sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
    2.30 +  match_sinl :: "'a \<oplus> 'b \<rightarrow> ('a \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
    2.31 +where
    2.32 +  "match_sinl = (\<Lambda> x k. sscase\<cdot>k\<cdot>(\<Lambda> b. fail)\<cdot>x)"
    2.33  
    2.34  definition
    2.35 -  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" where
    2.36 -  "match_sinr = sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
    2.37 +  match_sinr :: "'a \<oplus> 'b \<rightarrow> ('b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
    2.38 +where
    2.39 +  "match_sinr = (\<Lambda> x k. sscase\<cdot>(\<Lambda> a. fail)\<cdot>k\<cdot>x)"
    2.40  
    2.41  definition
    2.42 -  match_up :: "'a::cpo u \<rightarrow> 'a maybe" where
    2.43 -  "match_up = fup\<cdot>return"
    2.44 +  match_up :: "'a::cpo u \<rightarrow> ('a \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
    2.45 +where
    2.46 +  "match_up = (\<Lambda> x k. fup\<cdot>k\<cdot>x)"
    2.47  
    2.48  definition
    2.49 -  match_ONE :: "one \<rightarrow> unit maybe" where
    2.50 -  "match_ONE = (\<Lambda> ONE. return\<cdot>())"
    2.51 +  match_ONE :: "one \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
    2.52 +where
    2.53 +  "match_ONE = (\<Lambda> ONE k. k)"
    2.54 +
    2.55 +definition
    2.56 +  match_TT :: "tr \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
    2.57 +where
    2.58 +  "match_TT = (\<Lambda> x k. If x then k else fail fi)"
    2.59   
    2.60  definition
    2.61 -  match_TT :: "tr \<rightarrow> unit maybe" where
    2.62 -  "match_TT = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
    2.63 - 
    2.64 -definition
    2.65 -  match_FF :: "tr \<rightarrow> unit maybe" where
    2.66 -  "match_FF = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
    2.67 +  match_FF :: "tr \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
    2.68 +where
    2.69 +  "match_FF = (\<Lambda> x k. If x then fail else k fi)"
    2.70  
    2.71  lemma match_UU_simps [simp]:
    2.72 -  "match_UU\<cdot>x = fail"
    2.73 +  "match_UU\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
    2.74  by (simp add: match_UU_def)
    2.75  
    2.76  lemma match_cpair_simps [simp]:
    2.77 -  "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
    2.78 +  "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
    2.79  by (simp add: match_cpair_def)
    2.80  
    2.81  lemma match_spair_simps [simp]:
    2.82 -  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
    2.83 -  "match_spair\<cdot>\<bottom> = \<bottom>"
    2.84 +  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
    2.85 +  "match_spair\<cdot>\<bottom>\<cdot>k = \<bottom>"
    2.86  by (simp_all add: match_spair_def)
    2.87  
    2.88  lemma match_sinl_simps [simp]:
    2.89 -  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
    2.90 -  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
    2.91 -  "match_sinl\<cdot>\<bottom> = \<bottom>"
    2.92 +  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x"
    2.93 +  "y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail"
    2.94 +  "match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>"
    2.95  by (simp_all add: match_sinl_def)
    2.96  
    2.97  lemma match_sinr_simps [simp]:
    2.98 -  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
    2.99 -  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
   2.100 -  "match_sinr\<cdot>\<bottom> = \<bottom>"
   2.101 +  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail"
   2.102 +  "y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y"
   2.103 +  "match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>"
   2.104  by (simp_all add: match_sinr_def)
   2.105  
   2.106  lemma match_up_simps [simp]:
   2.107 -  "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
   2.108 -  "match_up\<cdot>\<bottom> = \<bottom>"
   2.109 +  "match_up\<cdot>(up\<cdot>x)\<cdot>k = k\<cdot>x"
   2.110 +  "match_up\<cdot>\<bottom>\<cdot>k = \<bottom>"
   2.111  by (simp_all add: match_up_def)
   2.112  
   2.113  lemma match_ONE_simps [simp]:
   2.114 -  "match_ONE\<cdot>ONE = return\<cdot>()"
   2.115 -  "match_ONE\<cdot>\<bottom> = \<bottom>"
   2.116 +  "match_ONE\<cdot>ONE\<cdot>k = k"
   2.117 +  "match_ONE\<cdot>\<bottom>\<cdot>k = \<bottom>"
   2.118  by (simp_all add: match_ONE_def)
   2.119  
   2.120  lemma match_TT_simps [simp]:
   2.121 -  "match_TT\<cdot>TT = return\<cdot>()"
   2.122 -  "match_TT\<cdot>FF = fail"
   2.123 -  "match_TT\<cdot>\<bottom> = \<bottom>"
   2.124 +  "match_TT\<cdot>TT\<cdot>k = k"
   2.125 +  "match_TT\<cdot>FF\<cdot>k = fail"
   2.126 +  "match_TT\<cdot>\<bottom>\<cdot>k = \<bottom>"
   2.127  by (simp_all add: match_TT_def)
   2.128  
   2.129  lemma match_FF_simps [simp]:
   2.130 -  "match_FF\<cdot>FF = return\<cdot>()"
   2.131 -  "match_FF\<cdot>TT = fail"
   2.132 -  "match_FF\<cdot>\<bottom> = \<bottom>"
   2.133 +  "match_FF\<cdot>FF\<cdot>k = k"
   2.134 +  "match_FF\<cdot>TT\<cdot>k = fail"
   2.135 +  "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
   2.136  by (simp_all add: match_FF_def)
   2.137  
   2.138  subsection {* Mutual recursion *}
     3.1 --- a/src/HOLCF/HOLCF.thy	Fri Apr 24 18:20:37 2009 +0200
     3.2 +++ b/src/HOLCF/HOLCF.thy	Fri Apr 24 21:27:49 2009 +0200
     3.3 @@ -9,13 +9,6 @@
     3.4    Domain ConvexPD Algebraic Universal Sum_Cpo Main
     3.5  uses
     3.6    "holcf_logic.ML"
     3.7 -  "Tools/cont_consts.ML"
     3.8 -  "Tools/cont_proc.ML"
     3.9 -  "Tools/domain/domain_library.ML"
    3.10 -  "Tools/domain/domain_syntax.ML"
    3.11 -  "Tools/domain/domain_axioms.ML"
    3.12 -  "Tools/domain/domain_theorems.ML"
    3.13 -  "Tools/domain/domain_extender.ML"
    3.14    "Tools/adm_tac.ML"
    3.15  begin
    3.16  
     4.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Apr 24 18:20:37 2009 +0200
     4.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Apr 24 21:27:49 2009 +0200
     4.3 @@ -288,8 +288,7 @@
     4.4  
     4.5  lemma Cons_not_UU: "a>>s ~= UU"
     4.6  apply (subst Consq_def2)
     4.7 -apply (rule seq.con_rews)
     4.8 -apply (rule Def_not_UU)
     4.9 +apply simp
    4.10  done
    4.11  
    4.12  
     5.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Fri Apr 24 18:20:37 2009 +0200
     5.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Fri Apr 24 21:27:49 2009 +0200
     5.3 @@ -347,12 +347,12 @@
     5.4  val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
     5.5  							atyp statetupel trans;
     5.6  val thy2 = (thy
     5.7 -|> ContConsts.add_consts
     5.8 -[(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn),
     5.9 -(automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn),
    5.10 -(automaton_name ^ "_trans",
    5.11 +|> Sign.add_consts
    5.12 +[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
    5.13 +(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
    5.14 +(Binding.name (automaton_name ^ "_trans"),
    5.15   "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
    5.16 -(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
    5.17 +(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
    5.18  |> add_defs
    5.19  [(automaton_name ^ "_initial_def",
    5.20  automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
    5.21 @@ -386,8 +386,8 @@
    5.22  val comp_list = clist aut_list;
    5.23  in
    5.24  thy
    5.25 -|> ContConsts.add_consts_i
    5.26 -[(automaton_name,
    5.27 +|> Sign.add_consts_i
    5.28 +[(Binding.name automaton_name,
    5.29  Type("*",
    5.30  [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
    5.31   Type("*",[Type("set",[st_typ]),
    5.32 @@ -407,8 +407,8 @@
    5.33  val rest_set = action_set_string thy acttyp actlist
    5.34  in
    5.35  thy
    5.36 -|> ContConsts.add_consts_i
    5.37 -[(automaton_name, auttyp,NoSyn)]
    5.38 +|> Sign.add_consts_i
    5.39 +[(Binding.name automaton_name, auttyp,NoSyn)]
    5.40  |> add_defs
    5.41  [(automaton_name ^ "_def",
    5.42  automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
    5.43 @@ -421,8 +421,8 @@
    5.44  val hid_set = action_set_string thy acttyp actlist
    5.45  in
    5.46  thy
    5.47 -|> ContConsts.add_consts_i
    5.48 -[(automaton_name, auttyp,NoSyn)]
    5.49 +|> Sign.add_consts_i
    5.50 +[(Binding.name automaton_name, auttyp,NoSyn)]
    5.51  |> add_defs
    5.52  [(automaton_name ^ "_def",
    5.53  automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
    5.54 @@ -441,8 +441,8 @@
    5.55  val acttyp = ren_act_type_of thy fun_name
    5.56  in
    5.57  thy
    5.58 -|> ContConsts.add_consts_i
    5.59 -[(automaton_name,
    5.60 +|> Sign.add_consts_i
    5.61 +[(Binding.name automaton_name,
    5.62  Type("*",
    5.63  [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
    5.64   Type("*",[Type("set",[st_typ]),
     6.1 --- a/src/HOLCF/IsaMakefile	Fri Apr 24 18:20:37 2009 +0200
     6.2 +++ b/src/HOLCF/IsaMakefile	Fri Apr 24 21:27:49 2009 +0200
     6.3 @@ -87,10 +87,19 @@
     6.4  
     6.5  HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
     6.6  
     6.7 -$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \
     6.8 -  ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
     6.9 +$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
    6.10 +  ../HOL/Library/Nat_Infinity.thy \
    6.11 +  ex/Dagstuhl.thy \
    6.12 +  ex/Dnat.thy \
    6.13 +  ex/Domain_ex.thy \
    6.14 +  ex/Fix2.thy \
    6.15 +  ex/Fixrec_ex.thy \
    6.16 +  ex/Focus_ex.thy \
    6.17 +  ex/Hoare.thy \
    6.18 +  ex/Loop.thy \
    6.19    ex/Powerdomain_ex.thy \
    6.20 -  ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
    6.21 +  ex/Stream.thy \
    6.22 +  ex/ROOT.ML
    6.23  	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
    6.24  
    6.25  
     7.1 --- a/src/HOLCF/One.thy	Fri Apr 24 18:20:37 2009 +0200
     7.2 +++ b/src/HOLCF/One.thy	Fri Apr 24 21:27:49 2009 +0200
     7.3 @@ -37,8 +37,8 @@
     7.4  lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
     7.5  by (induct x rule: one_induct) simp_all
     7.6  
     7.7 -lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
     7.8 -unfolding ONE_def by simp_all
     7.9 +lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
    7.10 +unfolding ONE_def by simp
    7.11  
    7.12  lemma one_neq_iffs [simp]:
    7.13    "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
     8.1 --- a/src/HOLCF/Tools/cont_consts.ML	Fri Apr 24 18:20:37 2009 +0200
     8.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Fri Apr 24 21:27:49 2009 +0200
     8.3 @@ -8,8 +8,8 @@
     8.4  
     8.5  signature CONT_CONSTS =
     8.6  sig
     8.7 -  val add_consts: (bstring * string * mixfix) list -> theory -> theory
     8.8 -  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     8.9 +  val add_consts: (binding * string * mixfix) list -> theory -> theory
    8.10 +  val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
    8.11  end;
    8.12  
    8.13  structure ContConsts: CONT_CONSTS =
    8.14 @@ -18,8 +18,6 @@
    8.15  
    8.16  (* misc utils *)
    8.17  
    8.18 -open HOLCFLogic;
    8.19 -
    8.20  fun first  (x,_,_) = x;
    8.21  fun second (_,x,_) = x;
    8.22  fun third  (_,_,x) = x;
    8.23 @@ -51,29 +49,33 @@
    8.24     declaration with the original name, type ...=>..., and the original mixfix
    8.25     is generated and connected to the other declaration via some translation.
    8.26  *)
    8.27 -fun fix_mixfix (syn                     , T, mx as Infix           p ) =
    8.28 -               (Syntax.const_name mx syn, T,       InfixName (syn, p))
    8.29 -  | fix_mixfix (syn                     , T, mx as Infixl           p ) =
    8.30 -               (Syntax.const_name mx syn, T,       InfixlName (syn, p))
    8.31 -  | fix_mixfix (syn                     , T, mx as Infixr           p ) =
    8.32 -               (Syntax.const_name mx syn, T,       InfixrName (syn, p))
    8.33 +fun const_binding mx = Binding.name o Syntax.const_name mx o Binding.name_of;
    8.34 +
    8.35 +fun fix_mixfix (syn                 , T, mx as Infix           p ) =
    8.36 +               (const_binding mx syn, T,       InfixName (Binding.name_of syn, p))
    8.37 +  | fix_mixfix (syn                 , T, mx as Infixl           p ) =
    8.38 +               (const_binding mx syn, T,       InfixlName (Binding.name_of syn, p))
    8.39 +  | fix_mixfix (syn                 , T, mx as Infixr           p ) =
    8.40 +               (const_binding mx syn, T,       InfixrName (Binding.name_of syn, p))
    8.41    | fix_mixfix decl = decl;
    8.42 +
    8.43  fun transform decl = let
    8.44          val (c, T, mx) = fix_mixfix decl;
    8.45 -        val c2 = "_cont_" ^ c;
    8.46 +        val c1 = Binding.name_of c;
    8.47 +        val c2 = "_cont_" ^ c1;
    8.48          val n  = Syntax.mixfix_args mx
    8.49 -    in     ((c ,               T,NoSyn),
    8.50 -            (c2,change_arrow n T,mx   ),
    8.51 -            trans_rules c2 c n mx) end;
    8.52 +    in     ((c, T, NoSyn),
    8.53 +            (Binding.name c2, change_arrow n T, mx),
    8.54 +            trans_rules c2 c1 n mx) end;
    8.55  
    8.56 -fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
    8.57 +fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
    8.58  |   cfun_arity _               = 0;
    8.59  
    8.60  fun is_contconst (_,_,NoSyn   ) = false
    8.61  |   is_contconst (_,_,Binder _) = false
    8.62  |   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    8.63                           handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
    8.64 -                                               quote (Syntax.const_name mx c));
    8.65 +                                               quote (Syntax.const_name mx (Binding.name_of c)));
    8.66  
    8.67  
    8.68  (* add_consts(_i) *)
    8.69 @@ -85,7 +87,7 @@
    8.70      val transformed_decls = map transform contconst_decls;
    8.71    in
    8.72      thy
    8.73 -    |> (Sign.add_consts_i o map (upd_first Binding.name))
    8.74 +    |> Sign.add_consts_i
    8.75        (normal_decls @ map first transformed_decls @ map second transformed_decls)
    8.76      |> Sign.add_trrules_i (maps third transformed_decls)
    8.77    end;
    8.78 @@ -100,7 +102,7 @@
    8.79  
    8.80  val _ =
    8.81    OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
    8.82 -    (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
    8.83 +    (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts));
    8.84  
    8.85  end;
    8.86  
     9.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Fri Apr 24 18:20:37 2009 +0200
     9.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Fri Apr 24 21:27:49 2009 +0200
     9.3 @@ -4,7 +4,14 @@
     9.4  Syntax generator for domain command.
     9.5  *)
     9.6  
     9.7 -structure Domain_Axioms = struct
     9.8 +signature DOMAIN_AXIOMS =
     9.9 +sig
    9.10 +  val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory
    9.11 +end;
    9.12 +
    9.13 +
    9.14 +structure Domain_Axioms : DOMAIN_AXIOMS =
    9.15 +struct
    9.16  
    9.17  local
    9.18  
    9.19 @@ -60,14 +67,18 @@
    9.20  			   (if con'=con then TT else FF) args)) cons))
    9.21  	in map ddef cons end;
    9.22  
    9.23 -  val mat_defs = let
    9.24 -	fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == 
    9.25 -		 list_ccomb(%%:(dname^"_when"),map 
    9.26 -			(fn (con',args) => (List.foldr /\#
    9.27 -			   (if con'=con
    9.28 -                               then mk_return (mk_ctuple (map (bound_arg args) args))
    9.29 -                               else mk_fail) args)) cons))
    9.30 -	in map mdef cons end;
    9.31 +  val mat_defs =
    9.32 +    let
    9.33 +      fun mdef (con,_) =
    9.34 +        let
    9.35 +          val k = Bound 0
    9.36 +          val x = Bound 1
    9.37 +          fun one_con (con', args') =
    9.38 +	    if con'=con then k else List.foldr /\# mk_fail args'
    9.39 +          val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
    9.40 +          val rhs = /\ "x" (/\ "k" (w ` x))
    9.41 +        in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
    9.42 +    in map mdef cons end;
    9.43  
    9.44    val pat_defs =
    9.45      let
    9.46 @@ -135,7 +146,7 @@
    9.47  
    9.48  in (* local *)
    9.49  
    9.50 -fun add_axioms (comp_dnam, eqs : eq list) thy' = let
    9.51 +fun add_axioms comp_dnam (eqs : eq list) thy' = let
    9.52    val comp_dname = Sign.full_bname thy' comp_dnam;
    9.53    val dnames = map (fst o fst) eqs;
    9.54    val x_name = idx_name dnames "x"; 
    10.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Fri Apr 24 18:20:37 2009 +0200
    10.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Fri Apr 24 21:27:49 2009 +0200
    10.3 @@ -1,35 +1,16 @@
    10.4  (*  Title:      HOLCF/Tools/domain/domain_extender.ML
    10.5 -    ID:         $Id$
    10.6      Author:     David von Oheimb
    10.7  
    10.8  Theory extender for domain command, including theory syntax.
    10.9 -
   10.10 -###TODO: 
   10.11 -
   10.12 -this definition
   10.13 -domain empty = silly empty
   10.14 -yields
   10.15 -Exception-
   10.16 -   TERM
   10.17 -      ("typ_of_term: bad encoding of type",
   10.18 -         [Abs ("uu", "_", Const ("NONE", "_"))]) raised
   10.19 -but this works fine:
   10.20 -domain Empty = silly Empty
   10.21 -
   10.22 -strange syntax errors are produced for:
   10.23 -domain xx = xx ("x yy")
   10.24 -domain 'a foo = foo (sel::"'a") 
   10.25 -and bar = bar ("'a dummy")
   10.26 -
   10.27  *)
   10.28  
   10.29  signature DOMAIN_EXTENDER =
   10.30  sig
   10.31 -  val add_domain: string * ((bstring * string list) *
   10.32 -    (string * mixfix * (bool * string option * string) list) list) list
   10.33 +  val add_domain_cmd: string -> (string list * binding * mixfix *
   10.34 +    (binding * (bool * binding option * string) list * mixfix) list) list
   10.35      -> theory -> theory
   10.36 -  val add_domain_i: string * ((bstring * string list) *
   10.37 -    (string * mixfix * (bool * string option * typ) list) list) list
   10.38 +  val add_domain: string -> (string list * binding * mixfix *
   10.39 +    (binding * (bool * binding option * typ) list * mixfix) list) list
   10.40      -> theory -> theory
   10.41  end;
   10.42  
   10.43 @@ -39,17 +20,21 @@
   10.44  open Domain_Library;
   10.45  
   10.46  (* ----- general testing and preprocessing of constructor list -------------- *)
   10.47 -fun check_and_sort_domain (dtnvs: (string * typ list) list, 
   10.48 -     cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
   10.49 +fun check_and_sort_domain
   10.50 +  (dtnvs : (string * typ list) list)
   10.51 +  (cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list)
   10.52 +  (sg : theory)
   10.53 +  : ((string * typ list) *
   10.54 +      (binding * (bool * binding option * typ) list * mixfix) list) list =
   10.55    let
   10.56      val defaultS = Sign.defaultS sg;
   10.57      val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
   10.58  	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
   10.59 -    val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of 
   10.60 +    val test_dupl_cons = (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of 
   10.61  	[] => false | dups => error ("Duplicate constructors: " 
   10.62  							 ^ commas_quote dups));
   10.63 -    val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
   10.64 -			       (List.concat (map third (List.concat cons'')))) of
   10.65 +    val test_dupl_sels = (case duplicates (op =) (map Binding.name_of (List.mapPartial second
   10.66 +			       (List.concat (map second (List.concat cons''))))) of
   10.67          [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
   10.68      val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
   10.69  	[] => false | dups => error("Duplicate type arguments: " 
   10.70 @@ -90,26 +75,31 @@
   10.71          |   analyse indirect (TVar _) = Imposs "extender:analyse";
   10.72  	fun check_pcpo T = if pcpo_type sg T then T
   10.73            else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
   10.74 -	val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
   10.75 +	val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false)));
   10.76        in ((dname,distinct_typevars), map analyse_con cons') end; 
   10.77    in ListPair.map analyse_equation (dtnvs,cons'')
   10.78    end; (* let *)
   10.79  
   10.80  (* ----- calls for building new thy and thms -------------------------------- *)
   10.81  
   10.82 -fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
   10.83 +fun gen_add_domain
   10.84 +  (prep_typ : theory -> 'a -> typ)
   10.85 +  (comp_dnam : string)
   10.86 +  (eqs''' : (string list * binding * mixfix *
   10.87 +              (binding * (bool * binding option * 'a) list * mixfix) list) list)
   10.88 +  (thy''' : theory) =
   10.89    let
   10.90 -    val dtnvs = map ((fn (dname,vs) => 
   10.91 -			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
   10.92 -                   o fst) eqs''';
   10.93 -    val cons''' = map snd eqs''';
   10.94 -    fun thy_type  (dname,tvars)  = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn);
   10.95 -    fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
   10.96 -    val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
   10.97 +    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
   10.98 +                  (dname, map (Syntax.read_typ_global thy''') vs, mx)) eqs''';
   10.99 +    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
  10.100 +    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
  10.101 +    fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
  10.102 +    val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
  10.103  		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
  10.104 -    val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
  10.105 -    val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
  10.106 -    val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
  10.107 +    val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
  10.108 +    val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
  10.109 +    val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = check_and_sort_domain dtnvs' cons'' thy'';
  10.110 +    val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
  10.111      val dts  = map (Type o fst) eqs';
  10.112      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
  10.113      fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
  10.114 @@ -118,16 +108,16 @@
  10.115            in if Symbol.is_letter c then c else "t" end
  10.116        | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
  10.117        | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
  10.118 -    fun one_con (con,mx,args) =
  10.119 -	((Syntax.const_name mx con),
  10.120 +    fun one_con (con,args,mx) =
  10.121 +	((Syntax.const_name mx (Binding.name_of con)),
  10.122  	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
  10.123  					find_index_eq tp dts,
  10.124  					DatatypeAux.dtyp_of_typ new_dts tp),
  10.125 -					sel,vn))
  10.126 +					Option.map Binding.name_of sel,vn))
  10.127  	     (args,(mk_var_names(map (typid o third) args)))
  10.128  	 ) : cons;
  10.129      val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
  10.130 -    val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
  10.131 +    val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
  10.132      val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
  10.133        Domain_Theorems.theorems (eq, eqs)) eqs
  10.134        ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
  10.135 @@ -138,8 +128,8 @@
  10.136      |> Sign.parent_path
  10.137    end;
  10.138  
  10.139 -val add_domain_i = gen_add_domain Sign.certify_typ;
  10.140 -val add_domain = gen_add_domain Syntax.read_typ_global;
  10.141 +val add_domain = gen_add_domain Sign.certify_typ;
  10.142 +val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
  10.143  
  10.144  
  10.145  (** outer syntax **)
  10.146 @@ -148,33 +138,47 @@
  10.147  
  10.148  val _ = OuterKeyword.keyword "lazy";
  10.149  
  10.150 -val dest_decl =
  10.151 +val dest_decl : (bool * binding option * string) parser =
  10.152    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
  10.153 -    (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
  10.154 +    (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
  10.155    || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
  10.156         >> (fn t => (true,NONE,t))
  10.157    || P.typ >> (fn t => (false,NONE,t));
  10.158  
  10.159  val cons_decl =
  10.160 -  P.name -- Scan.repeat dest_decl -- P.opt_mixfix
  10.161 -  >> (fn ((c, ds), mx) => (c, mx, ds));
  10.162 +  P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
  10.163 +
  10.164 +val type_var' =
  10.165 +  (P.type_ident ^^ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
  10.166 +
  10.167 +val type_args' =
  10.168 +  type_var' >> single ||
  10.169 +  P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
  10.170 +  Scan.succeed [];
  10.171 +
  10.172 +val domain_decl =
  10.173 +  (type_args' -- P.binding -- P.opt_infix) --
  10.174 +  (P.$$$ "=" |-- P.enum1 "|" cons_decl);
  10.175  
  10.176 -val type_var' = (P.type_ident ^^ 
  10.177 -                 Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
  10.178 -val type_args' = type_var' >> single ||
  10.179 -                 P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
  10.180 - 		 Scan.succeed [];
  10.181 +val domains_decl =
  10.182 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
  10.183 +  P.and_list1 domain_decl;
  10.184  
  10.185 -val domain_decl = (type_args' -- P.name >> Library.swap) -- 
  10.186 -                  (P.$$$ "=" |-- P.enum1 "|" cons_decl);
  10.187 -val domains_decl =
  10.188 -  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
  10.189 -  >> (fn (opt_name, doms) =>
  10.190 -      (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
  10.191 +fun mk_domain (opt_name : string option, doms : (((string list * binding) * mixfix) *
  10.192 +    ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
  10.193 +  let
  10.194 +    val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
  10.195 +    val specs : (string list * binding * mixfix *
  10.196 +      (binding * (bool * binding option * string) list * mixfix) list) list =
  10.197 +        map (fn (((vs, t), mx), cons) =>
  10.198 +          (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
  10.199 +    val comp_dnam =
  10.200 +      case opt_name of NONE => space_implode "_" names | SOME s => s;
  10.201 +  in add_domain_cmd comp_dnam specs end;
  10.202  
  10.203  val _ =
  10.204    OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
  10.205 -    (domains_decl >> (Toplevel.theory o add_domain));
  10.206 +    (domains_decl >> (Toplevel.theory o mk_domain));
  10.207  
  10.208  end;
  10.209  
    11.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Fri Apr 24 18:20:37 2009 +0200
    11.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri Apr 24 21:27:49 2009 +0200
    11.3 @@ -34,8 +34,6 @@
    11.4  
    11.5  structure Domain_Library = struct
    11.6  
    11.7 -open HOLCFLogic;
    11.8 -
    11.9  exception Impossible of string;
   11.10  fun Imposs msg = raise Impossible ("Domain:"^msg);
   11.11  
   11.12 @@ -72,7 +70,7 @@
   11.13        | index_vnames([],occupied) = [];
   11.14  in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
   11.15  
   11.16 -fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
   11.17 +fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
   11.18  fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
   11.19  
   11.20  (* ----- constructor list handling ----- *)
   11.21 @@ -99,6 +97,17 @@
   11.22  (* ----- support for type and mixfix expressions ----- *)
   11.23  
   11.24  infixr 5 -->;
   11.25 +fun mk_uT T = Type(@{type_name "u"}, [T]);
   11.26 +fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
   11.27 +fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
   11.28 +fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
   11.29 +val oneT = @{typ one};
   11.30 +val trT = @{typ tr};
   11.31 +
   11.32 +infixr 6 ->>;
   11.33 +val op ->> = mk_cfunT;
   11.34 +
   11.35 +fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
   11.36  
   11.37  (* ----- support for term expressions ----- *)
   11.38  
    12.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Fri Apr 24 18:20:37 2009 +0200
    12.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Fri Apr 24 21:27:49 2009 +0200
    12.3 @@ -4,32 +4,42 @@
    12.4  Syntax generator for domain command.
    12.5  *)
    12.6  
    12.7 -structure Domain_Syntax = struct 
    12.8 +signature DOMAIN_SYNTAX =
    12.9 +sig
   12.10 +  val add_syntax: string -> ((string * typ list) *
   12.11 +	(binding * (bool * binding option * typ) list * mixfix) list) list
   12.12 +    -> theory -> theory
   12.13 +end;
   12.14 +
   12.15 +
   12.16 +structure Domain_Syntax : DOMAIN_SYNTAX =
   12.17 +struct 
   12.18  
   12.19  local 
   12.20  
   12.21  open Domain_Library;
   12.22  infixr 5 -->; infixr 6 ->>;
   12.23  fun calc_syntax dtypeprod ((dname, typevars), 
   12.24 -	(cons': (string * mixfix * (bool * string option * typ) list) list)) =
   12.25 +	(cons': (binding * (bool * binding option * typ) list * mixfix) list)) : ((binding * typ * mixfix) list * ast Syntax.trrule list) =
   12.26  let
   12.27  (* ----- constants concerning the isomorphism ------------------------------- *)
   12.28  
   12.29  local
   12.30    fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
   12.31 -  fun prod     (_,_,args) = if args = [] then oneT
   12.32 -			    else foldr1 mk_sprodT (map opt_lazy args);
   12.33 +  fun prod     (_,args,_) = case args of [] => oneT
   12.34 +                            | _ => foldr1 mk_sprodT (map opt_lazy args);
   12.35    fun freetvar s = let val tvar = mk_TFree s in
   12.36  		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
   12.37 -  fun when_type (_   ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args);
   12.38 +  fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
   12.39  in
   12.40    val dtype  = Type(dname,typevars);
   12.41    val dtype2 = foldr1 mk_ssumT (map prod cons');
   12.42    val dnam = Long_Name.base_name dname;
   12.43 -  val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   12.44 -  val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   12.45 -  val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
   12.46 -  val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
   12.47 +  fun dbind s = Binding.name (dnam ^ s);
   12.48 +  val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
   12.49 +  val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
   12.50 +  val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
   12.51 +  val const_copy = (dbind "_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
   12.52  end;
   12.53  
   12.54  (* ----- constants concerning constructors, discriminators, and selectors --- *)
   12.55 @@ -40,23 +50,28 @@
   12.56  							 else      c::esc cs
   12.57  	|   esc []      = []
   12.58  	in implode o esc o Symbol.explode end;
   12.59 -  fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
   12.60 -  fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
   12.61 -			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
   12.62 +  fun dis_name_ con     = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
   12.63 +  fun mat_name_ con     = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
   12.64 +  fun pat_name_ con     = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
   12.65 +  fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
   12.66 +  fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
   12.67 +			   Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
   12.68  			(* strictly speaking, these constants have one argument,
   12.69  			   but the mixfix (without arguments) is introduced only
   12.70  			   to generate parse rules for non-alphanumeric names*)
   12.71 -  fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
   12.72 -			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
   12.73 -  fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
   12.74 -  fun sel (_   ,_,args) = List.mapPartial sel1 args;
   12.75    fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
   12.76  			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
   12.77 +  fun mk_matT (a,bs,c)  = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
   12.78 +  fun mat (con,args,mx) = (mat_name_ con,
   12.79 +                           mk_matT(dtype, map third args, freetvar "t" 1),
   12.80 +			   Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
   12.81 +  fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
   12.82 +  fun sel (con,args,mx) = List.mapPartial sel1 args;
   12.83    fun mk_patT (a,b)     = a ->> mk_maybeT b;
   12.84    fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
   12.85 -  fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
   12.86 +  fun pat (con,args,mx) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
   12.87  			   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
   12.88 -			   Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
   12.89 +			   Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
   12.90  
   12.91  in
   12.92    val consts_con = map con cons';
   12.93 @@ -68,14 +83,14 @@
   12.94  
   12.95  (* ----- constants concerning induction ------------------------------------- *)
   12.96  
   12.97 -  val const_take   = (dnam^"_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
   12.98 -  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT       , NoSyn);
   12.99 +  val const_take   = (dbind "_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
  12.100 +  val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
  12.101  
  12.102  (* ----- case translation --------------------------------------------------- *)
  12.103  
  12.104  local open Syntax in
  12.105    local
  12.106 -    fun c_ast con mx = Constant (Syntax.const_name mx con);
  12.107 +    fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
  12.108      fun expvar n     = Variable ("e"^(string_of_int n));
  12.109      fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
  12.110  				     (string_of_int m));
  12.111 @@ -83,9 +98,9 @@
  12.112      fun app s (l,r)  = mk_appl (Constant s) [l,r];
  12.113      val cabs = app "_cabs";
  12.114      val capp = app "Rep_CFun";
  12.115 -    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
  12.116 -    fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
  12.117 -    fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
  12.118 +    fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
  12.119 +    fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
  12.120 +    fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
  12.121      fun when1 n m = if n = m then arg1 n else K (Constant "UU");
  12.122  
  12.123      fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
  12.124 @@ -101,10 +116,10 @@
  12.125          (cabs (con1 n (con,mx,args), expvar n),
  12.126           Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
  12.127      
  12.128 -    val Case_trans = List.concat (map (fn (con,mx,args) =>
  12.129 +    val Case_trans = List.concat (map (fn (con,args,mx) =>
  12.130        let
  12.131          val cname = c_ast con mx;
  12.132 -        val pname = Constant (pat_name_ con);
  12.133 +        val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
  12.134          val ns = 1 upto length args;
  12.135          val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
  12.136          val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
  12.137 @@ -130,16 +145,19 @@
  12.138  
  12.139  in (* local *)
  12.140  
  12.141 -fun add_syntax (comp_dnam,eqs': ((string * typ list) *
  12.142 -	(string * mixfix * (bool * string option * typ) list) list) list) thy'' =
  12.143 +fun add_syntax
  12.144 +  (comp_dnam : string)
  12.145 +  (eqs' : ((string * typ list) *
  12.146 +	(binding * (bool * binding option * typ) list * mixfix) list) list)
  12.147 +  (thy'' : theory) =
  12.148  let
  12.149    val dtypes  = map (Type o fst) eqs';
  12.150    val boolT   = HOLogic.boolT;
  12.151    val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
  12.152    val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
  12.153 -  val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
  12.154 -  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
  12.155 -  val ctt           = map (calc_syntax funprod) eqs';
  12.156 +  val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
  12.157 +  val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
  12.158 +  val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
  12.159  in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ 
  12.160  				    (if length eqs'>1 then [const_copy] else[])@
  12.161  				    [const_bisim])
    13.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Apr 24 18:20:37 2009 +0200
    13.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Apr 24 21:27:49 2009 +0200
    13.3 @@ -314,8 +314,8 @@
    13.4  local
    13.5    fun mat_strict (con, _) =
    13.6      let
    13.7 -      val goal = mk_trp (strict (%%:(mat_name con)));
    13.8 -      val tacs = [rtac when_strict 1];
    13.9 +      val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
   13.10 +      val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
   13.11      in pg axs_mat_def goal (K tacs) end;
   13.12  
   13.13    val _ = trace " Proving mat_stricts...";
   13.14 @@ -323,10 +323,10 @@
   13.15  
   13.16    fun one_mat c (con, args) =
   13.17      let
   13.18 -      val lhs = %%:(mat_name c) ` con_app con args;
   13.19 +      val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
   13.20        val rhs =
   13.21          if con = c
   13.22 -        then mk_return (mk_ctuple (map %# args))
   13.23 +        then list_ccomb (%:"rhs", map %# args)
   13.24          else mk_fail;
   13.25        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
   13.26        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   13.27 @@ -374,30 +374,32 @@
   13.28  end;
   13.29  
   13.30  local
   13.31 -  val rev_contrapos = @{thm rev_contrapos};
   13.32    fun con_strict (con, args) = 
   13.33      let
   13.34 +      val rules = abs_strict :: @{thms con_strict_rules};
   13.35        fun one_strict vn =
   13.36          let
   13.37            fun f arg = if vname arg = vn then UU else %# arg;
   13.38            val goal = mk_trp (con_app2 con f args === UU);
   13.39 -          val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
   13.40 +          val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
   13.41          in pg con_appls goal (K tacs) end;
   13.42      in map one_strict (nonlazy args) end;
   13.43  
   13.44    fun con_defin (con, args) =
   13.45      let
   13.46 -      val concl = mk_trp (defined (con_app con args));
   13.47 -      val goal = lift_defined %: (nonlazy args, concl);
   13.48 -      fun tacs ctxt = [
   13.49 -        rtac @{thm rev_contrapos} 1,
   13.50 -        eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
   13.51 -        asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   13.52 -    in pg [] goal tacs end;
   13.53 +      fun iff_disj (t, []) = HOLogic.mk_not t
   13.54 +        | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
   13.55 +      val lhs = con_app con args === UU;
   13.56 +      val rhss = map (fn x => %:x === UU) (nonlazy args);
   13.57 +      val goal = mk_trp (iff_disj (lhs, rhss));
   13.58 +      val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
   13.59 +      val rules = rule1 :: @{thms con_defined_iff_rules};
   13.60 +      val tacs = [simp_tac (HOL_ss addsimps rules) 1];
   13.61 +    in pg con_appls goal (K tacs) end;
   13.62  in
   13.63    val _ = trace " Proving con_stricts...";
   13.64    val con_stricts = maps con_strict cons;
   13.65 -  val _ = trace " Proving pat_defins...";
   13.66 +  val _ = trace " Proving con_defins...";
   13.67    val con_defins = map con_defin cons;
   13.68    val con_rews = con_stricts @ con_defins;
   13.69  end;
   13.70 @@ -488,7 +490,6 @@
   13.71  end;
   13.72  
   13.73  val sel_rews = sel_stricts @ sel_defins @ sel_apps;
   13.74 -val rev_contrapos = @{thm rev_contrapos};
   13.75  
   13.76  val _ = trace " Proving dist_les...";
   13.77  val distincts_le =
    14.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Fri Apr 24 18:20:37 2009 +0200
    14.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Fri Apr 24 21:27:49 2009 +0200
    14.3 @@ -36,6 +36,8 @@
    14.4  
    14.5  infixr 6 ->>; val (op ->>) = cfunT;
    14.6  
    14.7 +fun cfunsT (Ts, U) = foldr cfunT U Ts;
    14.8 +
    14.9  fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
   14.10    | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
   14.11  
   14.12 @@ -57,7 +59,9 @@
   14.13    | tupleT [T] = T
   14.14    | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
   14.15  
   14.16 -fun matchT T = body_cfun T ->> maybeT (tupleT (binder_cfun T));
   14.17 +fun matchT (T, U) =
   14.18 +  body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
   14.19 +
   14.20  
   14.21  (*************************************************************************)
   14.22  (***************************** building terms ****************************)
   14.23 @@ -240,10 +244,10 @@
   14.24          fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
   14.25            | result_type T _ = T;
   14.26          val v = Free(n, result_type T vs);
   14.27 -        val m = Const(match_name c, matchT T);
   14.28 -        val k = lambda_ctuple vs rhs;
   14.29 +        val m = Const(match_name c, matchT (T, fastype_of rhs));
   14.30 +        val k = big_lambdas vs rhs;
   14.31        in
   14.32 -        (mk_bind (m`v, k), v, n::taken)
   14.33 +        (m`v`k, v, n::taken)
   14.34        end
   14.35    | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
   14.36    | _ => fixrec_err "pre_build: invalid pattern";
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOLCF/ex/Domain_ex.thy	Fri Apr 24 21:27:49 2009 +0200
    15.3 @@ -0,0 +1,221 @@
    15.4 +(*  Title:      HOLCF/ex/Domain_ex.thy
    15.5 +    Author:     Brian Huffman
    15.6 +*)
    15.7 +
    15.8 +header {* Domain package examples *}
    15.9 +
   15.10 +theory Domain_ex
   15.11 +imports HOLCF
   15.12 +begin
   15.13 +
   15.14 +text {* Domain constructors are strict by default. *}
   15.15 +
   15.16 +domain d1 = d1a | d1b "d1" "d1"
   15.17 +
   15.18 +lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
   15.19 +
   15.20 +text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
   15.21 +
   15.22 +domain d2 = d2a | d2b (lazy "d2")
   15.23 +
   15.24 +lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
   15.25 +
   15.26 +text {* Strict and lazy arguments may be mixed arbitrarily. *}
   15.27 +
   15.28 +domain d3 = d3a | d3b (lazy "d2") "d2"
   15.29 +
   15.30 +lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
   15.31 +
   15.32 +text {* Selectors can be used with strict or lazy constructor arguments. *}
   15.33 +
   15.34 +domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
   15.35 +
   15.36 +lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
   15.37 +
   15.38 +text {* Mixfix declarations can be given for data constructors. *}
   15.39 +
   15.40 +domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
   15.41 +
   15.42 +lemma "d5a \<noteq> x :#: y :#: z" by simp
   15.43 +
   15.44 +text {* Mixfix declarations can also be given for type constructors. *}
   15.45 +
   15.46 +domain ('a, 'b) lazypair (infixl ":*:" 25) =
   15.47 +  lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
   15.48 +
   15.49 +lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
   15.50 +by (rule allI, case_tac p, simp_all)
   15.51 +
   15.52 +text {* Non-recursive constructor arguments can have arbitrary types. *}
   15.53 +
   15.54 +domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
   15.55 +
   15.56 +text {*
   15.57 +  Indirect recusion is allowed for sums, products, lifting, and the
   15.58 +  continuous function space.  However, the domain package currently
   15.59 +  generates induction rules that are too weak.  A fix is planned for
   15.60 +  the next release.
   15.61 +*}
   15.62 +
   15.63 +domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c "'a d7 \<rightarrow> 'a"
   15.64 +
   15.65 +thm d7.ind -- "note the lack of inductive hypotheses"
   15.66 +
   15.67 +text {*
   15.68 +  Indirect recursion using previously-defined datatypes is currently
   15.69 +  not allowed.  This restriction should go away by the next release.
   15.70 +*}
   15.71 +(*
   15.72 +domain 'a slist = SNil | SCons 'a "'a slist"
   15.73 +domain 'a stree = STip | SBranch "'a stree slist" -- "illegal indirect recursion"
   15.74 +*)
   15.75 +
   15.76 +text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
   15.77 +
   15.78 +domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
   15.79 +
   15.80 +text {* Non-regular recursion is not allowed. *}
   15.81 +(*
   15.82 +domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
   15.83 +  -- "illegal direct recursion with different arguments"
   15.84 +domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
   15.85 +  -- "illegal direct recursion with different arguments"
   15.86 +*)
   15.87 +
   15.88 +text {*
   15.89 +  Mutually-recursive datatypes must have all the same type arguments,
   15.90 +  not necessarily in the same order.
   15.91 +*}
   15.92 +
   15.93 +domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
   15.94 +   and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
   15.95 +
   15.96 +text {* Induction rules for flat datatypes have no admissibility side-condition. *}
   15.97 +
   15.98 +domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
   15.99 +
  15.100 +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"
  15.101 +by (rule flattree.ind) -- "no admissibility requirement"
  15.102 +
  15.103 +text {* Trivial datatypes will produce a warning message. *}
  15.104 +
  15.105 +domain triv = triv1 triv triv
  15.106 +  -- "domain Domain_ex.triv is empty!"
  15.107 +
  15.108 +lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
  15.109 +
  15.110 +
  15.111 +subsection {* Generated constants and theorems *}
  15.112 +
  15.113 +domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
  15.114 +
  15.115 +lemmas tree_abs_defined_iff =
  15.116 +  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
  15.117 +
  15.118 +text {* Rules about ismorphism *}
  15.119 +term tree_rep
  15.120 +term tree_abs
  15.121 +thm tree.rep_iso
  15.122 +thm tree.abs_iso
  15.123 +thm tree.iso_rews
  15.124 +
  15.125 +text {* Rules about constructors *}
  15.126 +term Leaf
  15.127 +term Node
  15.128 +thm tree.Leaf_def tree.Node_def
  15.129 +thm tree.exhaust
  15.130 +thm tree.casedist
  15.131 +thm tree.compacts
  15.132 +thm tree.con_rews
  15.133 +thm tree.dist_les
  15.134 +thm tree.dist_eqs
  15.135 +thm tree.inverts
  15.136 +thm tree.injects
  15.137 +
  15.138 +text {* Rules about case combinator *}
  15.139 +term tree_when
  15.140 +thm tree.when_def
  15.141 +thm tree.when_rews
  15.142 +
  15.143 +text {* Rules about selectors *}
  15.144 +term left
  15.145 +term right
  15.146 +thm tree.sel_rews
  15.147 +
  15.148 +text {* Rules about discriminators *}
  15.149 +term is_Leaf
  15.150 +term is_Node
  15.151 +thm tree.dis_rews
  15.152 +
  15.153 +text {* Rules about pattern match combinators *}
  15.154 +term Leaf_pat
  15.155 +term Node_pat
  15.156 +thm tree.pat_rews
  15.157 +
  15.158 +text {* Rules about monadic pattern match combinators *}
  15.159 +term match_Leaf
  15.160 +term match_Node
  15.161 +thm tree.match_rews
  15.162 +
  15.163 +text {* Rules about copy function *}
  15.164 +term tree_copy
  15.165 +thm tree.copy_def
  15.166 +thm tree.copy_rews
  15.167 +
  15.168 +text {* Rules about take function *}
  15.169 +term tree_take
  15.170 +thm tree.take_def
  15.171 +thm tree.take_rews
  15.172 +thm tree.take_lemmas
  15.173 +thm tree.finite_ind
  15.174 +
  15.175 +text {* Rules about finiteness predicate *}
  15.176 +term tree_finite
  15.177 +thm tree.finite_def
  15.178 +thm tree.finites
  15.179 +
  15.180 +text {* Rules about bisimulation predicate *}
  15.181 +term tree_bisim
  15.182 +thm tree.bisim_def
  15.183 +thm tree.coind
  15.184 +
  15.185 +text {* Induction rule *}
  15.186 +thm tree.ind
  15.187 +
  15.188 +
  15.189 +subsection {* Known bugs *}
  15.190 +
  15.191 +text {* Declaring a mixfix with spaces causes some strange parse errors. *}
  15.192 +(*
  15.193 +domain xx = xx ("x y")
  15.194 +  -- "Inner syntax error: unexpected end of input"
  15.195 +
  15.196 +domain 'a foo = foo (sel::"'a") ("a b")
  15.197 +  -- {* Inner syntax error at "= UU" *}
  15.198 +*)
  15.199 +
  15.200 +text {*
  15.201 +  I don't know what is going on here.  The failed proof has to do with
  15.202 +  the finiteness predicate.
  15.203 +*}
  15.204 +(*
  15.205 +domain foo = Foo (lazy "bar") and bar = Bar
  15.206 +  -- "Tactic failed."
  15.207 +*)
  15.208 +
  15.209 +text {* Declaring class constraints on the LHS is currently broken. *}
  15.210 +(*
  15.211 +domain ('a::cpo) box = Box (lazy 'a)
  15.212 +  -- "Malformed YXML encoding: multiple results"
  15.213 +*)
  15.214 +
  15.215 +text {*
  15.216 +  Class constraints on the RHS are not supported yet.  This feature is
  15.217 +  planned to replace the old-style LHS class constraints.
  15.218 +*}
  15.219 +(*
  15.220 +domain 'a box = Box (lazy "'a::cpo")
  15.221 +  -- {* Inconsistent sort constraint for type variable "'a" *}
  15.222 +*)
  15.223 +
  15.224 +end
    16.1 --- a/src/HOLCF/ex/ROOT.ML	Fri Apr 24 18:20:37 2009 +0200
    16.2 +++ b/src/HOLCF/ex/ROOT.ML	Fri Apr 24 21:27:49 2009 +0200
    16.3 @@ -4,4 +4,4 @@
    16.4  *)
    16.5  
    16.6  use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
    16.7 -  "Loop", "Fixrec_ex", "Powerdomain_ex"];
    16.8 +  "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex"];
    17.1 --- a/src/HOLCF/ex/Stream.thy	Fri Apr 24 18:20:37 2009 +0200
    17.2 +++ b/src/HOLCF/ex/Stream.thy	Fri Apr 24 21:27:49 2009 +0200
    17.3 @@ -64,10 +64,10 @@
    17.4  section "scons"
    17.5  
    17.6  lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
    17.7 -by (auto, erule contrapos_pp, simp)
    17.8 +by simp
    17.9  
   17.10  lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
   17.11 -by auto
   17.12 +by simp
   17.13  
   17.14  lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)"
   17.15  by (auto,insert stream.exhaust [of x],auto)
   17.16 @@ -382,7 +382,6 @@
   17.17  
   17.18  lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
   17.19   apply (rule stream.casedist [of x], auto)
   17.20 -    apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
   17.21     apply (simp add: zero_inat_def)
   17.22    apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
   17.23   apply (case_tac "#s") apply (simp_all add: iSuc_Fin)