# HG changeset patch # User haftmann # Date 1240601269 -7200 # Node ID 44637646fa17d1945b51260000f6eb7f40b36f82 # Parent b2fa60d5673540fafd70a1f153c1e72caaa79b0f# Parent 96d053e00ec013fbd55484ec8a65730d6376738f merged diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Domain.thy Fri Apr 24 21:27:49 2009 +0200 @@ -6,6 +6,14 @@ theory Domain imports Ssum Sprod Up One Tr Fixrec +uses + ("Tools/cont_consts.ML") + ("Tools/cont_proc.ML") + ("Tools/domain/domain_library.ML") + ("Tools/domain/domain_syntax.ML") + ("Tools/domain/domain_axioms.ML") + ("Tools/domain/domain_theorems.ML") + ("Tools/domain/domain_extender.ML") begin defaultsort pcpo @@ -193,4 +201,24 @@ lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 + +subsection {* Installing the domain package *} + +lemmas con_strict_rules = + sinl_strict sinr_strict spair_strict1 spair_strict2 + +lemmas con_defin_rules = + sinl_defined sinr_defined spair_defined up_defined ONE_defined + +lemmas con_defined_iff_rules = + sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined + +use "Tools/cont_consts.ML" +use "Tools/cont_proc.ML" +use "Tools/domain/domain_library.ML" +use "Tools/domain/domain_syntax.ML" +use "Tools/domain/domain_axioms.ML" +use "Tools/domain/domain_theorems.ML" +use "Tools/domain/domain_extender.ML" + end diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Fixrec.thy Fri Apr 24 21:27:49 2009 +0200 @@ -475,86 +475,95 @@ defaultsort pcpo definition - match_UU :: "'a \ unit maybe" where - "match_UU = (\ x. fail)" + match_UU :: "'a \ 'c maybe \ 'c maybe" +where + "match_UU = strictify\(\ x k. fail)" definition - match_cpair :: "'a::cpo \ 'b::cpo \ ('a \ 'b) maybe" where - "match_cpair = csplit\(\ x y. return\)" + match_cpair :: "'a::cpo \ 'b::cpo \ ('a \ 'b \ 'c maybe) \ 'c maybe" +where + "match_cpair = (\ x k. csplit\k\x)" definition - match_spair :: "'a \ 'b \ ('a \ 'b) maybe" where - "match_spair = ssplit\(\ x y. return\)" + match_spair :: "'a \ 'b \ ('a \ 'b \ 'c maybe) \ 'c maybe" +where + "match_spair = (\ x k. ssplit\k\x)" definition - match_sinl :: "'a \ 'b \ 'a maybe" where - "match_sinl = sscase\return\(\ y. fail)" + match_sinl :: "'a \ 'b \ ('a \ 'c maybe) \ 'c maybe" +where + "match_sinl = (\ x k. sscase\k\(\ b. fail)\x)" definition - match_sinr :: "'a \ 'b \ 'b maybe" where - "match_sinr = sscase\(\ x. fail)\return" + match_sinr :: "'a \ 'b \ ('b \ 'c maybe) \ 'c maybe" +where + "match_sinr = (\ x k. sscase\(\ a. fail)\k\x)" definition - match_up :: "'a::cpo u \ 'a maybe" where - "match_up = fup\return" + match_up :: "'a::cpo u \ ('a \ 'c maybe) \ 'c maybe" +where + "match_up = (\ x k. fup\k\x)" definition - match_ONE :: "one \ unit maybe" where - "match_ONE = (\ ONE. return\())" + match_ONE :: "one \ 'c maybe \ 'c maybe" +where + "match_ONE = (\ ONE k. k)" + +definition + match_TT :: "tr \ 'c maybe \ 'c maybe" +where + "match_TT = (\ x k. If x then k else fail fi)" definition - match_TT :: "tr \ unit maybe" where - "match_TT = (\ b. If b then return\() else fail fi)" - -definition - match_FF :: "tr \ unit maybe" where - "match_FF = (\ b. If b then fail else return\() fi)" + match_FF :: "tr \ 'c maybe \ 'c maybe" +where + "match_FF = (\ x k. If x then fail else k fi)" lemma match_UU_simps [simp]: - "match_UU\x = fail" + "match_UU\x\k = (if x = \ then \ else fail)" by (simp add: match_UU_def) lemma match_cpair_simps [simp]: - "match_cpair\ = return\" + "match_cpair\\x, y\\k = k\x\y" by (simp add: match_cpair_def) lemma match_spair_simps [simp]: - "\x \ \; y \ \\ \ match_spair\(:x,y:) = return\" - "match_spair\\ = \" + "\x \ \; y \ \\ \ match_spair\(:x, y:)\k = k\x\y" + "match_spair\\\k = \" by (simp_all add: match_spair_def) lemma match_sinl_simps [simp]: - "x \ \ \ match_sinl\(sinl\x) = return\x" - "x \ \ \ match_sinl\(sinr\x) = fail" - "match_sinl\\ = \" + "x \ \ \ match_sinl\(sinl\x)\k = k\x" + "y \ \ \ match_sinl\(sinr\y)\k = fail" + "match_sinl\\\k = \" by (simp_all add: match_sinl_def) lemma match_sinr_simps [simp]: - "x \ \ \ match_sinr\(sinr\x) = return\x" - "x \ \ \ match_sinr\(sinl\x) = fail" - "match_sinr\\ = \" + "x \ \ \ match_sinr\(sinl\x)\k = fail" + "y \ \ \ match_sinr\(sinr\y)\k = k\y" + "match_sinr\\\k = \" by (simp_all add: match_sinr_def) lemma match_up_simps [simp]: - "match_up\(up\x) = return\x" - "match_up\\ = \" + "match_up\(up\x)\k = k\x" + "match_up\\\k = \" by (simp_all add: match_up_def) lemma match_ONE_simps [simp]: - "match_ONE\ONE = return\()" - "match_ONE\\ = \" + "match_ONE\ONE\k = k" + "match_ONE\\\k = \" by (simp_all add: match_ONE_def) lemma match_TT_simps [simp]: - "match_TT\TT = return\()" - "match_TT\FF = fail" - "match_TT\\ = \" + "match_TT\TT\k = k" + "match_TT\FF\k = fail" + "match_TT\\\k = \" by (simp_all add: match_TT_def) lemma match_FF_simps [simp]: - "match_FF\FF = return\()" - "match_FF\TT = fail" - "match_FF\\ = \" + "match_FF\FF\k = k" + "match_FF\TT\k = fail" + "match_FF\\\k = \" by (simp_all add: match_FF_def) subsection {* Mutual recursion *} diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/HOLCF.thy Fri Apr 24 21:27:49 2009 +0200 @@ -9,13 +9,6 @@ Domain ConvexPD Algebraic Universal Sum_Cpo Main uses "holcf_logic.ML" - "Tools/cont_consts.ML" - "Tools/cont_proc.ML" - "Tools/domain/domain_library.ML" - "Tools/domain/domain_syntax.ML" - "Tools/domain/domain_axioms.ML" - "Tools/domain/domain_theorems.ML" - "Tools/domain/domain_extender.ML" "Tools/adm_tac.ML" begin diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Apr 24 21:27:49 2009 +0200 @@ -288,8 +288,7 @@ lemma Cons_not_UU: "a>>s ~= UU" apply (subst Consq_def2) -apply (rule seq.con_rews) -apply (rule Def_not_UU) +apply simp done diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Fri Apr 24 21:27:49 2009 +0200 @@ -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]), diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/IsaMakefile Fri Apr 24 21:27:49 2009 +0200 @@ -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 diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/One.thy --- a/src/HOLCF/One.thy Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/One.thy Fri Apr 24 21:27:49 2009 +0200 @@ -37,8 +37,8 @@ lemma ONE_less_iff [simp]: "ONE \ x \ x = ONE" by (induct x rule: one_induct) simp_all -lemma dist_eq_one [simp]: "ONE \ \" "\ \ ONE" -unfolding ONE_def by simp_all +lemma ONE_defined [simp]: "ONE \ \" +unfolding ONE_def by simp lemma one_neq_iffs [simp]: "x \ ONE \ x = \" diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/cont_consts.ML Fri Apr 24 21:27:49 2009 +0200 @@ -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; diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Fri Apr 24 21:27:49 2009 +0200 @@ -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"; diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Fri Apr 24 21:27:49 2009 +0200 @@ -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; diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_library.ML Fri Apr 24 21:27:49 2009 +0200 @@ -34,8 +34,6 @@ structure Domain_Library = struct -open HOLCFLogic; - exception Impossible of string; fun Imposs msg = raise Impossible ("Domain:"^msg); @@ -72,7 +70,7 @@ | index_vnames([],occupied) = []; in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; -fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS); +fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; (* ----- constructor list handling ----- *) @@ -99,6 +97,17 @@ (* ----- support for type and mixfix expressions ----- *) infixr 5 -->; +fun mk_uT T = Type(@{type_name "u"}, [T]); +fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); +fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); +fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); +val oneT = @{typ one}; +val trT = @{typ tr}; + +infixr 6 ->>; +val op ->> = mk_cfunT; + +fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo}); (* ----- support for term expressions ----- *) diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Fri Apr 24 21:27:49 2009 +0200 @@ -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]) diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Fri Apr 24 21:27:49 2009 +0200 @@ -314,8 +314,8 @@ local fun mat_strict (con, _) = let - val goal = mk_trp (strict (%%:(mat_name con))); - val tacs = [rtac when_strict 1]; + val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU); + val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1]; in pg axs_mat_def goal (K tacs) end; val _ = trace " Proving mat_stricts..."; @@ -323,10 +323,10 @@ fun one_mat c (con, args) = let - val lhs = %%:(mat_name c) ` con_app con args; + val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs"; val rhs = if con = c - then mk_return (mk_ctuple (map %# args)) + then list_ccomb (%:"rhs", map %# args) else mk_fail; val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; @@ -374,30 +374,32 @@ end; local - val rev_contrapos = @{thm rev_contrapos}; fun con_strict (con, args) = let + val rules = abs_strict :: @{thms con_strict_rules}; fun one_strict vn = let fun f arg = if vname arg = vn then UU else %# arg; val goal = mk_trp (con_app2 con f args === UU); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]; + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; in pg con_appls goal (K tacs) end; in map one_strict (nonlazy args) end; fun con_defin (con, args) = let - val concl = mk_trp (defined (con_app con args)); - val goal = lift_defined %: (nonlazy args, concl); - fun tacs ctxt = [ - rtac @{thm rev_contrapos} 1, - eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1, - asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; - in pg [] goal tacs end; + fun iff_disj (t, []) = HOLogic.mk_not t + | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; + val lhs = con_app con args === UU; + val rhss = map (fn x => %:x === UU) (nonlazy args); + val goal = mk_trp (iff_disj (lhs, rhss)); + val rule1 = iso_locale RS @{thm iso.abs_defined_iff}; + val rules = rule1 :: @{thms con_defined_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in pg con_appls goal (K tacs) end; in val _ = trace " Proving con_stricts..."; val con_stricts = maps con_strict cons; - val _ = trace " Proving pat_defins..."; + val _ = trace " Proving con_defins..."; val con_defins = map con_defin cons; val con_rews = con_stricts @ con_defins; end; @@ -488,7 +490,6 @@ end; val sel_rews = sel_stricts @ sel_defins @ sel_apps; -val rev_contrapos = @{thm rev_contrapos}; val _ = trace " Proving dist_les..."; val distincts_le = diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/Tools/fixrec_package.ML Fri Apr 24 21:27:49 2009 +0200 @@ -36,6 +36,8 @@ infixr 6 ->>; val (op ->>) = cfunT; +fun cfunsT (Ts, U) = foldr cfunT U Ts; + fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); @@ -57,7 +59,9 @@ | tupleT [T] = T | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); -fun matchT T = body_cfun T ->> maybeT (tupleT (binder_cfun T)); +fun matchT (T, U) = + body_cfun T ->> cfunsT (binder_cfun T, U) ->> U; + (*************************************************************************) (***************************** building terms ****************************) @@ -240,10 +244,10 @@ fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs | result_type T _ = T; val v = Free(n, result_type T vs); - val m = Const(match_name c, matchT T); - val k = lambda_ctuple vs rhs; + val m = Const(match_name c, matchT (T, fastype_of rhs)); + val k = big_lambdas vs rhs; in - (mk_bind (m`v, k), v, n::taken) + (m`v`k, v, n::taken) end | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) | _ => fixrec_err "pre_build: invalid pattern"; diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/ex/Domain_ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/ex/Domain_ex.thy Fri Apr 24 21:27:49 2009 +0200 @@ -0,0 +1,221 @@ +(* 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\\\y = \" by simp + +text {* Constructors can be made lazy using the @{text "lazy"} keyword. *} + +domain d2 = d2a | d2b (lazy "d2") + +lemma "d2b\x \ \" by simp + +text {* Strict and lazy arguments may be mixed arbitrarily. *} + +domain d3 = d3a | d3b (lazy "d2") "d2" + +lemma "P (d3b\x\y = \) \ P (y = \)" 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 \ \ \ d4b_left\(d4b\x\y) = x" by simp + +text {* Mixfix declarations can be given for data constructors. *} + +domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) + +lemma "d5a \ 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 "\p::('a :*: 'b). p \ lfst\p :*: lsnd\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 \ 'b u" (lazy "('a :*: 'b) \ ('b \ '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 \ int lift" | d7b "'a \ 'a d7" | d7c "'a d7 \ '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 "\P \; P Tip; \x y. \x \ \; y \ \; P x; P y\ \ P (Branch\x\y)\ \ 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) = \" 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." +*) + +text {* Declaring class constraints on the LHS is currently broken. *} +(* +domain ('a::cpo) box = Box (lazy 'a) + -- "Malformed YXML encoding: multiple results" +*) + +text {* + Class constraints on the RHS are not supported yet. This feature is + planned to replace the old-style LHS class constraints. +*} +(* +domain 'a box = Box (lazy "'a::cpo") + -- {* Inconsistent sort constraint for type variable "'a" *} +*) + +end diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/ex/ROOT.ML --- a/src/HOLCF/ex/ROOT.ML Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/ex/ROOT.ML Fri Apr 24 21:27:49 2009 +0200 @@ -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"]; diff -r b2fa60d56735 -r 44637646fa17 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Fri Apr 24 18:20:37 2009 +0200 +++ b/src/HOLCF/ex/Stream.thy Fri Apr 24 21:27:49 2009 +0200 @@ -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 = \ | #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)