--- 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 \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
+where
+ "cfun_fun = (\<Lambda> f g p. g oo p oo f)"
+
+definition
+ ssum_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
+where
+ "ssum_fun = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
+
+definition
+ sprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
+where
+ "sprod_fun = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
+
+definition
+ cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
+where
+ "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. <f\<cdot>x, g\<cdot>y>))"
+
+definition
+ u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
+where
+ "u_fun = (\<Lambda> f. fup\<cdot>(up oo f))"
+
+lemma cfun_fun_strict: "b\<cdot>\<bottom> = \<bottom> \<Longrightarrow> cfun_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
+unfolding cfun_fun_def expand_cfun_eq by simp
+
+lemma ssum_fun_strict: "ssum_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
+unfolding ssum_fun_def by simp
+
+lemma sprod_fun_strict: "sprod_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
+unfolding sprod_fun_def by simp
+
+lemma u_fun_strict: "u_fun\<cdot>a\<cdot>\<bottom> = \<bottom>"
+unfolding u_fun_def by simp
+
+lemma ssum_fun_sinl: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+by (simp add: ssum_fun_def)
+
+lemma ssum_fun_sinr: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+by (simp add: ssum_fun_def)
+
+lemma sprod_fun_spair:
+ "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_fun\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+by (simp add: sprod_fun_def)
+
+lemma u_fun_up: "u_fun\<cdot>a\<cdot>(up\<cdot>x) = up\<cdot>(a\<cdot>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 =
--- 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 *)
--- 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)))
--- 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]);
--- 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 *)
--- 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 *)
--- 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 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c "'a d7 \<rightarrow> 'a"
+domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> '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