# HG changeset patch # User huffman # Date 1236954647 25200 # Node ID 110e59507eec584c9b4ece213b2c5a8b04b26998 # Parent b32d62c9c5835f5289015bb30a85fd03efec119b introduce new helper functions; clean up proofs diff -r b32d62c9c583 -r 110e59507eec src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Fri Mar 13 13:06:36 2009 +0100 +++ b/src/HOLCF/Universal.thy Fri Mar 13 07:30:47 2009 -0700 @@ -13,35 +13,35 @@ definition node :: "nat \ ubasis \ ubasis set \ ubasis" where - "node i x A = Suc (prod2nat (i, prod2nat (x, set2nat A)))" + "node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))" -lemma node_not_0 [simp]: "node i x A \ 0" +lemma node_not_0 [simp]: "node i a S \ 0" unfolding node_def by simp -lemma node_gt_0 [simp]: "0 < node i x A" +lemma node_gt_0 [simp]: "0 < node i a S" unfolding node_def by simp lemma node_inject [simp]: - "\finite A; finite B\ - \ node i x A = node j y B \ i = j \ x = y \ A = B" + "\finite S; finite T\ + \ node i a S = node j b T \ i = j \ a = b \ S = T" unfolding node_def by simp -lemma node_gt0: "i < node i x A" +lemma node_gt0: "i < node i a S" unfolding node_def less_Suc_eq_le by (rule le_prod2nat_1) -lemma node_gt1: "x < node i x A" +lemma node_gt1: "a < node i a S" unfolding node_def less_Suc_eq_le by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2]) lemma nat_less_power2: "n < 2^n" by (induct n) simp_all -lemma node_gt2: "\finite A; y \ A\ \ y < node i x A" +lemma node_gt2: "\finite S; b \ S\ \ b < node i a S" unfolding node_def less_Suc_eq_le set2nat_def apply (rule order_trans [OF _ le_prod2nat_2]) apply (rule order_trans [OF _ le_prod2nat_2]) -apply (rule order_trans [where y="setsum (op ^ 2) {y}"]) +apply (rule order_trans [where y="setsum (op ^ 2) {b}"]) apply (simp add: nat_less_power2 [THEN order_less_imp_le]) apply (erule setsum_mono2, simp, simp) done @@ -52,7 +52,7 @@ lemma node_cases: assumes 1: "x = 0 \ P" - assumes 2: "\i y A. \finite A; x = node i y A\ \ P" + assumes 2: "\i a S. \finite S; x = node i a S\ \ P" shows "P" apply (cases x) apply (erule 1) @@ -65,7 +65,7 @@ lemma node_induct: assumes 1: "P 0" - assumes 2: "\i x A. \P x; finite A; \y\A. P y\ \ P (node i x A)" + assumes 2: "\i a S. \P a; finite S; \b\S. P b\ \ P (node i a S)" shows "P x" apply (induct x rule: nat_less_induct) apply (case_tac n rule: node_cases) @@ -78,13 +78,13 @@ inductive ubasis_le :: "nat \ nat \ bool" where - ubasis_le_refl: "ubasis_le x x" + ubasis_le_refl: "ubasis_le a a" | ubasis_le_trans: - "\ubasis_le x y; ubasis_le y z\ \ ubasis_le x z" + "\ubasis_le a b; ubasis_le b c\ \ ubasis_le a c" | ubasis_le_lower: - "finite A \ ubasis_le x (node i x A)" + "finite S \ ubasis_le a (node i a S)" | ubasis_le_upper: - "\finite A; y \ A; ubasis_le x y\ \ ubasis_le (node i x A) y" + "\finite S; b \ S; ubasis_le a b\ \ ubasis_le (node i a S) b" lemma ubasis_le_minimal: "ubasis_le 0 x" apply (induct x rule: node_induct) @@ -99,8 +99,8 @@ ubasis_until :: "(ubasis \ bool) \ ubasis \ ubasis" where "ubasis_until P 0 = 0" -| "finite A \ ubasis_until P (node i x A) = - (if P (node i x A) then node i x A else ubasis_until P x)" +| "finite S \ ubasis_until P (node i a S) = + (if P (node i a S) then node i a S else ubasis_until P a)" apply clarify apply (rule_tac x=b in node_cases) apply simp @@ -157,8 +157,8 @@ done lemma ubasis_until_mono: - assumes "\i x A y. \finite A; P (node i x A); y \ A; ubasis_le x y\ \ P y" - shows "ubasis_le x y \ ubasis_le (ubasis_until P x) (ubasis_until P y)" + assumes "\i a S b. \finite S; P (node i a S); b \ S; ubasis_le a b\ \ P b" + shows "ubasis_le a b \ ubasis_le (ubasis_until P a) (ubasis_until P b)" apply (induct set: ubasis_le) apply (rule ubasis_le_refl) apply (erule (1) ubasis_le_trans) @@ -510,6 +510,12 @@ lemma rank_le_iff: "rank x \ n \ cb_take n x = x" by (rule iffI [OF rank_leD rank_leI]) +lemma rank_compact_bot [simp]: "rank compact_bot = 0" +using rank_leI [of 0 compact_bot] by simp + +lemma rank_eq_0_iff [simp]: "rank x = 0 \ x = compact_bot" +using rank_le_iff [of x 0] by auto + definition rank_le :: "'a compact_basis \ 'a compact_basis set" where @@ -558,15 +564,15 @@ lemma rank_lt_Un_rank_eq: "rank_lt x \ rank_eq x = rank_le x" unfolding rank_lt_def rank_eq_def rank_le_def by auto -subsubsection {* Reordering of basis elements *} +subsubsection {* Sequencing basis elements *} definition - reorder :: "'a compact_basis \ nat" + place :: "'a compact_basis \ nat" where - "reorder x = card (rank_lt x) + choose_pos (rank_eq x) x" + "place x = card (rank_lt x) + choose_pos (rank_eq x) x" -lemma reorder_bounded: "reorder x < card (rank_le x)" -unfolding reorder_def +lemma place_bounded: "place x < card (rank_le x)" +unfolding place_def apply (rule ord_less_eq_trans) apply (rule add_strict_left_mono) apply (rule choose_pos_bounded) @@ -579,53 +585,77 @@ apply (simp add: rank_lt_Un_rank_eq) done -lemma reorder_ge: "card (rank_lt x) \ reorder x" -unfolding reorder_def by simp +lemma place_ge: "card (rank_lt x) \ place x" +unfolding place_def by simp -lemma reorder_rank_mono: +lemma place_rank_mono: fixes x y :: "'a compact_basis" - shows "rank x < rank y \ reorder x < reorder y" -apply (rule less_le_trans [OF reorder_bounded]) -apply (rule order_trans [OF _ reorder_ge]) + shows "rank x < rank y \ place x < place y" +apply (rule less_le_trans [OF place_bounded]) +apply (rule order_trans [OF _ place_ge]) apply (rule card_mono) apply (rule finite_rank_lt) apply (simp add: rank_le_def rank_lt_def subset_eq) done -lemma reorder_eqD: "reorder x = reorder y \ x = y" +lemma place_eqD: "place x = place y \ x = y" apply (rule linorder_cases [where x="rank x" and y="rank y"]) - apply (drule reorder_rank_mono, simp) - apply (simp add: reorder_def) + apply (drule place_rank_mono, simp) + apply (simp add: place_def) apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD]) apply (rule finite_rank_eq) apply (simp cong: rank_lt_cong rank_eq_cong) apply (simp add: rank_eq_def) apply (simp add: rank_eq_def) - apply (drule reorder_rank_mono, simp) + apply (drule place_rank_mono, simp) done -lemma inj_reorder: "inj reorder" -by (rule inj_onI, erule reorder_eqD) +lemma inj_place: "inj place" +by (rule inj_onI, erule place_eqD) subsubsection {* Embedding and projection on basis elements *} +definition + sub :: "'a compact_basis \ 'a compact_basis" +where + "sub x = (case rank x of 0 \ compact_bot | Suc k \ cb_take k x)" + +lemma rank_sub_less: "x \ compact_bot \ rank (sub x) < rank x" +unfolding sub_def +apply (cases "rank x", simp) +apply (simp add: less_Suc_eq_le) +apply (rule rank_leI) +apply (rule cb_take_idem) +done + +lemma place_sub_less: "x \ compact_bot \ place (sub x) < place x" +apply (rule place_rank_mono) +apply (erule rank_sub_less) +done + +lemma sub_below: "sub x \ x" +unfolding sub_def by (cases "rank x", simp_all add: cb_take_less) + +lemma rank_less_imp_below_sub: "\x \ y; rank x < rank y\ \ x \ sub y" +unfolding sub_def +apply (cases "rank y", simp) +apply (simp add: less_Suc_eq_le) +apply (subgoal_tac "cb_take nat x \ cb_take nat y") +apply (simp add: rank_leD) +apply (erule cb_take_mono) +done + function basis_emb :: "'a compact_basis \ ubasis" where "basis_emb x = (if x = compact_bot then 0 else - node - (reorder x) - (case rank x of 0 \ 0 | Suc k \ basis_emb (cb_take k x)) - (basis_emb ` {y. reorder y < reorder x \ x \ y}))" + node (place x) (basis_emb (sub x)) + (basis_emb ` {y. place y < place x \ x \ y}))" by auto termination basis_emb -apply (relation "measure reorder", simp) -apply simp -apply (rule reorder_rank_mono) -apply (simp add: less_Suc_eq_le) -apply (rule rank_leI) -apply (rule cb_take_idem) +apply (relation "measure place", simp) +apply (simp add: place_sub_less) apply simp done @@ -634,101 +664,68 @@ lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0" by (simp add: basis_emb.simps) -lemma fin1: "finite {y. reorder y < reorder x \ x \ y}" +lemma fin1: "finite {y. place y < place x \ x \ y}" apply (subst Collect_conj_eq) apply (rule finite_Int) apply (rule disjI1) -apply (subgoal_tac "finite (reorder -` {n. n < reorder x})", simp) -apply (rule finite_vimageI [OF _ inj_reorder]) +apply (subgoal_tac "finite (place -` {n. n < place x})", simp) +apply (rule finite_vimageI [OF _ inj_place]) apply (simp add: lessThan_def [symmetric]) done -lemma fin2: "finite (basis_emb ` {y. reorder y < reorder x \ x \ y})" +lemma fin2: "finite (basis_emb ` {y. place y < place x \ x \ y})" by (rule finite_imageI [OF fin1]) -lemma basis_emb_mono [OF refl]: - "\n = max (reorder x) (reorder y); x \ y\ - \ ubasis_le (basis_emb x) (basis_emb y)" -proof (induct n arbitrary: x y rule: less_induct) +lemma rank_place_mono: + "\place x < place y; x \ y\ \ rank x < rank y" +apply (rule linorder_cases, assumption) +apply (simp add: place_def cong: rank_lt_cong rank_eq_cong) +apply (drule choose_pos_lessD) +apply (rule finite_rank_eq) +apply (simp add: rank_eq_def) +apply (simp add: rank_eq_def) +apply simp +apply (drule place_rank_mono, simp) +done + +lemma basis_emb_mono: + "x \ y \ ubasis_le (basis_emb x) (basis_emb y)" +proof (induct n \ "max (place x) (place y)" arbitrary: x y rule: less_induct) case (less n) - assume IH: - "\(m::nat) (x::'a compact_basis) y. - \m < n; m = max (reorder x) (reorder y); x \ y\ - \ ubasis_le (basis_emb x) (basis_emb y)" - assume n: "n = max (reorder x) (reorder y)" - assume less: "x \ y" - show ?case - proof (cases) - assume "x = compact_bot" - thus ?case by (simp add: ubasis_le_minimal) - next - assume x_neq [simp]: "x \ compact_bot" - with less have y_neq [simp]: "y \ compact_bot" - apply clarify - apply (drule antisym_less [OF compact_bot_minimal]) - apply simp + hence IH: + "\(a::'a compact_basis) b. + \max (place a) (place b) < max (place x) (place y); a \ b\ + \ ubasis_le (basis_emb a) (basis_emb b)" + by simp + show ?case proof (rule linorder_cases) + assume "place x < place y" + then have "rank x < rank y" + using `x \ y` by (rule rank_place_mono) + with `place x < place y` show ?case + apply (case_tac "y = compact_bot", simp) + apply (simp add: basis_emb.simps [of y]) + apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) + apply (rule IH) + apply (simp add: less_max_iff_disj) + apply (erule place_sub_less) + apply (erule rank_less_imp_below_sub [OF `x \ y`]) done - show ?case - proof (rule linorder_cases) - assume 1: "reorder x < reorder y" - show ?case - proof (rule linorder_cases) - assume "rank x < rank y" - with 1 show ?case - apply (case_tac "rank y", simp) - apply (subst basis_emb.simps [where x=y]) - apply simp - apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) - apply (rule IH [OF _ refl, unfolded n]) - apply (simp add: less_max_iff_disj) - apply (rule reorder_rank_mono) - apply (simp add: less_Suc_eq_le) - apply (rule rank_leI) - apply (rule cb_take_idem) - apply (simp add: less_Suc_eq_le) - apply (subgoal_tac "cb_take nat x \ cb_take nat y") - apply (simp add: rank_leD) - apply (rule cb_take_mono [OF less]) - done - next - assume "rank x = rank y" - with 1 show ?case - apply (simp add: reorder_def) - apply (simp cong: rank_lt_cong rank_eq_cong) - apply (drule choose_pos_lessD) - apply (rule finite_rank_eq) - apply (simp add: rank_eq_def) - apply (simp add: rank_eq_def) - apply (simp add: less) - done - next - assume "rank x > rank y" - hence "reorder x > reorder y" - by (rule reorder_rank_mono) - with 1 show ?case by simp - qed - next - assume "reorder x = reorder y" - hence "x = y" by (rule reorder_eqD) - thus ?case by (simp add: ubasis_le_refl) - next - assume "reorder x > reorder y" - with less show ?case - apply (simp add: basis_emb.simps [where x=x]) - apply (rule ubasis_le_upper [OF fin2], simp) - apply (cases "rank x") - apply (simp add: ubasis_le_minimal) - apply simp - apply (rule IH [OF _ refl, unfolded n]) - apply (simp add: less_max_iff_disj) - apply (rule reorder_rank_mono) - apply (simp add: less_Suc_eq_le) - apply (rule rank_leI) - apply (rule cb_take_idem) - apply (erule rev_trans_less) - apply (rule cb_take_less) - done - qed + next + assume "place x = place y" + hence "x = y" by (rule place_eqD) + thus ?case by (simp add: ubasis_le_refl) + next + assume "place x > place y" + with `x \ y` show ?case + apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal) + apply (simp add: basis_emb.simps [of x]) + apply (rule ubasis_le_upper [OF fin2], simp) + apply (rule IH) + apply (simp add: less_max_iff_disj) + apply (erule place_sub_less) + apply (erule rev_trans_less) + apply (rule sub_below) + done qed qed @@ -740,14 +737,14 @@ apply (simp add: basis_emb.simps) apply (simp add: basis_emb.simps) apply (simp add: basis_emb.simps) - apply (simp add: fin2 inj_eq [OF inj_reorder]) + apply (simp add: fin2 inj_eq [OF inj_place]) done definition - basis_prj :: "nat \ 'a compact_basis" + basis_prj :: "ubasis \ 'a compact_basis" where "basis_prj x = inv basis_emb - (ubasis_until (\x. x \ range (basis_emb :: 'a compact_basis \ nat)) x)" + (ubasis_until (\x. x \ range (basis_emb :: 'a compact_basis \ ubasis)) x)" lemma basis_prj_basis_emb: "\x. basis_prj (basis_emb x) = x" unfolding basis_prj_def @@ -758,8 +755,8 @@ done lemma basis_prj_node: - "\finite A; node i x A \ range (basis_emb :: 'a compact_basis \ nat)\ - \ basis_prj (node i x A) = (basis_prj x :: 'a compact_basis)" + "\finite S; node i a S \ range (basis_emb :: 'a compact_basis \ nat)\ + \ basis_prj (node i a S) = (basis_prj a :: 'a compact_basis)" unfolding basis_prj_def by simp lemma basis_prj_0: "basis_prj 0 = compact_bot" @@ -767,32 +764,41 @@ apply (rule basis_prj_basis_emb) done -lemma basis_prj_mono: "ubasis_le x y \ basis_prj x \ basis_prj y" - apply (erule ubasis_le.induct) - apply (rule refl_less) - apply (erule (1) trans_less) - apply (case_tac "node i x A \ range (basis_emb :: 'a compact_basis \ nat)") - apply (erule rangeE, rename_tac a) - apply (case_tac "a = compact_bot", simp) - apply (simp add: basis_prj_basis_emb) - apply (simp add: basis_emb.simps) - apply (clarsimp simp add: fin2) - apply (case_tac "rank a", simp) - apply (simp add: basis_prj_0) - apply (simp add: basis_prj_basis_emb) - apply (rule cb_take_less) - apply (simp add: basis_prj_node) - apply (case_tac "node i x A \ range (basis_emb :: 'a compact_basis \ nat)") - apply (erule rangeE, rename_tac a) - apply (case_tac "a = compact_bot", simp) - apply (simp add: basis_prj_basis_emb) - apply (simp add: basis_emb.simps) - apply (clarsimp simp add: fin2) - apply (case_tac "rank a", simp add: basis_prj_basis_emb) - apply (simp add: basis_prj_basis_emb) - apply (simp add: basis_prj_node) +lemma node_eq_basis_emb_iff: + "finite S \ node i a S = basis_emb x \ + x \ compact_bot \ i = place x \ a = basis_emb (sub x) \ + S = basis_emb ` {y. place y < place x \ x \ y}" +apply (cases "x = compact_bot", simp) +apply (simp add: basis_emb.simps [of x]) +apply (simp add: fin2) done +lemma basis_prj_mono: "ubasis_le a b \ basis_prj a \ basis_prj b" +proof (induct a b rule: ubasis_le.induct) + case (ubasis_le_refl a) show ?case by (rule refl_less) +next + case (ubasis_le_trans a b c) thus ?case by - (rule trans_less) +next + case (ubasis_le_lower S a i) thus ?case + apply (case_tac "node i a S \ range (basis_emb :: 'a compact_basis \ nat)") + apply (erule rangeE, rename_tac x) + apply (simp add: basis_prj_basis_emb) + apply (simp add: node_eq_basis_emb_iff) + apply (simp add: basis_prj_basis_emb) + apply (rule sub_below) + apply (simp add: basis_prj_node) + done +next + case (ubasis_le_upper S b a i) thus ?case + apply (case_tac "node i a S \ range (basis_emb :: 'a compact_basis \ nat)") + apply (erule rangeE, rename_tac x) + apply (simp add: basis_prj_basis_emb) + apply (clarsimp simp add: node_eq_basis_emb_iff) + apply (simp add: basis_prj_basis_emb) + apply (simp add: basis_prj_node) + done +qed + lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" unfolding basis_prj_def apply (subst f_inv_f [where f=basis_emb]) @@ -806,7 +812,8 @@ node choose choose_pos - reorder + place + sub subsubsection {* EP-pair from any bifinite domain into @{typ udom} *}