# HG changeset patch # User huffman # Date 1243023539 25200 # Node ID 689aa7da48cc16f72aeb64ffe766f2e0c7772cd2 # Parent 9434cd5ef24a22101e1f9785e9a269167d6a8bb8 define copy functions using combinators; add checking for failed proofs of induction rules diff -r 9434cd5ef24a -r 689aa7da48cc src/HOLCF/Tools/domain/domain_axioms.ML --- 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 - *) diff -r 9434cd5ef24a -r 689aa7da48cc src/HOLCF/Tools/domain/domain_theorems.ML --- 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 *) diff -r 9434cd5ef24a -r 689aa7da48cc src/HOLCF/ex/Domain_ex.thy --- 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 \ 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