define copy functions using combinators; add checking for failed proofs of induction rules
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Fri May 22 10:36:38 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Fri May 22 13:18:59 2009 -0700
@@ -6,6 +6,8 @@
signature DOMAIN_AXIOMS =
sig
+ 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
@@ -24,11 +26,27 @@
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
+(* 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"})];
+
+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);
+
fun calc_axioms
(comp_dname : string)
(eqs : eq list)
(n : int)
- (((dname,_),cons) : eq)
+ (eqn as ((dname,_),cons) : eq)
: string * (string * term) list * (string * term) list =
let
@@ -47,14 +65,10 @@
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 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;
(* -- definitions concerning the constructors, discriminators and selectors - *)
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 22 10:36:38 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 22 13:18:59 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 Fri May 22 10:36:38 2009 -0700
+++ b/src/HOLCF/ex/Domain_ex.thy Fri May 22 13:18:59 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