domain package no longer generates copy functions; all proofs use take functions instead
--- a/src/HOLCF/Domain.thy Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Domain.thy Tue Mar 02 00:34:26 2010 -0800
@@ -250,6 +250,27 @@
lemmas sel_defined_iff_rules =
cfcomp2 sfst_defined_iff ssnd_defined_iff
+lemmas take_con_rules =
+ ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
+ sprod_map_spair' sprod_map_strict u_map_up u_map_strict
+
+lemma lub_ID_take_lemma:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
+proof -
+ have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
+ using assms(3) by simp
+ then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
+ using assms(1) by (simp add: lub_distribs)
+ then show "x = y"
+ using assms(2) by simp
+qed
+
+lemma lub_ID_reach:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ shows "(\<Squnion>n. t n\<cdot>x) = x"
+using assms by (simp add: lub_distribs)
+
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
use "Tools/Domain/domain_library.ML"
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 02 00:34:26 2010 -0800
@@ -902,15 +902,10 @@
shows "s1<<s2"
apply (rule_tac t="s1" in seq.reach [THEN subst])
apply (rule_tac t="s2" in seq.reach [THEN subst])
-apply (rule fix_def2 [THEN ssubst])
-apply (subst contlub_cfun_fun)
-apply (rule chain_iterate)
-apply (subst contlub_cfun_fun)
-apply (rule chain_iterate)
apply (rule lub_mono)
-apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
-apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
-apply (rule prems [unfolded seq.take_def])
+apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule assms)
done
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 00:34:26 2010 -0800
@@ -16,6 +16,8 @@
val add_axioms :
bool ->
+ ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list ->
bstring -> Domain_Library.eq list -> theory -> theory
end;
@@ -67,22 +69,8 @@
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'));
- val copy_def =
- let fun r i = proj (Bound 0) eqs i;
- in
- ("copy_def", %%:(dname^"_copy") == /\ "f"
- (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
- end;
-
(* ----- axiom and definitions concerning induction ------------------------- *)
- val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
- `%x_name === %:x_name));
- val take_def =
- ("take_def",
- %%:(dname^"_take") ==
- mk_lam("n",proj
- (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
val finite_def =
("finite_def",
%%:(dname^"_finite") ==
@@ -90,9 +78,8 @@
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
in (dnam,
- (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
- (if definitional then [] else [copy_def]) @
- [take_def, finite_def])
+ (if definitional then [] else [abs_iso_ax, rep_iso_ax]),
+ [finite_def])
end; (* let (calc_axioms) *)
@@ -112,14 +99,11 @@
fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-fun add_axioms definitional comp_dnam (eqs : eq list) thy' =
+fun add_axioms definitional eqs' 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)));
fun one_con (con, _, args) =
let
@@ -165,20 +149,74 @@
fun add_one (dnam, axs, dfs) =
Sign.add_path dnam
- #> add_defs_infer dfs
#> add_axioms_infer axs
#> Sign.parent_path;
val map_tab = Domain_Isomorphism.get_map_tab thy';
+ val axs = mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs;
+ val thy = thy' |> fold add_one axs;
- val thy = thy'
- |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
+ fun get_iso_info ((dname, tyvars), cons') =
+ let
+ 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);
+ val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso");
+ val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso");
+ val lhsT = Type(dname,tyvars);
+ val rhsT = foldr1 mk_ssumT (map prod cons');
+ val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
+ val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
+ in
+ {
+ absT = lhsT,
+ repT = rhsT,
+ abs_const = abs_const,
+ rep_const = rep_const,
+ abs_inverse = ax_abs_iso,
+ rep_inverse = ax_rep_iso
+ }
+ end;
+ val dom_binds = map (Binding.name o Long_Name.base_name) dnames;
+ val thy =
+ if definitional then thy
+ else snd (Domain_Isomorphism.define_take_functions
+ (dom_binds ~~ map get_iso_info eqs') thy);
+
+ fun add_one' (dnam, axs, dfs) =
+ Sign.add_path dnam
+ #> add_defs_infer dfs
+ #> Sign.parent_path;
+ val thy = fold add_one' axs thy;
+
+ (* declare lub_take axioms *)
+ local
+ fun ax_lub_take dname =
+ let
+ val dnam : string = Long_Name.base_name dname;
+ val take_const = %%:(dname^"_take");
+ val lub = %%: @{const_name lub};
+ val image = %%: @{const_name image};
+ val UNIV = %%: @{const_name UNIV};
+ val lhs = lub $ (image $ take_const $ UNIV);
+ val ax = mk_trp (lhs === ID);
+ in
+ add_one (dnam, [("lub_take", ax)], [])
+ end
+ in
+ val thy =
+ if definitional then thy
+ else fold ax_lub_take dnames thy
+ end;
val use_copy_def = length eqs>1 andalso not definitional;
in
thy
- |> Sign.add_path comp_dnam
- |> add_defs_infer ((*bisim_def::*)(if use_copy_def then [copy_def] else []))
+ |> Sign.add_path comp_dnam
+(*
+ |> add_defs_infer [bisim_def]
+*)
|> Sign.parent_path
end; (* let (add_axioms) *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 00:34:26 2010 -0800
@@ -164,7 +164,7 @@
) : cons;
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
- val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs;
+ val thy = thy' |> Domain_Axioms.add_axioms false eqs' comp_dnam eqs;
val ((rewss, take_rews), theorems_thy) =
thy
|> fold_map (fn (eq, (x,cs)) =>
@@ -237,7 +237,7 @@
) : cons;
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
- val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs;
+ val thy = thy' |> Domain_Axioms.add_axioms true eqs' comp_dnam eqs;
val ((rewss, take_rews), theorems_thy) =
thy
|> fold_map (fn (eq, (x,cs)) =>
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 00:34:26 2010 -0800
@@ -122,6 +122,17 @@
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
+fun mk_lub t =
+ let
+ val T = Term.range_type (Term.fastype_of t);
+ val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
+ val UNIV_const = @{term "UNIV :: nat set"};
+ val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
+ val image_const = Const (@{const_name image}, image_type);
+ in
+ lub_const $ (image_const $ t $ UNIV_const)
+ end;
+
(* splits a cterm into the right and lefthand sides of equality *)
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
@@ -424,7 +435,8 @@
fun mk_goal take_const = mk_deflation (take_const $ i);
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
val adm_rules =
- @{thms adm_conj adm_deflation cont2cont_fst cont2cont_snd cont_id};
+ @{thms adm_conj adm_subst [OF _ adm_deflation]
+ cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
take_0_thms @ @{thms deflation_UU simp_thms};
val deflation_rules =
@@ -436,8 +448,10 @@
EVERY
[rtac @{thm nat.induct} 1,
simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
- simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
- REPEAT (resolve_tac deflation_rules 1 ORELSE atac 1)])
+ asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
+ REPEAT (etac @{thm conjE} 1
+ ORELSE resolve_tac deflation_rules 1
+ ORELSE atac 1)])
end;
fun conjuncts [] thm = []
| conjuncts (n::[]) thm = [(n, thm)]
@@ -795,7 +809,8 @@
val start_thms =
@{thm split_def} :: map_apply_thms;
val adm_rules =
- @{thms adm_conj adm_deflation cont2cont_fst cont2cont_snd cont_id};
+ @{thms adm_conj adm_subst [OF _ adm_deflation]
+ cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
@{thms fst_strict snd_strict deflation_UU simp_thms};
val deflation_rules =
@@ -821,115 +836,58 @@
(conjuncts deflation_map_binds deflation_map_thm);
val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy;
- (* define copy combinators *)
- val new_dts =
- map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
- val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns);
- val copy_arg = Free ("f", copy_arg_type);
- val copy_args =
- let fun mk_copy_args [] t = []
- | mk_copy_args (_::[]) t = [t]
- | mk_copy_args (_::xs) t =
- mk_fst t :: mk_copy_args xs (mk_snd t);
- in mk_copy_args doms copy_arg end;
- fun copy_of_dtyp (T, dt) =
- if Datatype_Aux.is_rec_type dt
- then copy_of_dtyp' (T, dt)
- else mk_ID T
- and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i
- | copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = mk_ID T
- | copy_of_dtyp' (T, Datatype_Aux.DtType (c, ds)) =
- case Symtab.lookup map_tab' c of
- SOME f =>
- list_ccomb
- (Const (f, mapT T), map copy_of_dtyp (snd (dest_Type T) ~~ ds))
- | NONE =>
- (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T);
- fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy =
+ (* definitions and proofs related to take functions *)
+ val (take_info, thy) =
+ define_take_functions (dom_binds ~~ iso_infos) thy;
+ val {take_consts, take_defs, chain_take_thms, take_0_thms,
+ take_Suc_thms, deflation_take_thms} = take_info;
+
+ (* least-upper-bound lemma for take functions *)
+ val lub_take_lemma =
let
- val copy_type = copy_arg_type ->> (lhsT ->> lhsT);
- val copy_bind = Binding.suffix_name "_copy" tbind;
- val (copy_const, thy) = thy |>
- Sign.declare_const ((copy_bind, copy_type), NoSyn);
- val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
- val body = copy_of_dtyp (rhsT, dtyp);
- val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
- val rhs = big_lambda copy_arg comp;
- val eqn = Logic.mk_equals (copy_const, rhs);
- val (copy_def, thy) =
- thy
- |> Sign.add_path (Binding.name_of tbind)
- |> yield_singleton (PureThy.add_defs false o map Thm.no_attributes)
- (Binding.name "copy_def", eqn)
- ||> Sign.parent_path;
- in ((copy_const, copy_def), thy) end;
- val ((copy_consts, copy_defs), thy) = thy
- |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
- |>> ListPair.unzip;
-
- (* define combined copy combinator *)
- val ((c_const, c_def_thms), thy) =
- if length doms = 1
- then ((hd copy_consts, []), thy)
- else
- let
- val c_type = copy_arg_type ->> copy_arg_type;
- val c_name = space_implode "_" (map Binding.name_of dom_binds);
- val c_bind = Binding.name (c_name ^ "_copy");
- val c_body =
- mk_tuple (map (mk_capply o rpair copy_arg) copy_consts);
- val c_rhs = big_lambda copy_arg c_body;
- val (c_const, thy) =
- Sign.declare_const ((c_bind, c_type), NoSyn) thy;
- val c_eqn = Logic.mk_equals (c_const, c_rhs);
- val (c_def_thms, thy) =
- thy
- |> Sign.add_path c_name
- |> (PureThy.add_defs false o map Thm.no_attributes)
- [(Binding.name "copy_def", c_eqn)]
- ||> Sign.parent_path;
- in ((c_const, c_def_thms), thy) end;
-
- (* fixed-point lemma for combined copy combinator *)
- val fix_copy_lemma =
- let
- fun mk_map_ID (map_const, (T, rhsT)) =
- list_ccomb (map_const, map mk_ID (snd (dest_Type T)));
+ val lhs = mk_tuple (map mk_lub take_consts);
+ fun mk_map_ID (map_const, (lhsT, rhsT)) =
+ list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT)));
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
- val goal = mk_eqs (mk_fix c_const, rhs);
- val rules =
- [@{thm pair_collapse}, @{thm split_def}]
- @ map_apply_thms
- @ c_def_thms @ copy_defs
- @ MapIdData.get thy;
- val tac = simp_tac (beta_ss addsimps rules) 1;
+ val goal = mk_trp (mk_eq (lhs, rhs));
+ val start_rules =
+ @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
+ @ @{thms pair_collapse split_def}
+ @ map_apply_thms @ MapIdData.get thy;
+ val rules0 =
+ @{thms iterate_0 Pair_strict} @ take_0_thms;
+ val rules1 =
+ @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv}
+ @ take_Suc_thms;
+ val tac =
+ EVERY
+ [simp_tac (HOL_basic_ss addsimps start_rules) 1,
+ simp_tac (HOL_basic_ss addsimps @{thms fix_def2}) 1,
+ rtac @{thm lub_eq} 1,
+ rtac @{thm nat.induct} 1,
+ simp_tac (HOL_basic_ss addsimps rules0) 1,
+ asm_full_simp_tac (beta_ss addsimps rules1) 1];
in
Goal.prove_global thy [] [] goal (K tac)
end;
- (* prove reach lemmas *)
- val reach_thm_projs =
- let fun mk_projs [] t = []
- | mk_projs (x::[]) t = [(x, t)]
- | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
- in mk_projs dom_binds (mk_fix c_const) end;
- fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy =
+ (* prove lub of take equals ID *)
+ fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
let
- val x = Free ("x", lhsT);
- val goal = mk_eqs (mk_capply (t, x), x);
- val rules =
- fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1};
- val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
- val reach_thm = Goal.prove_global thy [] [] goal (K tac);
+ val i = Free ("i", natT);
+ val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT);
+ val tac =
+ EVERY
+ [rtac @{thm trans} 1, rtac map_ID_thm 2,
+ cut_facts_tac [lub_take_lemma] 1,
+ REPEAT (etac @{thm Pair_inject} 1), atac 1];
+ val lub_take_thm = Goal.prove_global thy [] [] goal (K tac);
in
- thy
- |> Sign.add_path (Binding.name_of bind)
- |> yield_singleton (PureThy.add_thms o map Thm.no_attributes)
- (Binding.name "reach", reach_thm)
- ||> Sign.parent_path
+ add_qualified_thm "lub_take" (Binding.name_of bind, lub_take_thm) thy
end;
- val (reach_thms, thy) = thy |>
- fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
+ val (lub_take_thms, thy) =
+ fold_map prove_lub_take
+ (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
in
(iso_infos, thy)
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 00:34:26 2010 -0800
@@ -9,7 +9,6 @@
val calc_syntax:
theory ->
bool ->
- typ ->
(string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list ->
(binding * typ * mixfix) list
@@ -31,7 +30,6 @@
fun calc_syntax thy
(definitional : bool)
- (dtypeprod : typ)
((dname : string, typevars : typ list),
(cons': (binding * (bool * binding option * typ) list * mixfix) list))
: (binding * typ * mixfix) list =
@@ -50,18 +48,16 @@
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_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
end;
(* ----- constants concerning induction ------------------------------------- *)
- val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
val optional_consts =
- if definitional then [] else [const_rep, const_abs, const_copy];
+ if definitional then [] else [const_rep, const_abs];
- in (optional_consts @ [const_take, const_finite])
+ in (optional_consts @ [const_finite])
end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
@@ -75,22 +71,15 @@
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 list =
- map (calc_syntax thy'' definitional funprod) eqs';
+ map (calc_syntax thy'' definitional) eqs';
in thy''
|> Cont_Consts.add_consts
- (flat ctt @
- (if length eqs'>1 andalso not definitional
- then [const_copy] else []) @
- [const_bisim])
+ (flat ctt @ [const_bisim])
end; (* let *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 00:34:26 2010 -0800
@@ -120,7 +120,9 @@
in
val ax_abs_iso = ga "abs_iso" dname;
val ax_rep_iso = ga "rep_iso" dname;
- val ax_copy_def = ga "copy_def" dname;
+ val ax_take_0 = ga "take_0" dname;
+ val ax_take_Suc = ga "take_Suc" dname;
+ val ax_take_strict = ga "take_strict" dname;
end; (* local *)
(* ----- define constructors ------------------------------------------------ *)
@@ -177,68 +179,38 @@
(* ----- theorems concerning one induction step ----------------------------- *)
-val copy_strict =
- let
- val _ = trace " Proving copy_strict...";
- val goal = mk_trp (strict (dc_copy `% "f"));
- val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
- val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
- in
- SOME (pg [ax_copy_def] goal (K tacs))
- handle
- THM (s, _, _) => (trace s; NONE)
- | ERROR s => (trace s; NONE)
- end;
+local
+ fun dc_take dn = %%:(dn^"_take");
+ val dnames = map (fst o fst) eqs;
+ fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
+ val axs_take_strict = map get_take_strict dnames;
-local
- fun copy_app (con, _, args) =
+ fun one_take_app (con, _, args) =
let
- val lhs = dc_copy`%"f"`(con_app con args);
+ fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
if Datatype_Aux.is_rec_type (dtyp_of arg)
then Domain_Axioms.copy_of_dtyp map_tab
- (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+ mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
+ val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
val rhs = con_app2 con one_rhs args;
fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
- val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
- (* FIXME! case_UU_tac *)
- fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
- val rules = [ax_abs_iso] @ @{thms domain_map_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;
+ val goal = mk_trp (lhs === rhs);
+ val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
+ val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
+ val tacs =
+ [simp_tac (HOL_basic_ss addsimps rules) 1,
+ asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
+ in pg con_appls goal (K tacs) end;
+ val take_apps = map (Drule.export_without_context o one_take_app) cons;
in
- val _ = trace " Proving copy_apps...";
- val copy_apps = map copy_app cons;
+ val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
end;
-local
- fun one_strict (con, _, args) =
- let
- val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
- val rews = the_list copy_strict @ copy_apps @ con_rews;
- (* FIXME! case_UU_tac *)
- fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
- [asm_simp_tac (HOLCF_ss addsimps rews) 1];
- in
- SOME (pg [] goal tacs)
- handle
- THM (s, _, _) => (trace s; NONE)
- | ERROR s => (trace s; NONE)
- end;
-
- fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args;
-in
- val _ = trace " Proving copy_stricts...";
- val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons);
-end;
-
-val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts;
-
in
thy
|> Sign.add_path (Long_Name.base_name dname)
@@ -257,12 +229,12 @@
((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
((Binding.name "injects" , injects ), [Simplifier.simp_add]),
- ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]),
+ ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
((Binding.name "match_rews", mat_rews ),
[Simplifier.simp_add, Fixrec.fixrec_simp_add])]
|> Sign.parent_path
|> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- pat_rews @ dist_les @ dist_eqs @ copy_rews)
+ pat_rews @ dist_les @ dist_eqs)
end; (* let *)
fun comp_theorems (comp_dnam, eqs: eq list) thy =
@@ -282,10 +254,10 @@
local
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
in
- val axs_reach = map (ga "reach" ) dnames;
val axs_take_def = map (ga "take_def" ) dnames;
+ val axs_chain_take = map (ga "chain_take") dnames;
+ val axs_lub_take = map (ga "lub_take" ) dnames;
val axs_finite_def = map (ga "finite_def") dnames;
- val ax_copy2_def = ga "copy_def" comp_dnam;
(* TEMPORARILY DISABLED
val ax_bisim_def = ga "bisim_def" comp_dnam;
TEMPORARILY DISABLED *)
@@ -297,7 +269,6 @@
in
val cases = map (gt "casedist" ) dnames;
val con_rews = maps (gts "con_rews" ) dnames;
- val copy_rews = maps (gts "copy_rews") dnames;
end;
fun dc_take dn = %%:(dn^"_take");
@@ -307,55 +278,8 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
-local
- val iterate_Cprod_ss = global_simpset_of @{theory Fix};
- val copy_con_rews = copy_rews @ con_rews;
- val copy_take_defs =
- (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
- val _ = trace " Proving take_stricts...";
- fun one_take_strict ((dn, args), _) =
- let
- val goal = mk_trp (strict (dc_take dn $ %:"n"));
- val rules = [
- @{thm monofun_fst [THEN monofunE]},
- @{thm monofun_snd [THEN monofunE]}];
- val tacs = [
- rtac @{thm UU_I} 1,
- rtac @{thm below_eq_trans} 1,
- resolve_tac axs_reach 2,
- rtac @{thm monofun_cfun_fun} 1,
- REPEAT (resolve_tac rules 1),
- rtac @{thm iterate_below_fix} 1];
- in pg axs_take_def goal (K tacs) end;
- val take_stricts = map one_take_strict eqs;
- fun take_0 n dn =
- let
- val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU);
- in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
- val take_0s = mapn take_0 1 dnames;
- val _ = trace " Proving take_apps...";
- fun one_take_app dn (con, _, args) =
- let
- fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
- fun one_rhs arg =
- if Datatype_Aux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp map_tab
- mk_take (dtyp_of arg) ` (%# arg)
- else (%# arg);
- val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
- val rhs = con_app2 con one_rhs args;
- fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
- fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
- fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
- val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
- in pg copy_take_defs goal (K tacs) end;
- fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons;
- val take_apps = maps one_take_apps eqs;
-in
- val take_rews = map Drule.export_without_context
- (take_stricts @ take_0s @ take_apps);
-end; (* local *)
+val take_rews =
+ maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
local
fun one_con p (con, _, args) =
@@ -375,7 +299,7 @@
fun ind_term concf = Library.foldr one_eq
(mapn (fn n => fn x => (P_name n, x)) 1 conss,
mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
- val take_ss = HOL_ss addsimps take_rews;
+ val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
fun quant_tac ctxt i = EVERY
(mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
@@ -449,28 +373,15 @@
val _ = trace " Proving take_lemmas...";
val take_lemmas =
let
- fun take_lemma n (dn, ax_reach) =
- let
- val lhs = dc_take dn $ Bound 0 `%(x_name n);
- val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
- val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
- val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
- val rules = [contlub_fst RS contlubE RS ssubst,
- contlub_snd RS contlubE RS ssubst];
- fun tacf {prems, context} = [
- res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
- res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
- stac fix_def2 1,
- REPEAT (CHANGED
- (resolve_tac rules 1 THEN chain_tac 1)),
- stac contlub_cfun_fun 1,
- stac contlub_cfun_fun 2,
- rtac lub_equal 3,
- chain_tac 1,
- rtac allI 1,
- resolve_tac prems 1];
- in pg'' thy axs_take_def goal tacf end;
- in mapn take_lemma 1 (dnames ~~ axs_reach) end;
+ fun take_lemma (ax_chain_take, ax_lub_take) =
+ @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take];
+ in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
+
+ val axs_reach =
+ let
+ fun reach (ax_chain_take, ax_lub_take) =
+ @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take];
+ in map reach (axs_chain_take ~~ axs_lub_take) end;
(* ----- theorems concerning finiteness and induction ----------------------- *)
@@ -580,22 +491,28 @@
val cont_rules =
[cont_id, cont_const, cont2cont_Rep_CFun,
cont2cont_fst, cont2cont_snd];
+ val subgoal =
+ let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
+ in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
+ val subgoal' = legacy_infer_term thy subgoal;
fun tacf {prems, context} =
- map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
- quant_tac context 1,
- rtac (adm_impl_admw RS wfix_ind) 1,
- REPEAT_DETERM (rtac adm_all 1),
- REPEAT_DETERM (
- TRY (rtac adm_conj 1) THEN
- rtac adm_subst 1 THEN
- REPEAT (resolve_tac cont_rules 1) THEN
- resolve_tac prems 1),
- strip_tac 1,
- rtac (rewrite_rule axs_take_def finite_ind) 1,
- ind_prems_tac prems];
+ let
+ val subtac =
+ EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
+ val subthm = Goal.prove context [] [] subgoal' (K subtac);
+ in
+ map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
+ cut_facts_tac (subthm :: take (length dnames) prems) 1,
+ REPEAT (rtac @{thm conjI} 1 ORELSE
+ EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
+ resolve_tac axs_chain_take 1,
+ asm_simp_tac HOL_basic_ss 1])
+ ]
+ end;
val ind = (pg'' thy [] goal tacf
handle ERROR _ =>
- (warning "Cannot prove infinite induction rule"; TrueI));
+ (warning "Cannot prove infinite induction rule"; TrueI)
+ );
in (finites, ind) end
)
handle THM _ =>
@@ -603,7 +520,6 @@
| ERROR _ =>
(warning "Cannot prove induction rule"; ([], TrueI));
-
end; (* local *)
(* ----- theorem concerning coinduction ------------------------------------- *)
@@ -667,8 +583,8 @@
in thy |> Sign.add_path comp_dnam
|> snd o PureThy.add_thmss [
- ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
((Binding.name "take_lemmas", take_lemmas ), []),
+ ((Binding.name "reach" , axs_reach ), []),
((Binding.name "finites" , finites ), []),
((Binding.name "finite_ind" , [finite_ind]), []),
((Binding.name "ind" , [ind] ), [])(*,
--- a/src/HOLCF/ex/Domain_ex.thy Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy Tue Mar 02 00:34:26 2010 -0800
@@ -134,7 +134,7 @@
text {* Rules about case combinator *}
term tree_when
-thm tree.when_def
+thm tree.tree_when_def
thm tree.when_rews
text {* Rules about selectors *}
@@ -157,16 +157,17 @@
term match_Node
thm tree.match_rews
-text {* Rules about copy function *}
-term tree_copy
-thm tree.copy_def
-thm tree.copy_rews
-
text {* Rules about take function *}
term tree_take
thm tree.take_def
+thm tree.take_0
+thm tree.take_Suc
thm tree.take_rews
+thm tree.chain_take
+thm tree.take_take
+thm tree.deflation_take
thm tree.take_lemmas
+thm tree.reach
thm tree.finite_ind
text {* Rules about finiteness predicate *}
--- a/src/HOLCF/ex/New_Domain.thy Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/ex/New_Domain.thy Tue Mar 02 00:34:26 2010 -0800
@@ -51,12 +51,12 @@
thm ltree.reach
text {*
- The definition of the copy function uses map functions associated with
+ The definition of the take function uses map functions associated with
each type constructor involved in the definition. A map function
for the lazy list type has been generated by the new domain package.
*}
-thm ltree.copy_def
+thm ltree.take_rews
thm llist_map_def
lemma ltree_induct:
@@ -67,24 +67,24 @@
assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
shows "P x"
proof -
- have "\<forall>x. P (fix\<cdot>ltree_copy\<cdot>x)"
- proof (rule fix_ind)
- show "adm (\<lambda>a. \<forall>x. P (a\<cdot>x))"
- by (simp add: adm_subst [OF _ adm])
- next
- show "\<forall>x. P (\<bottom>\<cdot>x)"
- by (simp add: bot)
- next
- fix f :: "'a ltree \<rightarrow> 'a ltree"
- assume f: "\<forall>x. P (f\<cdot>x)"
- show "\<forall>x. P (ltree_copy\<cdot>f\<cdot>x)"
- apply (rule allI)
- apply (case_tac x)
- apply (simp add: bot)
- apply (simp add: Leaf)
- apply (simp add: Branch [OF f])
- done
- qed
+ have "P (\<Squnion>i. ltree_take i\<cdot>x)"
+ using adm
+ proof (rule admD)
+ fix i
+ show "P (ltree_take i\<cdot>x)"
+ proof (induct i arbitrary: x)
+ case (0 x)
+ show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
+ next
+ case (Suc n x)
+ show "P (ltree_take (Suc n)\<cdot>x)"
+ apply (cases x)
+ apply (simp add: bot)
+ apply (simp add: Leaf)
+ apply (simp add: Branch Suc)
+ done
+ qed
+ qed (simp add: ltree.chain_take)
thus ?thesis
by (simp add: ltree.reach)
qed
--- a/src/HOLCF/ex/Stream.thy Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy Tue Mar 02 00:34:26 2010 -0800
@@ -143,16 +143,10 @@
lemma stream_reach2: "(LUB i. stream_take i$s) = s"
-apply (insert stream.reach [of s], erule subst) back
-apply (simp add: fix_def2 stream.take_def)
-apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
-by simp
+by (rule stream.reach)
lemma chain_stream_take: "chain (%i. stream_take i$s)"
-apply (rule chainI)
-apply (rule monofun_cfun_fun)
-apply (simp add: stream.take_def del: iterate_Suc)
-by (rule chainE, simp)
+by (simp add: stream.chain_take)
lemma stream_take_prefix [simp]: "stream_take n$s << s"
apply (insert stream_reach2 [of s])
@@ -259,10 +253,9 @@
lemma stream_ind2:
"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x"
apply (insert stream.reach [of x],erule subst)
-apply (frule adm_impl_admw, rule wfix_ind, auto)
-apply (rule adm_subst [THEN adm_impl_admw],auto)
+apply (erule admD, rule chain_stream_take)
apply (insert stream_finite_ind2 [of P])
-by (simp add: stream.take_def)
+by simp