# HG changeset patch # User huffman # Date 1292949819 28800 # Node ID 17b09240893cb3046f6914c171500bd6ef6d135b # Parent 177f91b9f8e70fb64c44979c00c31ea5e7c0473c declare more simp rules, rewrite proofs in Isar-style diff -r 177f91b9f8e7 -r 17b09240893c src/HOL/HOLCF/Bifinite.thy --- a/src/HOL/HOLCF/Bifinite.thy Tue Dec 21 16:41:31 2010 +0100 +++ b/src/HOL/HOLCF/Bifinite.thy Tue Dec 21 08:43:39 2010 -0800 @@ -33,7 +33,7 @@ apply (rule finite_deflation_approx) done -lemma compact_approx: "compact (approx n\x)" +lemma compact_approx [simp]: "compact (approx n\x)" apply (rule finite_deflation.compact) apply (rule finite_deflation_approx) done diff -r 177f91b9f8e7 -r 17b09240893c src/HOL/HOLCF/Universal.thy --- a/src/HOL/HOLCF/Universal.thy Tue Dec 21 16:41:31 2010 +0100 +++ b/src/HOL/HOLCF/Universal.thy Tue Dec 21 08:43:39 2010 -0800 @@ -250,9 +250,13 @@ typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}" by auto -lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)" +lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)" by (rule Rep_compact_basis [unfolded mem_Collect_eq]) +lemma Abs_compact_basis_inverse' [simp]: + "compact x \ Rep_compact_basis (Abs_compact_basis x) = x" +by (rule Abs_compact_basis_inverse [unfolded mem_Collect_eq]) + instantiation compact_basis :: (pcpo) below begin @@ -276,7 +280,7 @@ "compact_bot = Abs_compact_basis \" lemma Rep_compact_bot [simp]: "Rep_compact_basis compact_bot = \" -unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) +unfolding compact_bot_def by simp lemma compact_bot_minimal [simp]: "compact_bot \ a" unfolding compact_le_def Rep_compact_bot by simp @@ -419,7 +423,7 @@ lemma Rep_cb_take: "Rep_compact_basis (cb_take (Suc n) a) = approx n\(Rep_compact_basis a)" -by (simp add: Abs_compact_basis_inverse cb_take.simps(2) compact_approx) +by (simp add: cb_take.simps(2)) lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric] @@ -428,7 +432,7 @@ apply (simp add: Rep_compact_basis_inject [symmetric]) apply (simp add: Rep_cb_take) apply (rule compact_eq_approx) -apply (rule compact_Rep_compact_basis) +apply (rule Rep_compact_basis') done lemma cb_take_less: "cb_take n x \ x" @@ -783,61 +787,49 @@ fix w :: "'a" show "below.ideal (approximants w)" proof (rule below.idealI) - show "\x. x \ approximants w" - unfolding approximants_def - apply (rule_tac x="Abs_compact_basis (approx 0\w)" in exI) - apply (simp add: Abs_compact_basis_inverse approx_below compact_approx) - done + have "Abs_compact_basis (approx 0\w) \ approximants w" + by (simp add: approximants_def approx_below) + thus "\x. x \ approximants w" .. next fix x y :: "'a compact_basis" - assume "x \ approximants w" "y \ approximants w" - thus "\z \ approximants w. x \ z \ y \ z" - unfolding approximants_def - apply simp - apply (cut_tac a=x in compact_Rep_compact_basis) - apply (cut_tac a=y in compact_Rep_compact_basis) - apply (drule compact_eq_approx) - apply (drule compact_eq_approx) - apply (clarify, rename_tac i j) - apply (rule_tac x="Abs_compact_basis (approx (max i j)\w)" in exI) - apply (simp add: compact_le_def) - apply (simp add: Abs_compact_basis_inverse approx_below compact_approx) - apply (erule subst, erule subst) - apply (simp add: monofun_cfun chain_mono [OF chain_approx]) - done + assume x: "x \ approximants w" and y: "y \ approximants w" + obtain i where i: "approx i\(Rep_compact_basis x) = Rep_compact_basis x" + using compact_eq_approx Rep_compact_basis' by fast + obtain j where j: "approx j\(Rep_compact_basis y) = Rep_compact_basis y" + using compact_eq_approx Rep_compact_basis' by fast + let ?z = "Abs_compact_basis (approx (max i j)\w)" + have "?z \ approximants w" + by (simp add: approximants_def approx_below) + moreover from x y have "x \ ?z \ y \ ?z" + by (simp add: approximants_def compact_le_def) + (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2) + ultimately show "\z \ approximants w. x \ z \ y \ z" .. next fix x y :: "'a compact_basis" assume "x \ y" "y \ approximants w" thus "x \ approximants w" - unfolding approximants_def - apply simp - apply (simp add: compact_le_def) - apply (erule (1) below_trans) - done + unfolding approximants_def compact_le_def + by (auto elim: below_trans) qed next fix Y :: "nat \ 'a" - assume Y: "chain Y" - show "approximants (\i. Y i) = (\i. approximants (Y i))" + assume "chain Y" + thus "approximants (\i. Y i) = (\i. approximants (Y i))" unfolding approximants_def - apply safe - apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) - apply (erule below_lub [OF Y]) - done + by (auto simp add: compact_below_lub_iff) next fix a :: "'a compact_basis" show "approximants (Rep_compact_basis a) = {b. b \ a}" unfolding approximants_def compact_le_def .. next fix x y :: "'a" - assume "approximants x \ approximants y" thus "x \ y" - apply (subgoal_tac "(\i. approx i\x) \ y") - apply (simp add: lub_distribs) - apply (rule admD, simp, simp) - apply (drule_tac c="Abs_compact_basis (approx i\x)" in subsetD) - apply (simp add: approximants_def Abs_compact_basis_inverse - approx_below compact_approx) - apply (simp add: approximants_def Abs_compact_basis_inverse compact_approx) - done + assume "approximants x \ approximants y" + hence "\z. compact z \ z \ x \ z \ y" + by (simp add: approximants_def subset_eq) + (metis Abs_compact_basis_inverse') + hence "(\i. approx i\x) \ y" + by (simp add: lub_below approx_below) + thus "x \ y" + by (simp add: lub_distribs) next show "\f::'a compact_basis \ nat. inj f" by (rule exI, rule inj_place)