--- a/src/HOLCF/Domain.thy Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Domain.thy Tue Apr 21 17:02:48 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
--- a/src/HOLCF/Fixrec.thy Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Fixrec.thy Tue Apr 21 17:02:48 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 *}
--- a/src/HOLCF/HOLCF.thy Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/HOLCF.thy Tue Apr 21 17:02:48 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
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Apr 21 17:02:48 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
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Apr 21 17:02:48 2009 -0700
@@ -347,12 +347,12 @@
val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list
atyp statetupel trans;
val thy2 = (thy
-|> ContConsts.add_consts
-[(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn),
-(automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn),
-(automaton_name ^ "_trans",
+|> Sign.add_consts
+[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
+(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
+(Binding.name (automaton_name ^ "_trans"),
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
-(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
+(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
|> add_defs
[(automaton_name ^ "_initial_def",
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
@@ -386,8 +386,8 @@
val comp_list = clist aut_list;
in
thy
-|> ContConsts.add_consts_i
-[(automaton_name,
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
Type("*",
[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
Type("*",[Type("set",[st_typ]),
@@ -407,8 +407,8 @@
val rest_set = action_set_string thy acttyp actlist
in
thy
-|> ContConsts.add_consts_i
-[(automaton_name, auttyp,NoSyn)]
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
|> add_defs
[(automaton_name ^ "_def",
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
@@ -421,8 +421,8 @@
val hid_set = action_set_string thy acttyp actlist
in
thy
-|> ContConsts.add_consts_i
-[(automaton_name, auttyp,NoSyn)]
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
|> add_defs
[(automaton_name ^ "_def",
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
@@ -441,8 +441,8 @@
val acttyp = ren_act_type_of thy fun_name
in
thy
-|> ContConsts.add_consts_i
-[(automaton_name,
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
Type("*",
[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
Type("*",[Type("set",[st_typ]),
--- a/src/HOLCF/IsaMakefile Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/IsaMakefile Tue Apr 21 17:02:48 2009 -0700
@@ -87,10 +87,19 @@
HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
-$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \
- ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
+$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
+ ../HOL/Library/Nat_Infinity.thy \
+ ex/Dagstuhl.thy \
+ ex/Dnat.thy \
+ ex/Domain_ex.thy \
+ ex/Fix2.thy \
+ ex/Fixrec_ex.thy \
+ ex/Focus_ex.thy \
+ ex/Hoare.thy \
+ ex/Loop.thy \
ex/Powerdomain_ex.thy \
- ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
+ ex/Stream.thy \
+ ex/ROOT.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
--- a/src/HOLCF/One.thy Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/One.thy Tue Apr 21 17:02:48 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>"
--- a/src/HOLCF/Tools/cont_consts.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML Tue Apr 21 17:02:48 2009 -0700
@@ -8,8 +8,8 @@
signature CONT_CONSTS =
sig
- val add_consts: (bstring * string * mixfix) list -> theory -> theory
- val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
+ val add_consts: (binding * string * mixfix) list -> theory -> theory
+ val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
end;
structure ContConsts: CONT_CONSTS =
@@ -18,8 +18,6 @@
(* misc utils *)
-open HOLCFLogic;
-
fun first (x,_,_) = x;
fun second (_,x,_) = x;
fun third (_,_,x) = x;
@@ -51,29 +49,33 @@
declaration with the original name, type ...=>..., and the original mixfix
is generated and connected to the other declaration via some translation.
*)
-fun fix_mixfix (syn , T, mx as Infix p ) =
- (Syntax.const_name mx syn, T, InfixName (syn, p))
- | fix_mixfix (syn , T, mx as Infixl p ) =
- (Syntax.const_name mx syn, T, InfixlName (syn, p))
- | fix_mixfix (syn , T, mx as Infixr p ) =
- (Syntax.const_name mx syn, T, InfixrName (syn, p))
+fun const_binding mx = Binding.name o Syntax.const_name mx o Binding.name_of;
+
+fun fix_mixfix (syn , T, mx as Infix p ) =
+ (const_binding mx syn, T, InfixName (Binding.name_of syn, p))
+ | fix_mixfix (syn , T, mx as Infixl p ) =
+ (const_binding mx syn, T, InfixlName (Binding.name_of syn, p))
+ | fix_mixfix (syn , T, mx as Infixr p ) =
+ (const_binding mx syn, T, InfixrName (Binding.name_of syn, p))
| fix_mixfix decl = decl;
+
fun transform decl = let
val (c, T, mx) = fix_mixfix decl;
- val c2 = "_cont_" ^ c;
+ val c1 = Binding.name_of c;
+ val c2 = "_cont_" ^ c1;
val n = Syntax.mixfix_args mx
- in ((c , T,NoSyn),
- (c2,change_arrow n T,mx ),
- trans_rules c2 c n mx) end;
+ in ((c, T, NoSyn),
+ (Binding.name c2, change_arrow n T, mx),
+ trans_rules c2 c1 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
| is_contconst (_,_,Binder _) = false
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name mx c));
+ quote (Syntax.const_name mx (Binding.name_of c)));
(* add_consts(_i) *)
@@ -85,7 +87,7 @@
val transformed_decls = map transform contconst_decls;
in
thy
- |> (Sign.add_consts_i o map (upd_first Binding.name))
+ |> Sign.add_consts_i
(normal_decls @ map first transformed_decls @ map second transformed_decls)
|> Sign.add_trrules_i (maps third transformed_decls)
end;
@@ -100,7 +102,7 @@
val _ =
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
+ (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts));
end;
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Tue Apr 21 17:02:48 2009 -0700
@@ -4,7 +4,14 @@
Syntax generator for domain command.
*)
-structure Domain_Axioms = struct
+signature DOMAIN_AXIOMS =
+sig
+ val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory
+end;
+
+
+structure Domain_Axioms : DOMAIN_AXIOMS =
+struct
local
@@ -60,14 +67,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
@@ -135,7 +146,7 @@
in (* local *)
-fun add_axioms (comp_dnam, eqs : eq list) thy' = let
+fun add_axioms comp_dnam (eqs : eq list) thy' = let
val comp_dname = Sign.full_bname thy' comp_dnam;
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
--- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Tue Apr 21 17:02:48 2009 -0700
@@ -1,35 +1,16 @@
(* 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) *
- (string * mixfix * (bool * string option * string) list) list) list
+ val add_domain_cmd: string -> (string list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
- val add_domain_i: string * ((bstring * string list) *
- (string * mixfix * (bool * string option * typ) list) list) list
+ val add_domain: string -> (string list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
end;
@@ -39,17 +20,21 @@
open Domain_Library;
(* ----- general testing and preprocessing of constructor list -------------- *)
-fun check_and_sort_domain (dtnvs: (string * typ list) list,
- cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
+fun check_and_sort_domain
+ (dtnvs : (string * typ list) list)
+ (cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list)
+ (sg : theory)
+ : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
let
val defaultS = Sign.defaultS sg;
val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of
+ val test_dupl_cons = (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups));
- val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
- (List.concat (map third (List.concat cons'')))) of
+ val test_dupl_sels = (case duplicates (op =) (map Binding.name_of (List.mapPartial second
+ (List.concat (map second (List.concat cons''))))) of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
[] => false | dups => error("Duplicate type arguments: "
@@ -90,26 +75,31 @@
| analyse indirect (TVar _) = Imposs "extender:analyse";
fun check_pcpo T = if pcpo_type sg T then T
else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
- val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
+ val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false)));
in ((dname,distinct_typevars), map analyse_con cons') end;
in ListPair.map analyse_equation (dtnvs,cons'')
end; (* let *)
(* ----- calls for building new thy and thms -------------------------------- *)
-fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
+fun gen_add_domain
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : (string list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
let
- val dtnvs = map ((fn (dname,vs) =>
- (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
- 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)
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map (Syntax.read_typ_global thy''') vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' 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 thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
+ val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+ val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = 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';
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
@@ -118,16 +108,16 @@
in if Symbol.is_letter c then c else "t" end
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun one_con (con,mx,args) =
- ((Syntax.const_name mx con),
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
find_index_eq tp dts,
DatatypeAux.dtyp_of_typ new_dts tp),
- sel,vn))
+ Option.map Binding.name_of sel,vn))
(args,(mk_var_names(map (typid o third) args)))
) : cons;
val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
+ val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
Domain_Theorems.theorems (eq, eqs)) eqs
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
@@ -138,8 +128,8 @@
|> Sign.parent_path
end;
-val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain Syntax.read_typ_global;
+val add_domain = gen_add_domain Sign.certify_typ;
+val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
(** outer syntax **)
@@ -148,33 +138,47 @@
val _ = OuterKeyword.keyword "lazy";
-val dest_decl =
+val dest_decl : (bool * binding option * string) parser =
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
|| P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
>> (fn t => (true,NONE,t))
|| 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.binding -- 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.binding -- 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 * binding) * mixfix) *
+ ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
+ let
+ val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
+ val specs : (string list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list =
+ map (fn (((vs, t), mx), cons) =>
+ (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
+ val comp_dnam =
+ case opt_name of NONE => space_implode "_" names | SOME s => s;
+ in add_domain_cmd comp_dnam 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;
--- a/src/HOLCF/Tools/domain/domain_library.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Tue Apr 21 17:02:48 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 ----- *)
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Tue Apr 21 17:02:48 2009 -0700
@@ -4,32 +4,42 @@
Syntax generator for domain command.
*)
-structure Domain_Syntax = struct
+signature DOMAIN_SYNTAX =
+sig
+ val add_syntax: string -> ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
+end;
+
+
+structure Domain_Syntax : DOMAIN_SYNTAX =
+struct
local
open Domain_Library;
infixr 5 -->; infixr 6 ->>;
fun calc_syntax dtypeprod ((dname, typevars),
- (cons': (string * mixfix * (bool * string option * typ) list) list)) =
+ (cons': (binding * (bool * binding option * typ) list * mixfix) list)) : ((binding * typ * mixfix) list * ast Syntax.trrule list) =
let
(* ----- constants concerning the isomorphism ------------------------------- *)
local
fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
- fun prod (_,_,args) = if args = [] then oneT
- else foldr1 mk_sprodT (map opt_lazy args);
+ fun prod (_,args,_) = case args of [] => oneT
+ | _ => foldr1 mk_sprodT (map opt_lazy args);
fun freetvar s = let val tvar = mk_TFree s in
if tvar mem typevars then freetvar ("t"^s) else tvar end;
- fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args);
+ fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
in
val dtype = Type(dname,typevars);
val dtype2 = foldr1 mk_ssumT (map prod cons');
val dnam = Long_Name.base_name dname;
- val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
- val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
- val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
+ fun dbind s = Binding.name (dnam ^ s);
+ val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
end;
(* ----- constants concerning constructors, discriminators, and selectors --- *)
@@ -40,23 +50,28 @@
else c::esc cs
| esc [] = []
in implode o esc o Symbol.explode end;
- fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
- fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
- Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
+ fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+ fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+ fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+ fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
+ fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
(* 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)),
- 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_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+ fun mat (con,args,mx) = (mat_name_ con,
+ mk_matT(dtype, map third args, freetvar "t" 1),
+ Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
+ fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+ fun sel (con,args,mx) = List.mapPartial sel1 args;
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) --->
+ fun pat (con,args,mx) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
- Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
+ Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
in
val consts_con = map con cons';
@@ -68,14 +83,14 @@
(* ----- constants concerning induction ------------------------------------- *)
- val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
- val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn);
+ val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
(* ----- case translation --------------------------------------------------- *)
local open Syntax in
local
- fun c_ast con mx = Constant (Syntax.const_name mx con);
+ fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
fun expvar n = Variable ("e"^(string_of_int n));
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
(string_of_int m));
@@ -83,9 +98,9 @@
fun app s (l,r) = mk_appl (Constant s) [l,r];
val cabs = app "_cabs";
val capp = app "Rep_CFun";
- fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
- fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
+ fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+ fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+ fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
fun when1 n m = if n = m then arg1 n else K (Constant "UU");
fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
@@ -101,10 +116,10 @@
(cabs (con1 n (con,mx,args), expvar n),
Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
- val Case_trans = List.concat (map (fn (con,mx,args) =>
+ val Case_trans = List.concat (map (fn (con,args,mx) =>
let
val cname = c_ast con mx;
- val pname = Constant (pat_name_ con);
+ val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
val ns = 1 upto length args;
val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
@@ -130,16 +145,19 @@
in (* local *)
-fun add_syntax (comp_dnam,eqs': ((string * typ list) *
- (string * mixfix * (bool * string option * typ) list) list) list) thy'' =
+fun add_syntax
+ (comp_dnam : string)
+ (eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (thy'' : theory) =
let
val dtypes = map (Type o fst) eqs';
val boolT = HOLogic.boolT;
val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
- val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
- val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
- val ctt = map (calc_syntax funprod) eqs';
+ val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+ val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+ val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
(if length eqs'>1 then [const_copy] else[])@
[const_bisim])
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Tue Apr 21 17:02:48 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 =
--- a/src/HOLCF/Tools/fixrec_package.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Tue Apr 21 17:02:48 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";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Domain_ex.thy Tue Apr 21 17:02:48 2009 -0700
@@ -0,0 +1,206 @@
+(* Title: HOLCF/ex/Domain_ex.thy
+ Author: Brian Huffman
+*)
+
+header {* Domain package examples *}
+
+theory Domain_ex
+imports HOLCF
+begin
+
+text {* Domain constructors are strict by default. *}
+
+domain d1 = d1a | d1b "d1" "d1"
+
+lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
+
+text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
+
+domain d2 = d2a | d2b (lazy "d2")
+
+lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
+
+text {* Strict and lazy arguments may be mixed arbitrarily. *}
+
+domain d3 = d3a | d3b (lazy "d2") "d2"
+
+lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
+
+text {* Selectors can be used with strict or lazy constructor arguments. *}
+
+domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
+
+lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
+
+text {* Mixfix declarations can be given for data constructors. *}
+
+domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
+
+lemma "d5a \<noteq> x :#: y :#: z" by simp
+
+text {* Mixfix declarations can also be given for type constructors. *}
+
+domain ('a, 'b) lazypair (infixl ":*:" 25) =
+ lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
+
+lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
+by (rule allI, case_tac p, simp_all)
+
+text {* Non-recursive constructor arguments can have arbitrary types. *}
+
+domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
+
+text {*
+ Indirect recusion is allowed for sums, products, lifting, and the
+ continuous function space. However, the domain package currently
+ generates induction rules that are too weak. A fix is planned for
+ the next release.
+*}
+
+domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c "'a d7 \<rightarrow> 'a"
+
+thm d7.ind -- "note the lack of inductive hypotheses"
+
+text {*
+ Indirect recursion using previously-defined datatypes is currently
+ not allowed. This restriction should go away by the next release.
+*}
+(*
+domain 'a slist = SNil | SCons 'a "'a slist"
+domain 'a stree = STip | SBranch "'a stree slist" -- "illegal indirect recursion"
+*)
+
+text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
+
+domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
+
+text {* Non-regular recursion is not allowed. *}
+(*
+domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
+ -- "illegal direct recursion with different arguments"
+domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
+ -- "illegal direct recursion with different arguments"
+*)
+
+text {*
+ Mutually-recursive datatypes must have all the same type arguments,
+ not necessarily in the same order.
+*}
+
+domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
+ and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
+
+text {* Induction rules for flat datatypes have no admissibility side-condition. *}
+
+domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
+
+lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
+by (rule flattree.ind) -- "no admissibility requirement"
+
+text {* Trivial datatypes will produce a warning message. *}
+
+domain triv = triv1 triv triv
+ -- "domain Domain_ex.triv is empty!"
+
+lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
+
+
+subsection {* Generated constants and theorems *}
+
+domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
+
+lemmas tree_abs_defined_iff =
+ iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
+
+text {* Rules about ismorphism *}
+term tree_rep
+term tree_abs
+thm tree.rep_iso
+thm tree.abs_iso
+thm tree.iso_rews
+
+text {* Rules about constructors *}
+term Leaf
+term Node
+thm tree.Leaf_def tree.Node_def
+thm tree.exhaust
+thm tree.casedist
+thm tree.compacts
+thm tree.con_rews
+thm tree.dist_les
+thm tree.dist_eqs
+thm tree.inverts
+thm tree.injects
+
+text {* Rules about case combinator *}
+term tree_when
+thm tree.when_def
+thm tree.when_rews
+
+text {* Rules about selectors *}
+term left
+term right
+thm tree.sel_rews
+
+text {* Rules about discriminators *}
+term is_Leaf
+term is_Node
+thm tree.dis_rews
+
+text {* Rules about pattern match combinators *}
+term Leaf_pat
+term Node_pat
+thm tree.pat_rews
+
+text {* Rules about monadic pattern match combinators *}
+term match_Leaf
+term match_Node
+thm tree.match_rews
+
+text {* Rules about copy function *}
+term tree_copy
+thm tree.copy_def
+thm tree.copy_rews
+
+text {* Rules about take function *}
+term tree_take
+thm tree.take_def
+thm tree.take_rews
+thm tree.take_lemmas
+thm tree.finite_ind
+
+text {* Rules about finiteness predicate *}
+term tree_finite
+thm tree.finite_def
+thm tree.finites
+
+text {* Rules about bisimulation predicate *}
+term tree_bisim
+thm tree.bisim_def
+thm tree.coind
+
+text {* Induction rule *}
+thm tree.ind
+
+
+subsection {* Known bugs *}
+
+text {* Declaring a mixfix with spaces causes some strange parse errors. *}
+(*
+domain xx = xx ("x y")
+ -- "Inner syntax error: unexpected end of input"
+
+domain 'a foo = foo (sel::"'a") ("a b")
+ -- {* Inner syntax error at "= UU" *}
+*)
+
+text {*
+ I don't know what is going on here. The failed proof has to do with
+ the finiteness predicate.
+*}
+(*
+domain foo = Foo (lazy "bar") and bar = Bar
+ -- "Tactic failed."
+*)
+
+end
--- a/src/HOLCF/ex/ROOT.ML Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/ex/ROOT.ML Tue Apr 21 17:02:48 2009 -0700
@@ -4,4 +4,4 @@
*)
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
- "Loop", "Fixrec_ex", "Powerdomain_ex"];
+ "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex"];
--- a/src/HOLCF/ex/Stream.thy Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOLCF/ex/Stream.thy Tue Apr 21 17:02:48 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)