--- a/src/HOLCF/Domain.thy Fri Mar 05 23:52:09 2010 +0100
+++ b/src/HOLCF/Domain.thy Sat Mar 06 00:21:21 2010 +0100
@@ -214,6 +214,102 @@
ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
+subsection {* Take functions and finiteness *}
+
+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)
+
+text {*
+ Let a ``decisive'' function be a deflation that maps every input to
+ either itself or bottom. Then if a domain's take functions are all
+ decisive, then all values in the domain are finite.
+*}
+
+definition
+ decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
+where
+ "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
+
+lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
+ unfolding decisive_def by simp
+
+lemma decisive_cases:
+ assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
+using assms unfolding decisive_def by auto
+
+lemma decisive_bottom: "decisive \<bottom>"
+ unfolding decisive_def by simp
+
+lemma decisive_ID: "decisive ID"
+ unfolding decisive_def by simp
+
+lemma decisive_ssum_map:
+ assumes f: "decisive f"
+ assumes g: "decisive g"
+ shows "decisive (ssum_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_sprod_map:
+ assumes f: "decisive f"
+ assumes g: "decisive g"
+ shows "decisive (sprod_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_abs_rep:
+ fixes abs rep
+ assumes iso: "iso abs rep"
+ assumes d: "decisive d"
+ shows "decisive (abs oo d oo rep)"
+apply (rule decisiveI)
+apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
+apply (simp add: iso.rep_iso [OF iso])
+apply (simp add: iso.abs_strict [OF iso])
+done
+
+lemma lub_ID_finite:
+ assumes chain: "chain d"
+ assumes lub: "(\<Squnion>n. d n) = ID"
+ assumes decisive: "\<And>n. decisive (d n)"
+ shows "\<exists>n. d n\<cdot>x = x"
+proof -
+ have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
+ have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
+ have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
+ using decisive unfolding decisive_def by simp
+ hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
+ by auto
+ hence "finite (range (\<lambda>n. d n\<cdot>x))"
+ by (rule finite_subset, simp)
+ with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
+ by (rule finite_range_imp_finch)
+ then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
+ unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
+ with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
+qed
+
+
subsection {* Installing the domain package *}
lemmas con_strict_rules =
@@ -253,23 +349,6 @@
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/Representable.thy Fri Mar 05 23:52:09 2010 +0100
+++ b/src/HOLCF/Representable.thy Sat Mar 06 00:21:21 2010 +0100
@@ -12,6 +12,44 @@
("Tools/Domain/domain_isomorphism.ML")
begin
+subsection {* Preliminaries: Take proofs *}
+
+text {*
+ This section contains lemmas that are used in a module that supports
+ the domain isomorphism package; the module contains proofs related
+ to take functions and the finiteness predicate.
+*}
+
+lemma deflation_abs_rep:
+ fixes abs and rep and d
+ assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
+ assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
+ shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
+by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
+
+lemma deflation_chain_min:
+ assumes chain: "chain d"
+ assumes defl: "\<And>n. deflation (d n)"
+ shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
+proof (rule linorder_le_cases)
+ assume "m \<le> n"
+ with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
+ by (rule deflation_below_comp1 [OF defl defl])
+ moreover from `m \<le> n` have "min m n = m" by simp
+ ultimately show ?thesis by simp
+next
+ assume "n \<le> m"
+ with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
+ by (rule deflation_below_comp2 [OF defl defl])
+ moreover from `n \<le> m` have "min m n = n" by simp
+ ultimately show ?thesis by simp
+qed
+
+use "Tools/Domain/domain_take_proofs.ML"
+
+
subsection {* Class of representable types *}
text "Overloaded embedding and projection functions between
@@ -180,33 +218,6 @@
shows "abs\<cdot>(rep\<cdot>x) = x"
unfolding abs_def rep_def by (simp add: REP [symmetric])
-lemma deflation_abs_rep:
- fixes abs and rep and d
- assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
- assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
- shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
-by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
-
-lemma deflation_chain_min:
- assumes chain: "chain d"
- assumes defl: "\<And>n. deflation (d n)"
- shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
-proof (rule linorder_le_cases)
- assume "m \<le> n"
- with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
- by (rule deflation_below_comp1 [OF defl defl])
- moreover from `m \<le> n` have "min m n = m" by simp
- ultimately show ?thesis by simp
-next
- assume "n \<le> m"
- with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
- by (rule deflation_below_comp2 [OF defl defl])
- moreover from `n \<le> m` have "min m n = n" by simp
- ultimately show ?thesis by simp
-qed
-
subsection {* Proving a subtype is representable *}
@@ -777,7 +788,6 @@
subsection {* Constructing Domain Isomorphisms *}
-use "Tools/Domain/domain_take_proofs.ML"
use "Tools/Domain/domain_isomorphism.ML"
setup {*
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Mar 05 23:52:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Mar 06 00:21:21 2010 +0100
@@ -99,26 +99,13 @@
infix -->>;
infix 9 `;
-val deflT = @{typ "udom alg_defl"};
-
fun mapT (T as Type (_, Ts)) =
(map (fn T => T ->> T) Ts) -->> (T ->> T)
| mapT T = T ->> T;
-fun mk_Rep_of T =
- Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
-
-fun coerce_const T = Const (@{const_name coerce}, T);
-
-fun isodefl_const T =
- Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
-
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
-(* splits a cterm into the right and lefthand sides of equality *)
-fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
-
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
(******************************************************************************)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Mar 05 23:52:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 06 00:21:21 2010 +0100
@@ -216,8 +216,13 @@
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
in
+ val axs_rep_iso = map (ga "rep_iso") dnames;
+ val axs_abs_iso = map (ga "abs_iso") dnames;
val axs_chain_take = map (ga "chain_take") dnames;
+ val lub_take_thms = map (ga "lub_take") dnames;
val axs_finite_def = map (ga "finite_def") dnames;
+ val take_0_thms = map (ga "take_0") dnames;
+ val take_Suc_thms = map (ga "take_Suc") dnames;
val cases = map (ga "casedist" ) dnames;
val con_rews = maps (gts "con_rews" ) dnames;
end;
@@ -318,75 +323,41 @@
(
if is_finite
then (* finite case *)
- let
- fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
- fun dname_lemma dn =
- let
- val prem1 = mk_trp (defined (%:"x"));
- val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
- val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
- val concl = mk_trp (take_enough dn);
- val goal = prem1 ===> prem2 ===> concl;
- val tacs = [
- etac disjE 1,
- etac notE 1,
- resolve_tac take_lemmas 1,
- 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
+ val decisive_lemma =
let
- fun mk_eqn n ((dn, args), _) =
- let
- val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
- val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
- in
- mk_constrainall
- (x_name n, Type (dn,args), mk_disj (disj1, disj2))
- end;
- val goal =
- mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
- fun arg_tacs ctxt vn = [
- eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
- etac disjE 1,
- asm_simp_tac (HOL_ss addsimps con_rews) 1,
- asm_simp_tac take_ss 1];
- fun con_tacs ctxt (con, args) =
- asm_simp_tac take_ss 1 ::
- maps (arg_tacs ctxt) (nonlazy_rec args);
- fun foo_tacs ctxt n (cons, cases) =
- simp_tac take_ss 1 ::
- rtac allI 1 ::
- res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
- asm_simp_tac take_ss 1 ::
- maps (con_tacs ctxt) cons;
- fun tacs ctxt =
- rtac allI 1 ::
- InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
- simp_tac take_ss 1 ::
- TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
- flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
- in pg [] goal tacs end;
-
- fun one_finite (dn, l1b) =
+ val iso_locale_thms =
+ map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
+ axs_abs_iso axs_rep_iso;
+ val decisive_abs_rep_thms =
+ map (fn x => @{thm decisive_abs_rep} OF [x])
+ iso_locale_thms;
+ val n = Free ("n", @{typ nat});
+ fun mk_decisive t = %%: @{const_name decisive} $ t;
+ fun f dn = mk_decisive (dc_take dn $ n);
+ val goal = mk_trp (foldr1 mk_conj (map f dnames));
+ val rules0 = @{thm decisive_bottom} :: take_0_thms;
+ val rules1 =
+ take_Suc_thms @ decisive_abs_rep_thms
+ @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
+ val tacs = [
+ rtac @{thm nat.induct} 1,
+ simp_tac (HOL_ss addsimps rules0) 1,
+ asm_simp_tac (HOL_ss addsimps rules1) 1];
+ in pg [] goal (K tacs) end;
+ fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
+ fun one_finite (dn, decisive_thm) =
let
val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
- fun tacs ctxt = [
- (* FIXME! case_UU_tac *)
- case_UU_tac ctxt take_rews 1 "x",
- eresolve_tac finite_lemmas1a 1,
- step_tac HOL_cs 1,
- step_tac HOL_cs 1,
- cut_facts_tac [l1b] 1,
- fast_tac HOL_cs 1];
- in pg axs_finite_def goal tacs end;
+ val tacs = [
+ rtac @{thm lub_ID_finite} 1,
+ resolve_tac axs_chain_take 1,
+ resolve_tac lub_take_thms 1,
+ rtac decisive_thm 1];
+ in pg axs_finite_def goal (K tacs) end;
val _ = trace " Proving finites";
- val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
+ val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
val _ = trace " Proving ind";
val ind =
let