# HG changeset patch # User huffman # Date 1243023736 25200 # Node ID c4c1692d4eee7a109d100c177a6f78bc74236840 # Parent 689aa7da48cc16f72aeb64ffe766f2e0c7772cd2# Parent df6945ac4193208197a69cc29ae36755c387e4f2 merged diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/Domain.thy Fri May 22 13:22:16 2009 -0700 @@ -202,6 +202,65 @@ lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 +subsection {* Combinators for building copy functions *} + +definition + cfun_fun :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" +where + "cfun_fun = (\ f g p. g oo p oo f)" + +definition + ssum_fun :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" +where + "ssum_fun = (\ f g. sscase\(sinl oo f)\(sinr oo g))" + +definition + sprod_fun :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" +where + "sprod_fun = (\ f g. ssplit\(\ x y. (:f\x, g\y:)))" + +definition + cprod_fun :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" +where + "cprod_fun = (\ f g. csplit\(\ x y. x, g\y>))" + +definition + u_fun :: "('a \ 'b) \ 'a u \ 'b u" +where + "u_fun = (\ f. fup\(up oo f))" + +lemma cfun_fun_strict: "b\\ = \ \ cfun_fun\a\b\\ = \" +unfolding cfun_fun_def expand_cfun_eq by simp + +lemma ssum_fun_strict: "ssum_fun\a\b\\ = \" +unfolding ssum_fun_def by simp + +lemma sprod_fun_strict: "sprod_fun\a\b\\ = \" +unfolding sprod_fun_def by simp + +lemma u_fun_strict: "u_fun\a\\ = \" +unfolding u_fun_def by simp + +lemma ssum_fun_sinl: "x \ \ \ ssum_fun\f\g\(sinl\x) = sinl\(f\x)" +by (simp add: ssum_fun_def) + +lemma ssum_fun_sinr: "x \ \ \ ssum_fun\f\g\(sinr\x) = sinr\(g\x)" +by (simp add: ssum_fun_def) + +lemma sprod_fun_spair: + "x \ \ \ y \ \ \ sprod_fun\f\g\(:x, y:) = (:f\x, g\y:)" +by (simp add: sprod_fun_def) + +lemma u_fun_up: "u_fun\a\(up\x) = up\(a\x)" +by (simp add: u_fun_def) + +lemmas domain_fun_stricts = + ssum_fun_strict sprod_fun_strict u_fun_strict + +lemmas domain_fun_simps = + ssum_fun_sinl ssum_fun_sinr sprod_fun_spair u_fun_up + + subsection {* Installing the domain package *} lemmas con_strict_rules = diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Fri May 22 13:22:16 2009 -0700 @@ -6,124 +6,147 @@ signature DOMAIN_AXIOMS = sig - val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory + val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term + + val calc_axioms : + string -> Domain_Library.eq list -> int -> Domain_Library.eq -> + string * (string * term) list * (string * term) list + + val add_axioms : + bstring -> Domain_Library.eq list -> theory -> theory end; structure Domain_Axioms :> DOMAIN_AXIOMS = struct -local +open Domain_Library; -open Domain_Library; infixr 0 ===>;infixr 0 ==>;infix 0 == ; infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; -fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= -let - -(* ----- axioms and definitions concerning the isomorphism ------------------ *) +(* FIXME: use theory data for this *) +val copy_tab : string Symtab.table = + Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}), + (@{type_name "++"}, @{const_name "ssum_fun"}), + (@{type_name "**"}, @{const_name "sprod_fun"}), + (@{type_name "*"}, @{const_name "cprod_fun"}), + (@{type_name "u"}, @{const_name "u_fun"})]; - val dc_abs = %%:(dname^"_abs"); - val dc_rep = %%:(dname^"_rep"); - val x_name'= "x"; - val x_name = idx_name eqs x_name' (n+1); - val dnam = Long_Name.base_name dname; +fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID +and copy r (DatatypeAux.DtRec i) = r i + | copy r (DatatypeAux.DtTFree a) = ID + | copy r (DatatypeAux.DtType (c, ds)) = + case Symtab.lookup copy_tab c of + SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) + | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); - val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); - val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); +fun calc_axioms + (comp_dname : string) + (eqs : eq list) + (n : int) + (eqn as ((dname,_),cons) : eq) + : string * (string * term) list * (string * term) list = + let + + (* ----- axioms and definitions concerning the isomorphism ------------------ *) - val when_def = ("when_def",%%:(dname^"_when") == - List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => - Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); - - val copy_def = let - fun idxs z x arg = if is_rec arg - then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x) - else Bound(z-x); - fun one_con (con,args) = - List.foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args; - in ("copy_def", %%:(dname^"_copy") == - /\ "f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end; + val dc_abs = %%:(dname^"_abs"); + val dc_rep = %%:(dname^"_rep"); + val x_name'= "x"; + val x_name = idx_name eqs x_name' (n+1); + val dnam = Long_Name.base_name dname; + + val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); + val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); -(* -- definitions concerning the constructors, discriminators and selectors - *) + val when_def = ("when_def",%%:(dname^"_when") == + List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => + Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); + + val copy_def = + let fun r i = cproj (Bound 0) eqs i; + in ("copy_def", %%:(dname^"_copy") == + /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; - fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); - fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); - fun inj y 1 _ = y - | inj y _ 0 = mk_sinl y - | inj y i j = mk_sinr (inj y (i-1) (j-1)); - in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; - - val con_defs = mapn (fn n => fn (con,args) => - (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; - - val dis_defs = let - fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (List.foldr /\# + (* -- definitions concerning the constructors, discriminators and selectors - *) + + fun con_def m n (_,args) = let + fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); + fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); + fun inj y 1 _ = y + | inj y _ 0 = mk_sinl y + | inj y i j = mk_sinr (inj y (i-1) (j-1)); + in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; + + val con_defs = mapn (fn n => fn (con,args) => + (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; + + val dis_defs = let + fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => (List.foldr /\# (if con'=con then TT else FF) args)) cons)) in map ddef 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 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 - fun pdef (con,args) = - let - val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - val xs = map (bound_arg args) args; - val r = Bound (length args); - val rhs = case args of [] => mk_return HOLogic.unit - | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; - in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == - list_ccomb(%%:(dname^"_when"), map one_con cons)) - end - in map pdef cons end; + val pat_defs = + let + fun pdef (con,args) = + let + val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; + val xs = map (bound_arg args) args; + val r = Bound (length args); + val rhs = case args of [] => mk_return HOLogic.unit + | _ => mk_ctuple_pat ps ` mk_ctuple xs; + fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; + in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == + list_ccomb(%%:(dname^"_when"), map one_con cons)) + end + in map pdef cons end; - val sel_defs = let - fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => if con'<>con then UU else - List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); + val sel_defs = let + fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => if con'<>con then UU else + List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; -(* ----- axiom and definitions concerning induction ------------------------- *) + (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj - (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); - val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, - mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); + val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n + `%x_name === %:x_name)); + val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj + (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); + val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, + mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); -in (dnam, - [abs_iso_ax, rep_iso_ax, reach_ax], - [when_def, copy_def] @ - con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ - [take_def, finite_def]) -end; (* let (calc_axioms) *) + in (dnam, + [abs_iso_ax, rep_iso_ax, reach_ax], + [when_def, copy_def] @ + con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ + [take_def, finite_def]) + end; (* let (calc_axioms) *) (* legacy type inference *) fun legacy_infer_term thy t = - singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); + singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); @@ -137,62 +160,70 @@ fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; fun add_matchers (((dname,_),cons) : eq) thy = - let - val con_names = map fst cons; - val mat_names = map mat_name con_names; - fun qualify n = Sign.full_name thy (Binding.name n); - val ms = map qualify con_names ~~ map qualify mat_names; - in FixrecPackage.add_matchers ms thy end; - -in (* local *) + let + val con_names = map fst cons; + val mat_names = map mat_name con_names; + fun qualify n = Sign.full_name thy (Binding.name n); + val ms = map qualify con_names ~~ map qualify mat_names; + in FixrecPackage.add_matchers ms thy end; -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"; - fun copy_app dname = %%:(dname^"_copy")`Bound 0; - val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\ "f"(mk_ctuple (map copy_app dnames))); - val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", +fun add_axioms comp_dnam (eqs : eq list) thy' = let - fun one_con (con,args) = let - val nonrec_args = filter_out is_rec args; - val rec_args = List.filter is_rec args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = length nonrec_args + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = List.foldr mk_conj (mk_conj( - Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) - (mapn rel_app 1 rec_args); - in List.foldr mk_ex (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns end; - fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( - proj (Bound 2) eqs n $ Bound 1 $ Bound 0, - foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) - ::map one_con cons)))); - in foldr1 mk_conj (mapn one_comp 0 eqs)end )); - fun add_one (thy,(dnam,axs,dfs)) = thy - |> Sign.add_path dnam - |> add_defs_infer dfs - |> add_axioms_infer axs - |> Sign.parent_path; - val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); -in thy |> Sign.add_path comp_dnam - |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) - |> Sign.parent_path - |> fold add_matchers eqs -end; (* let (add_axioms) *) + val comp_dname = Sign.full_bname thy' comp_dnam; + val dnames = map (fst o fst) eqs; + val x_name = idx_name dnames "x"; + fun copy_app dname = %%:(dname^"_copy")`Bound 0; + val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == + /\ "f"(mk_ctuple (map copy_app dnames))); -end; (* local *) + fun one_con (con,args) = let + val nonrec_args = filter_out is_rec args; + val rec_args = List.filter is_rec args; + val recs_cnt = length rec_args; + val allargs = nonrec_args @ rec_args + @ map (upd_vname (fn s=> s^"'")) rec_args; + val allvns = map vname allargs; + fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; + val vns1 = map (vname_arg "" ) args; + val vns2 = map (vname_arg "'") args; + val allargs_cnt = length nonrec_args + 2*recs_cnt; + val rec_idxs = (recs_cnt-1) downto 0; + val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) + (allargs~~((allargs_cnt-1) downto 0))); + fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ + Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); + val capps = + List.foldr mk_conj + (mk_conj( + Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) + (mapn rel_app 1 rec_args); + in List.foldr mk_ex + (Library.foldr mk_conj + (map (defined o Bound) nonlazy_idxs,capps)) allvns + end; + fun one_comp n (_,cons) = + mk_all(x_name(n+1), + mk_all(x_name(n+1)^"'", + mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0, + foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) + ::map one_con cons)))); + val bisim_def = + ("bisim_def", + %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); + + fun add_one (thy,(dnam,axs,dfs)) = + thy |> Sign.add_path dnam + |> add_defs_infer dfs + |> add_axioms_infer axs + |> Sign.parent_path; + + val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); + + in thy |> Sign.add_path comp_dnam + |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) + |> Sign.parent_path + |> fold add_matchers eqs + end; (* let (add_axioms) *) + end; (* struct *) diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Fri May 22 13:22:16 2009 -0700 @@ -122,8 +122,7 @@ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); 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, + ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp), Option.map Binding.name_of sel,vn)) (args,(mk_var_names(map (typid o third) args))) diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_library.ML Fri May 22 13:22:16 2009 -0700 @@ -78,6 +78,8 @@ val UU : term; val TT : term; val FF : term; + val ID : term; + val oo : term * term -> term; val mk_up : term -> term; val mk_sinl : term -> term; val mk_sinr : term -> term; @@ -89,7 +91,9 @@ val mk_return : term -> term; val cproj : term -> 'a list -> int -> term; val list_ccomb : term * term list -> term; +(* val con_app : string -> ('a * 'b * string) list -> term; +*) val con_app2 : string -> ('a -> term) -> 'a list -> term; val proj : term -> 'a list -> int -> term; val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a; @@ -123,11 +127,13 @@ val mk_All : string * term -> term; (* Domain specifications *) - type arg = (bool * int * DatatypeAux.dtyp) * string option * string; + eqtype arg; type cons = string * arg list; type eq = (string * typ list) * cons list; + val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg; val is_lazy : arg -> bool; val rec_of : arg -> int; + val dtyp_of : arg -> DatatypeAux.dtyp; val sel_of : arg -> string option; val vname : arg -> string; val upd_vname : (string -> string) -> arg -> arg; @@ -142,6 +148,9 @@ val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) val idx_name : 'a list -> string -> int -> string; val app_rec_arg : (int -> term) -> arg -> term; + val con_app : string -> arg list -> term; + val dtyp_of_eq : eq -> DatatypeAux.dtyp; + (* Name mangling *) val strip_esc : string -> string; @@ -198,7 +207,7 @@ (* ----- constructor list handling ----- *) type arg = - (bool * int * DatatypeAux.dtyp) * (* (lazy,recursive element or ~1) *) + (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *) string option * (* selector name *) string; (* argument name *) @@ -211,8 +220,14 @@ typ list) * (* arguments of abstracted type *) cons list; (* represented type, as a constructor list *) -fun rec_of arg = second (first arg); -fun is_lazy arg = first (first arg); +val mk_arg = I; + +fun rec_of ((_,dtyp),_,_) = + case dtyp of DatatypeAux.DtRec i => i | _ => ~1; +(* FIXME: what about indirect recursion? *) + +fun is_lazy arg = fst (first arg); +fun dtyp_of arg = snd (first arg); val sel_of = second; val vname = third; val upd_vname = upd_third; @@ -221,6 +236,25 @@ fun nonlazy args = map vname (filter_out is_lazy args); fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); + +(* ----- combinators for making dtyps ----- *) + +fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]); +fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]); +fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]); +fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]); +val unitD = DatatypeAux.DtType(@{type_name "unit"}, []); +val boolD = DatatypeAux.DtType(@{type_name "bool"}, []); +val oneD = mk_liftD unitD; +val trD = mk_liftD boolD; +fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds; +fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds; + +fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D; +fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args); +fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons); + + (* ----- support for type and mixfix expressions ----- *) fun mk_uT T = Type(@{type_name "u"}, [T]); diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Fri May 22 13:22:16 2009 -0700 @@ -6,163 +6,174 @@ signature DOMAIN_SYNTAX = sig - val add_syntax: string -> ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory + val calc_syntax: + typ -> + (string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list -> + (binding * typ * mixfix) list * ast Syntax.trrule list + + 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 +struct open Domain_Library; infixr 5 -->; infixr 6 ->>; -fun calc_syntax dtypeprod ((dname, typevars), - (cons': (binding * (bool * binding option * typ) list * mixfix) list)) : ((binding * typ * mixfix) list * ast Syntax.trrule list) = -let -(* ----- constants concerning the isomorphism ------------------------------- *) + +fun calc_syntax + (dtypeprod : typ) + ((dname : string, typevars : typ 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,_) = 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); -in - val dtype = Type(dname,typevars); - val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Long_Name.base_name dname; - 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; + local + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + 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); + in + val dtype = Type(dname,typevars); + val dtype2 = foldr1 mk_ssumT (map prod cons'); + val dnam = Long_Name.base_name dname; + 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 --- *) + (* ----- constants concerning constructors, discriminators, and selectors --- *) -local - val escape = let - fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs - else c::esc cs - | esc [] = [] - in implode o esc o Symbol.explode end; - 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 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,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 (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); + local + val escape = let + fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs + else c::esc cs + | esc [] = [] + in implode o esc o Symbol.explode end; + 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 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,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 (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); -in - val consts_con = map con cons'; - val consts_dis = map dis cons'; - val consts_mat = map mat cons'; - val consts_pat = map pat cons'; - val consts_sel = List.concat(map sel cons'); -end; + in + val consts_con = map con cons'; + val consts_dis = map dis cons'; + val consts_mat = map mat cons'; + val consts_pat = map pat cons'; + val consts_sel = List.concat(map sel cons'); + end; -(* ----- constants concerning induction ------------------------------------- *) + (* ----- constants concerning induction ------------------------------------- *) - val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); - val const_finite = (dbind "_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 --------------------------------------------------- *) + (* ----- case translation --------------------------------------------------- *) -local open Syntax in - local - 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)); - fun argvars n args = mapn (argvar n) 1 args; - fun app s (l,r) = mk_appl (Constant s) [l,r]; - val cabs = app "_cabs"; - val capp = app "Rep_CFun"; - 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"); + local open Syntax in + local + 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)); + fun argvars n args = mapn (argvar n) 1 args; + fun app s (l,r) = mk_appl (Constant s) [l,r]; + val cabs = app "_cabs"; + val capp = app "Rep_CFun"; + 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"]; - fun app_pat x = mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" - | args_list xs = foldr1 (app "_args") xs; - in - val case_trans = ParsePrintRule - (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), - capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); - - val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule - (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,args,mx) => - let - val cname = c_ast con mx; - 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; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; - in - [ParseRule (app_pat (Library.foldl capp (cname, xs)), - mk_appl pname (map app_pat xs)), - ParseRule (app_var (Library.foldl capp (cname, xs)), - app_var (args_list xs)), - PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] - end) cons'); - end; -end; + fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; + fun app_pat x = mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "_noargs" + | args_list xs = foldr1 (app "_args") xs; + in + val case_trans = + ParsePrintRule + (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), + capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); -in ([const_rep, const_abs, const_when, const_copy] @ - consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ - [const_take, const_finite], - (case_trans::(abscon_trans @ Case_trans))) -end; (* let *) + fun one_abscon_trans n (con,mx,args) = + ParsePrintRule + (cabs (con1 n (con,mx,args), expvar n), + Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); + val abscon_trans = mapn one_abscon_trans 1 cons'; + + fun one_case_trans (con,args,mx) = + let + val cname = c_ast con mx; + 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; + val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + in + [ParseRule (app_pat (Library.foldl capp (cname, xs)), + mk_appl pname (map app_pat xs)), + ParseRule (app_var (Library.foldl capp (cname, xs)), + app_var (args_list xs)), + PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (mk_appl pname ps, args_list vs))] + end; + val Case_trans = List.concat (map one_case_trans cons'); + end; + end; + + in ([const_rep, const_abs, const_when, const_copy] @ + consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ + [const_take, const_finite], + (case_trans::(abscon_trans @ Case_trans))) + end; (* let *) (* ----- putting all the syntax stuff together ------------------------------ *) -in (* local *) +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 = (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]) + |> Sign.add_trrules_i (List.concat(map snd ctt)) + end; (* let *) -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 = (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]) - |> Sign.add_trrules_i (List.concat(map snd ctt)) -end; (* let *) - -end; (* local *) end; (* struct *) diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 22 13:22:16 2009 -0700 @@ -577,21 +577,28 @@ val copy_strict = let + val _ = trace " Proving copy_strict..."; val goal = mk_trp (strict (dc_copy `% "f")); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1]; + val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts}; + val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; in pg [ax_copy_def] goal (K tacs) end; local fun copy_app (con, args) = let val lhs = dc_copy`%"f"`(con_app con args); - val rhs = con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args; + fun one_rhs arg = + if DatatypeAux.is_rec_type (dtyp_of arg) + then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg) + else (%# arg); + val rhs = con_app2 con one_rhs args; val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; - val stricts = abs_strict::when_strict::con_stricts; + val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts}; fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1]; - in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; + val rules = [ax_abs_iso] @ @{thms domain_fun_simps}; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; + in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; in val _ = trace " Proving copy_apps..."; val copy_apps = map copy_app cons; @@ -706,8 +713,12 @@ fun mk_eqn dn (con, args) = let fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; + fun one_rhs arg = + if DatatypeAux.is_rec_type (dtyp_of arg) + then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg) + else (%# arg); val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); - val rhs = con_app2 con (app_rec_arg mk_take) args; + val rhs = con_app2 con one_rhs args; in Library.foldr mk_all (map vname args, lhs === rhs) end; fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); @@ -812,7 +823,9 @@ in tacs1 @ maps cases_tacs (conss ~~ cases) end; - in pg'' thy [] goal tacf end; + in pg'' thy [] goal tacf + handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI) + end; val _ = trace " Proving take_lemmas..."; val take_lemmas = @@ -842,6 +855,7 @@ val _ = trace " Proving finites, ind..."; val (finites, ind) = + ( if is_finite then (* finite case *) let @@ -860,8 +874,10 @@ asm_simp_tac take_ss 1, atac 1]; in pg [] goal (K tacs) end; + val _ = trace " Proving finite_lemmas1a"; val finite_lemmas1a = map dname_lemma dnames; + val _ = trace " Proving finite_lemma1b"; val finite_lemma1b = let fun mk_eqn n ((dn, args), _) = @@ -908,7 +924,9 @@ fast_tac HOL_cs 1]; in pg axs_finite_def goal tacs end; + val _ = trace " Proving finites"; val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b); + val _ = trace " Proving ind"; val ind = let fun concf n dn = %:(P_name n) $ %:(x_name n); @@ -952,7 +970,14 @@ val ind = (pg'' thy [] goal tacf handle ERROR _ => (warning "Cannot prove infinite induction rule"; refl)); - in (finites, ind) end; + in (finites, ind) end + ) + handle THM _ => + (warning "Induction proofs failed (THM raised)."; ([], TrueI)) + | ERROR _ => + (warning "Induction proofs failed (ERROR raised)."; ([], TrueI)); + + end; (* local *) (* ----- theorem concerning coinduction ------------------------------------- *) @@ -1010,6 +1035,7 @@ val inducts = ProjectRule.projections (ProofContext.init thy) ind; fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); +val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); in thy |> Sign.add_path comp_dnam |> snd o PureThy.add_thmss [ @@ -1019,7 +1045,8 @@ ((Binding.name "finite_ind" , [finite_ind]), []), ((Binding.name "ind" , [ind] ), []), ((Binding.name "coind" , [coind] ), [])] - |> snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)) + |> (if induct_failed then I + else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) |> Sign.parent_path |> pair take_rews end; (* let *) end; (* local *) diff -r df6945ac4193 -r c4c1692d4eee src/HOLCF/ex/Domain_ex.thy --- a/src/HOLCF/ex/Domain_ex.thy Thu May 21 19:15:22 2009 +0200 +++ b/src/HOLCF/ex/Domain_ex.thy Fri May 22 13:22:16 2009 -0700 @@ -53,13 +53,13 @@ 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. + cannot prove the induction rules. A fix is planned for the next + release. *} -domain 'a d7 = d7a "'a d7 \ int lift" | d7b "'a \ 'a d7" | d7c "'a d7 \ 'a" +domain 'a d7 = d7a "'a d7 \ int lift" | d7b "'a \ 'a d7" | d7c (lazy "'a d7 \ 'a") -thm d7.ind -- "note the lack of inductive hypotheses" +thm d7.ind -- "currently replaced with dummy theorem" text {* Indirect recursion using previously-defined datatypes is currently