# HG changeset patch # User huffman # Date 1287271362 25200 # Node ID 8f8f18a8868501be694aa5eadd2d2899b0f64c87 # Parent 876689e6bbdf38effc2d2c87365014fd0781bea9 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check diff -r 876689e6bbdf -r 8f8f18a88685 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Sat Oct 16 15:26:30 2010 -0700 +++ b/src/HOLCF/Domain.thy Sat Oct 16 16:22:42 2010 -0700 @@ -10,7 +10,6 @@ ("Tools/cont_consts.ML") ("Tools/cont_proc.ML") ("Tools/Domain/domain_constructors.ML") - ("Tools/Domain/domain_library.ML") ("Tools/Domain/domain_axioms.ML") ("Tools/Domain/domain_theorems.ML") ("Tools/Domain/domain_extender.ML") @@ -154,7 +153,6 @@ use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" -use "Tools/Domain/domain_library.ML" use "Tools/Domain/domain_axioms.ML" use "Tools/Domain/domain_constructors.ML" use "Tools/Domain/domain_theorems.ML" diff -r 876689e6bbdf -r 8f8f18a88685 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Sat Oct 16 15:26:30 2010 -0700 +++ b/src/HOLCF/IsaMakefile Sat Oct 16 16:22:42 2010 -0700 @@ -74,7 +74,6 @@ Tools/Domain/domain_axioms.ML \ Tools/Domain/domain_constructors.ML \ Tools/Domain/domain_isomorphism.ML \ - Tools/Domain/domain_library.ML \ Tools/Domain/domain_take_proofs.ML \ Tools/Domain/domain_theorems.ML \ Tools/fixrec.ML \ diff -r 876689e6bbdf -r 8f8f18a88685 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Sat Oct 16 15:26:30 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Sat Oct 16 16:22:42 2010 -0700 @@ -35,7 +35,15 @@ structure Domain_Extender :> DOMAIN_EXTENDER = struct -open Domain_Library; +open HOLCF_Library; + +fun first (x,_,_) = x; +fun second (_,x,_) = x; +fun third (_,_,x) = x; + +fun upd_first f (x,y,z) = (f x, y, z); +fun upd_second f (x,y,z) = ( x, f y, z); +fun upd_third f (x,y,z) = ( x, y, f z); (* ----- general testing and preprocessing of constructor list -------------- *) fun check_and_sort_domain @@ -94,22 +102,22 @@ | SOME typevars => if indirect then error ("Indirect recursion of type " ^ - quote (string_of_typ thy t)) + quote (Syntax.string_of_typ_global thy t)) else if dname <> s orelse (** BUG OR FEATURE?: mutual recursion may use different arguments **) remove_sorts typevars = remove_sorts typl then Type(s,map (analyse true) typl) else error ("Direct recursion of type " ^ - quote (string_of_typ thy t) ^ + quote (Syntax.string_of_typ_global thy t) ^ " with different arguments")) - | analyse indirect (TVar _) = Imposs "extender:analyse"; + | analyse indirect (TVar _) = error "extender:analyse"; fun check_pcpo lazy T = let val sort = arg_sort lazy in if Sign.of_sort thy (T, sort) then T else error ("Constructor argument type is not of sort " ^ Syntax.string_of_sort_global thy sort ^ ": " ^ - string_of_typ thy T) + Syntax.string_of_typ_global thy T) end; fun analyse_arg (lazy, sel, T) = (lazy, sel, check_pcpo lazy (analyse false T)); @@ -167,7 +175,7 @@ check_and_sort_domain arg_sort dtnvs' cons'' tmp_thy; val dts : typ list = map (Type o fst) eqs'; - fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T; + fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; fun mk_con_typ (bind, args, mx) = if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); @@ -179,28 +187,17 @@ val ((iso_infos, take_info), thy) = add_isos iso_spec thy; - val new_dts : (string * string list) list = - map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; - fun one_con (con,args,mx) : cons = - (Binding.name_of con, (* FIXME preverse binding (!?) *) - ListPair.map (fn ((lazy,sel,tp),vn) => - mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn)) - (args, Datatype_Prop.make_tnames (map third args))); - val eqs : eq list = - map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val (constr_infos, thy) = thy |> fold_map (fn ((dbind, (_,cs)), info) => Domain_Constructors.add_domain_constructors dbind cs info) (dbinds ~~ eqs' ~~ iso_infos); - val (take_rews, theorems_thy) = - thy - |> Domain_Theorems.comp_theorems (comp_dbind, eqs) - dbinds take_info constr_infos; + val (take_rews, thy) = + Domain_Theorems.comp_theorems comp_dbind + dbinds take_info constr_infos thy; in - theorems_thy + thy end; fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = diff -r 876689e6bbdf -r 8f8f18a88685 src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Sat Oct 16 15:26:30 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,239 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_library.ML - Author: David von Oheimb - -Library for domain command. -*) - - -(* infix syntax *) - -infixr 5 -->; -infixr 6 ->>; -infixr 0 ===>; -infixr 0 ==>; -infix 0 ==; -infix 1 ===; -infix 1 ~=; - -infix 9 ` ; -infix 9 `% ; -infix 9 `%%; - - -(* ----- specific support for domain ---------------------------------------- *) - -signature DOMAIN_LIBRARY = -sig - val first : 'a * 'b * 'c -> 'a - val second : 'a * 'b * 'c -> 'b - val third : 'a * 'b * 'c -> 'c - val upd_second : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c - val upd_third : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd - val mapn : (int -> 'a -> 'b) -> int -> 'a list -> 'b list - val atomize : Proof.context -> thm -> thm list - - val Imposs : string -> 'a; - val cpo_type : theory -> typ -> bool; - val pcpo_type : theory -> typ -> bool; - val string_of_typ : theory -> typ -> string; - - (* Creating HOLCF types *) - val mk_ssumT : typ * typ -> typ; - val mk_sprodT : typ * typ -> typ; - val mk_uT : typ -> typ; - val oneT : typ; - val pcpoS : sort; - - (* Creating HOLCF terms *) - val %: : string -> term; - val %%: : string -> term; - val ` : term * term -> term; - val `% : term * string -> term; - val UU : term; - val ID : term; - val list_ccomb : term * term list -> term; - val con_app2 : string -> ('a -> term) -> 'a list -> term; - val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a - val proj : term -> 'a list -> int -> term; - - (* Creating propositions *) - val mk_conj : term * term -> term; - val mk_disj : term * term -> term; - val mk_imp : term * term -> term; - val mk_lam : string * term -> term; - val mk_all : string * term -> term; - val mk_ex : string * term -> term; - val mk_constrainall : string * typ * term -> term; - val === : term * term -> term; - val defined : term -> term; - val mk_adm : term -> term; - val lift : ('a -> term) -> 'a list * term -> term; - val lift_defined : ('a -> term) -> 'a list * term -> term; - - (* Creating meta-propositions *) - val mk_trp : term -> term; (* HOLogic.mk_Trueprop *) - val == : term * term -> term; - val ===> : term * term -> term; - val mk_All : string * term -> term; - - (* Domain specifications *) - eqtype arg; - type cons = string * arg list; - type eq = (string * typ list) * cons list; - val mk_arg : (bool * Datatype.dtyp) * string -> arg; - val is_lazy : arg -> bool; - val rec_of : arg -> int; - val dtyp_of : arg -> Datatype.dtyp; - val vname : arg -> string; - val upd_vname : (string -> string) -> arg -> arg; - val is_rec : arg -> bool; - val is_nonlazy_rec : arg -> bool; - val nonlazy : arg list -> string list; - val nonlazy_rec : arg list -> string list; - val %# : arg -> term; - val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) - val idx_name : 'a list -> string -> int -> string; - val con_app : string -> arg list -> term; -end; - -structure Domain_Library :> DOMAIN_LIBRARY = -struct - -fun first (x,_,_) = x; -fun second (_,x,_) = x; -fun third (_,_,x) = x; - -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -fun mapn f n [] = [] - | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; - -fun foldr'' f (l,f2) = - let fun itr [] = raise Fail "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) - in itr l end; - -fun atomize ctxt thm = - let - val r_inst = read_instantiate ctxt; - fun at thm = - case concl_of thm of - _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) - | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) - | _ => [thm]; - in map zero_var_indexes (at thm) end; - -exception Impossible of string; -fun Imposs msg = raise Impossible ("Domain:"^msg); - -fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); -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 ----- *) - -type arg = - (bool * Datatype.dtyp) * (* (lazy, recursive element) *) - string; (* argument name *) - -type cons = - string * (* operator name of constr *) - arg list; (* argument list *) - -type eq = - (string * (* name of abstracted type *) - typ list) * (* arguments of abstracted type *) - cons list; (* represented type, as a constructor list *) - -val mk_arg = I; - -fun rec_of ((_,dtyp),_) = - case dtyp of Datatype_Aux.DtRec i => i | _ => ~1; -(* FIXME: what about indirect recursion? *) - -fun is_lazy arg = fst (fst arg); -fun dtyp_of arg = snd (fst arg); -val vname = snd; -val upd_vname = apsnd; -fun is_rec arg = rec_of arg >=0; -fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); -fun nonlazy args = map vname (filter_out is_lazy args); -fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); - - -(* ----- support for type and mixfix expressions ----- *) - -fun mk_uT T = Type(@{type_name "u"}, [T]); -fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]); -fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]); -val oneT = @{typ one}; - -(* ----- support for term expressions ----- *) - -fun %: s = Free(s,dummyT); -fun %# arg = %:(vname arg); -fun %%: s = Const(s,dummyT); - -local open HOLogic in -val mk_trp = mk_Trueprop; -fun mk_conj (S,T) = conj $ S $ T; -fun mk_disj (S,T) = disj $ S $ T; -fun mk_imp (S,T) = imp $ S $ T; -fun mk_lam (x,T) = Abs(x,dummyT,T); -fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); -fun mk_ex (x,P) = mk_exists (x,dummyT,P); -fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type.constraint (typ --> boolT) (mk_lam(x,P))); -end - -fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) - -infixr 0 ===>; fun S ===> T = %%: "==>" $ S $ T; -infix 0 ==; fun S == T = %%: "==" $ S $ T; -infix 1 ===; fun S === T = %%: @{const_name HOL.eq} $ S $ T; -infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); - -infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x; -infix 9 `% ; fun f`% s = f` %: s; -infix 9 `%%; fun f`%%s = f` %%:s; - -fun mk_adm t = %%: @{const_name adm} $ t; -val ID = %%: @{const_name ID}; -fun mk_strictify t = %%: @{const_name strictify}`t; -fun mk_ssplit t = %%: @{const_name ssplit}`t; -fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; -fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; - -val pcpoS = @{sort pcpo}; - -val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) -fun con_app2 con f args = list_ccomb(%%:con,map f args); -fun con_app con = con_app2 con %#; -fun prj _ _ x ( _::[]) _ = x - | prj _ _ _ [] _ = raise Fail "Domain_Library.prj: empty list" - | prj f1 _ x (_::y::ys) 0 = f1 x y - | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); -fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x; -fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); - -val UU = %%: @{const_name UU}; -fun defined t = t ~= UU; -fun cpair (t,u) = %%: @{const_name Pair} $ t $ u; -fun spair (t,u) = %%: @{const_name spair}`t`u; -fun lift_defined f = lift (fn x => defined (f x)); -fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1); - -fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = - (case cont_eta_contract body of - body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f - else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') - | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) - | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t - | cont_eta_contract t = t; - -fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); - -end; (* struct *) diff -r 876689e6bbdf -r 8f8f18a88685 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Oct 16 15:26:30 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Oct 16 16:22:42 2010 -0700 @@ -10,8 +10,7 @@ signature DOMAIN_THEOREMS = sig val comp_theorems : - binding * Domain_Library.eq list -> - binding list -> + binding -> binding list -> Domain_Take_Proofs.take_induct_info -> Domain_Constructors.constr_info list -> theory -> thm list * theory @@ -154,7 +153,7 @@ (take_rews : thm list) (thy : theory) = let - val comp_dname = Sign.full_name thy comp_dbind; + val comp_dname = Binding.name_of comp_dbind; val iso_infos = map #iso_info constr_infos; val exhausts = map #exhaust constr_infos; @@ -281,15 +280,15 @@ val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; fun ind_rule (dname, rule) = - ((Binding.empty, [rule]), + ((Binding.empty, rule), [Rule_Cases.case_names case_ns, Induct.induct_type dname]); in thy - |> snd o Global_Theory.add_thmss [ - ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []), - ((Binding.qualified true "induct" comp_dbind, [ind] ), [])] - |> (snd o Global_Theory.add_thmss (map ind_rule (dnames ~~ inducts))) + |> snd o Global_Theory.add_thms [ + ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), + ((Binding.qualified true "induct" comp_dbind, ind ), [])] + |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) end; (* prove_induction *) (******************************************************************************) @@ -303,8 +302,6 @@ (take_rews : thm list list) (thy : theory) : theory = let - val comp_dname = Sign.full_name thy comp_dbind; - val iso_infos = map #iso_info constr_infos; val newTs = map #absT iso_infos; @@ -423,18 +420,19 @@ (******************************************************************************) fun comp_theorems - (comp_dbind : binding, eqs : Domain_Library.eq list) + (comp_dbind : binding) (dbinds : binding list) (take_info : Domain_Take_Proofs.take_induct_info) (constr_infos : Domain_Constructors.constr_info list) (thy : theory) = let -val dnames = map (fst o fst) eqs; -val comp_dname = Sign.full_name thy comp_dbind; +val comp_dname = Binding.name_of comp_dbind; (* Test for emptiness *) +(* FIXME: reimplement emptiness test local open Domain_Library; + val dnames = map (fst o fst) eqs; val conss = map snd eqs; fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso @@ -450,16 +448,19 @@ val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; val is_emptys = map warn n__eqs; end; +*) (* Test for indirect recursion *) local - open Domain_Library; - fun indirect_arg arg = - rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg); + val newTs = map (#absT o #iso_info) constr_infos; + fun indirect_typ (Type (_, Ts)) = + exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts + | indirect_typ _ = false; + fun indirect_arg (_, T) = indirect_typ T; fun indirect_con (_, args) = exists indirect_arg args; - fun indirect_eq (_, cons) = exists indirect_con cons; + fun indirect_eq cons = exists indirect_con cons; in - val is_indirect = exists indirect_eq eqs; + val is_indirect = exists indirect_eq (map #con_specs constr_infos); val _ = if is_indirect then message "Indirect recursion detected, skipping proofs of (co)induction rules" diff -r 876689e6bbdf -r 8f8f18a88685 src/HOLCF/ex/Pattern_Match.thy --- a/src/HOLCF/ex/Pattern_Match.thy Sat Oct 16 15:26:30 2010 -0700 +++ b/src/HOLCF/ex/Pattern_Match.thy Sat Oct 16 16:22:42 2010 -0700 @@ -359,6 +359,9 @@ ML {* local open HOLCF_Library in +infixr 6 ->>; +infix 9 ` ; + val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};