1.1 --- a/src/HOLCF/Domain.thy Mon Apr 20 12:27:23 2009 +0200
1.2 +++ b/src/HOLCF/Domain.thy Tue Apr 21 06:44:14 2009 -0700
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 Mon Apr 20 12:27:23 2009 +0200
2.2 +++ b/src/HOLCF/Fixrec.thy Tue Apr 21 06:44:14 2009 -0700
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 Mon Apr 20 12:27:23 2009 +0200
3.2 +++ b/src/HOLCF/HOLCF.thy Tue Apr 21 06:44:14 2009 -0700
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 Mon Apr 20 12:27:23 2009 +0200
4.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Apr 21 06:44:14 2009 -0700
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/One.thy Mon Apr 20 12:27:23 2009 +0200
5.2 +++ b/src/HOLCF/One.thy Tue Apr 21 06:44:14 2009 -0700
5.3 @@ -37,8 +37,8 @@
5.4 lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
5.5 by (induct x rule: one_induct) simp_all
5.6
5.7 -lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
5.8 -unfolding ONE_def by simp_all
5.9 +lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
5.10 +unfolding ONE_def by simp
5.11
5.12 lemma one_neq_iffs [simp]:
5.13 "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
6.1 --- a/src/HOLCF/Tools/cont_consts.ML Mon Apr 20 12:27:23 2009 +0200
6.2 +++ b/src/HOLCF/Tools/cont_consts.ML Tue Apr 21 06:44:14 2009 -0700
6.3 @@ -18,8 +18,6 @@
6.4
6.5 (* misc utils *)
6.6
6.7 -open HOLCFLogic;
6.8 -
6.9 fun first (x,_,_) = x;
6.10 fun second (_,x,_) = x;
6.11 fun third (_,_,x) = x;
6.12 @@ -66,7 +64,7 @@
6.13 (c2,change_arrow n T,mx ),
6.14 trans_rules c2 c n mx) end;
6.15
6.16 -fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
6.17 +fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
6.18 | cfun_arity _ = 0;
6.19
6.20 fun is_contconst (_,_,NoSyn ) = false
7.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML Mon Apr 20 12:27:23 2009 +0200
7.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Tue Apr 21 06:44:14 2009 -0700
7.3 @@ -60,14 +60,18 @@
7.4 (if con'=con then TT else FF) args)) cons))
7.5 in map ddef cons end;
7.6
7.7 - val mat_defs = let
7.8 - fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) ==
7.9 - list_ccomb(%%:(dname^"_when"),map
7.10 - (fn (con',args) => (List.foldr /\#
7.11 - (if con'=con
7.12 - then mk_return (mk_ctuple (map (bound_arg args) args))
7.13 - else mk_fail) args)) cons))
7.14 - in map mdef cons end;
7.15 + val mat_defs =
7.16 + let
7.17 + fun mdef (con,_) =
7.18 + let
7.19 + val k = Bound 0
7.20 + val x = Bound 1
7.21 + fun one_con (con', args') =
7.22 + if con'=con then k else List.foldr /\# mk_fail args'
7.23 + val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
7.24 + val rhs = /\ "x" (/\ "k" (w ` x))
7.25 + in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
7.26 + in map mdef cons end;
7.27
7.28 val pat_defs =
7.29 let
8.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML Mon Apr 20 12:27:23 2009 +0200
8.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Tue Apr 21 06:44:14 2009 -0700
8.3 @@ -1,34 +1,15 @@
8.4 (* Title: HOLCF/Tools/domain/domain_extender.ML
8.5 - ID: $Id$
8.6 Author: David von Oheimb
8.7
8.8 Theory extender for domain command, including theory syntax.
8.9 -
8.10 -###TODO:
8.11 -
8.12 -this definition
8.13 -domain empty = silly empty
8.14 -yields
8.15 -Exception-
8.16 - TERM
8.17 - ("typ_of_term: bad encoding of type",
8.18 - [Abs ("uu", "_", Const ("NONE", "_"))]) raised
8.19 -but this works fine:
8.20 -domain Empty = silly Empty
8.21 -
8.22 -strange syntax errors are produced for:
8.23 -domain xx = xx ("x yy")
8.24 -domain 'a foo = foo (sel::"'a")
8.25 -and bar = bar ("'a dummy")
8.26 -
8.27 *)
8.28
8.29 signature DOMAIN_EXTENDER =
8.30 sig
8.31 - val add_domain: string * ((bstring * string list) *
8.32 + val add_domain: string * ((bstring * string list * mixfix) *
8.33 (string * mixfix * (bool * string option * string) list) list) list
8.34 -> theory -> theory
8.35 - val add_domain_i: string * ((bstring * string list) *
8.36 + val add_domain_i: string * ((bstring * string list * mixfix) *
8.37 (string * mixfix * (bool * string option * typ) list) list) list
8.38 -> theory -> theory
8.39 end;
8.40 @@ -99,16 +80,17 @@
8.41
8.42 fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
8.43 let
8.44 - val dtnvs = map ((fn (dname,vs) =>
8.45 - (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
8.46 + val dtnvs = map ((fn (dname,vs,mx) =>
8.47 + (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs, mx))
8.48 o fst) eqs''';
8.49 val cons''' = map snd eqs''';
8.50 - fun thy_type (dname,tvars) = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn);
8.51 - fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
8.52 - val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
8.53 + fun thy_type (dname,tvars,mx) = (Binding.name (Long_Name.base_name dname), length tvars, mx);
8.54 + fun thy_arity (dname,tvars,mx) = (dname, map (snd o dest_TFree) tvars, pcpoS);
8.55 + val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
8.56 |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
8.57 val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
8.58 - val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
8.59 + val dtnvs' = map (fn (dname,vs,mx) => (dname,vs)) dtnvs;
8.60 + val eqs' = check_and_sort_domain (dtnvs',cons'') thy'';
8.61 val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
8.62 val dts = map (Type o fst) eqs';
8.63 val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
8.64 @@ -148,7 +130,7 @@
8.65
8.66 val _ = OuterKeyword.keyword "lazy";
8.67
8.68 -val dest_decl =
8.69 +val dest_decl : (bool * string option * string) parser =
8.70 P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
8.71 (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
8.72 || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
8.73 @@ -156,25 +138,37 @@
8.74 || P.typ >> (fn t => (false,NONE,t));
8.75
8.76 val cons_decl =
8.77 - P.name -- Scan.repeat dest_decl -- P.opt_mixfix
8.78 - >> (fn ((c, ds), mx) => (c, mx, ds));
8.79 + P.name -- Scan.repeat dest_decl -- P.opt_mixfix;
8.80
8.81 -val type_var' = (P.type_ident ^^
8.82 - Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
8.83 -val type_args' = type_var' >> single ||
8.84 - P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
8.85 - Scan.succeed [];
8.86 +val type_var' =
8.87 + (P.type_ident ^^ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
8.88
8.89 -val domain_decl = (type_args' -- P.name >> Library.swap) --
8.90 - (P.$$$ "=" |-- P.enum1 "|" cons_decl);
8.91 +val type_args' =
8.92 + type_var' >> single ||
8.93 + P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
8.94 + Scan.succeed [];
8.95 +
8.96 +val domain_decl =
8.97 + (type_args' -- P.name -- P.opt_infix) --
8.98 + (P.$$$ "=" |-- P.enum1 "|" cons_decl);
8.99 +
8.100 val domains_decl =
8.101 - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
8.102 - >> (fn (opt_name, doms) =>
8.103 - (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
8.104 + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
8.105 + P.and_list1 domain_decl;
8.106 +
8.107 +fun mk_domain (opt_name : string option, doms : (((string list * bstring) * mixfix) *
8.108 + ((string * (bool * string option * string) list) * mixfix) list) list ) =
8.109 + let
8.110 + val names = map (fn (((_, t), _), _) => t) doms;
8.111 + val specs = map (fn (((vs, t), mx), cons) =>
8.112 + ((t, vs, mx), map (fn ((c, ds), mx) => (c, mx, ds)) cons)) doms;
8.113 + val big_name =
8.114 + case opt_name of NONE => space_implode "_" names | SOME s => s;
8.115 + in add_domain (big_name, specs) end;
8.116
8.117 val _ =
8.118 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
8.119 - (domains_decl >> (Toplevel.theory o add_domain));
8.120 + (domains_decl >> (Toplevel.theory o mk_domain));
8.121
8.122 end;
8.123
9.1 --- a/src/HOLCF/Tools/domain/domain_library.ML Mon Apr 20 12:27:23 2009 +0200
9.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML Tue Apr 21 06:44:14 2009 -0700
9.3 @@ -34,8 +34,6 @@
9.4
9.5 structure Domain_Library = struct
9.6
9.7 -open HOLCFLogic;
9.8 -
9.9 exception Impossible of string;
9.10 fun Imposs msg = raise Impossible ("Domain:"^msg);
9.11
9.12 @@ -72,7 +70,7 @@
9.13 | index_vnames([],occupied) = [];
9.14 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
9.15
9.16 -fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
9.17 +fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
9.18 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
9.19
9.20 (* ----- constructor list handling ----- *)
9.21 @@ -99,6 +97,17 @@
9.22 (* ----- support for type and mixfix expressions ----- *)
9.23
9.24 infixr 5 -->;
9.25 +fun mk_uT T = Type(@{type_name "u"}, [T]);
9.26 +fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
9.27 +fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
9.28 +fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
9.29 +val oneT = @{typ one};
9.30 +val trT = @{typ tr};
9.31 +
9.32 +infixr 6 ->>;
9.33 +val op ->> = mk_cfunT;
9.34 +
9.35 +fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
9.36
9.37 (* ----- support for term expressions ----- *)
9.38
10.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML Mon Apr 20 12:27:23 2009 +0200
10.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Tue Apr 21 06:44:14 2009 -0700
10.3 @@ -46,12 +46,14 @@
10.4 (* strictly speaking, these constants have one argument,
10.5 but the mixfix (without arguments) is introduced only
10.6 to generate parse rules for non-alphanumeric names*)
10.7 - fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
10.8 + fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
10.9 + if tvar mem typevars then freetvar ("t"^s) n else tvar end;
10.10 + fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
10.11 + fun mat (con,s,args) = (mat_name_ con,
10.12 + mk_matT(dtype, map third args, freetvar "t" 1),
10.13 Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
10.14 fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
10.15 fun sel (_ ,_,args) = List.mapPartial sel1 args;
10.16 - fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
10.17 - if tvar mem typevars then freetvar ("t"^s) n else tvar end;
10.18 fun mk_patT (a,b) = a ->> mk_maybeT b;
10.19 fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
10.20 fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
11.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Apr 20 12:27:23 2009 +0200
11.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Tue Apr 21 06:44:14 2009 -0700
11.3 @@ -314,8 +314,8 @@
11.4 local
11.5 fun mat_strict (con, _) =
11.6 let
11.7 - val goal = mk_trp (strict (%%:(mat_name con)));
11.8 - val tacs = [rtac when_strict 1];
11.9 + val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
11.10 + val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
11.11 in pg axs_mat_def goal (K tacs) end;
11.12
11.13 val _ = trace " Proving mat_stricts...";
11.14 @@ -323,10 +323,10 @@
11.15
11.16 fun one_mat c (con, args) =
11.17 let
11.18 - val lhs = %%:(mat_name c) ` con_app con args;
11.19 + val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
11.20 val rhs =
11.21 if con = c
11.22 - then mk_return (mk_ctuple (map %# args))
11.23 + then list_ccomb (%:"rhs", map %# args)
11.24 else mk_fail;
11.25 val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
11.26 val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
11.27 @@ -374,30 +374,32 @@
11.28 end;
11.29
11.30 local
11.31 - val rev_contrapos = @{thm rev_contrapos};
11.32 fun con_strict (con, args) =
11.33 let
11.34 + val rules = abs_strict :: @{thms con_strict_rules};
11.35 fun one_strict vn =
11.36 let
11.37 fun f arg = if vname arg = vn then UU else %# arg;
11.38 val goal = mk_trp (con_app2 con f args === UU);
11.39 - val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
11.40 + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
11.41 in pg con_appls goal (K tacs) end;
11.42 in map one_strict (nonlazy args) end;
11.43
11.44 fun con_defin (con, args) =
11.45 let
11.46 - val concl = mk_trp (defined (con_app con args));
11.47 - val goal = lift_defined %: (nonlazy args, concl);
11.48 - fun tacs ctxt = [
11.49 - rtac @{thm rev_contrapos} 1,
11.50 - eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
11.51 - asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
11.52 - in pg [] goal tacs end;
11.53 + fun iff_disj (t, []) = HOLogic.mk_not t
11.54 + | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
11.55 + val lhs = con_app con args === UU;
11.56 + val rhss = map (fn x => %:x === UU) (nonlazy args);
11.57 + val goal = mk_trp (iff_disj (lhs, rhss));
11.58 + val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
11.59 + val rules = rule1 :: @{thms con_defined_iff_rules};
11.60 + val tacs = [simp_tac (HOL_ss addsimps rules) 1];
11.61 + in pg con_appls goal (K tacs) end;
11.62 in
11.63 val _ = trace " Proving con_stricts...";
11.64 val con_stricts = maps con_strict cons;
11.65 - val _ = trace " Proving pat_defins...";
11.66 + val _ = trace " Proving con_defins...";
11.67 val con_defins = map con_defin cons;
11.68 val con_rews = con_stricts @ con_defins;
11.69 end;
11.70 @@ -488,7 +490,6 @@
11.71 end;
11.72
11.73 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
11.74 -val rev_contrapos = @{thm rev_contrapos};
11.75
11.76 val _ = trace " Proving dist_les...";
11.77 val distincts_le =
12.1 --- a/src/HOLCF/Tools/fixrec_package.ML Mon Apr 20 12:27:23 2009 +0200
12.2 +++ b/src/HOLCF/Tools/fixrec_package.ML Tue Apr 21 06:44:14 2009 -0700
12.3 @@ -36,6 +36,8 @@
12.4
12.5 infixr 6 ->>; val (op ->>) = cfunT;
12.6
12.7 +fun cfunsT (Ts, U) = foldr cfunT U Ts;
12.8 +
12.9 fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
12.10 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
12.11
12.12 @@ -57,7 +59,9 @@
12.13 | tupleT [T] = T
12.14 | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
12.15
12.16 -fun matchT T = body_cfun T ->> maybeT (tupleT (binder_cfun T));
12.17 +fun matchT (T, U) =
12.18 + body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
12.19 +
12.20
12.21 (*************************************************************************)
12.22 (***************************** building terms ****************************)
12.23 @@ -240,10 +244,10 @@
12.24 fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
12.25 | result_type T _ = T;
12.26 val v = Free(n, result_type T vs);
12.27 - val m = Const(match_name c, matchT T);
12.28 - val k = lambda_ctuple vs rhs;
12.29 + val m = Const(match_name c, matchT (T, fastype_of rhs));
12.30 + val k = big_lambdas vs rhs;
12.31 in
12.32 - (mk_bind (m`v, k), v, n::taken)
12.33 + (m`v`k, v, n::taken)
12.34 end
12.35 | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
12.36 | _ => fixrec_err "pre_build: invalid pattern";
13.1 --- a/src/HOLCF/ex/Stream.thy Mon Apr 20 12:27:23 2009 +0200
13.2 +++ b/src/HOLCF/ex/Stream.thy Tue Apr 21 06:44:14 2009 -0700
13.3 @@ -64,10 +64,10 @@
13.4 section "scons"
13.5
13.6 lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
13.7 -by (auto, erule contrapos_pp, simp)
13.8 +by simp
13.9
13.10 lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
13.11 -by auto
13.12 +by simp
13.13
13.14 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)"
13.15 by (auto,insert stream.exhaust [of x],auto)
13.16 @@ -382,7 +382,6 @@
13.17
13.18 lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
13.19 apply (rule stream.casedist [of x], auto)
13.20 - apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
13.21 apply (simp add: zero_inat_def)
13.22 apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
13.23 apply (case_tac "#s") apply (simp_all add: iSuc_Fin)