declare more simp rules, rewrite proofs in Isar-style
authorhuffman
Tue Dec 21 08:43:39 2010 -0800 (2010-12-21)
changeset 4137017b09240893c
parent 41369 177f91b9f8e7
child 41374 a35af5180c01
declare more simp rules, rewrite proofs in Isar-style
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Universal.thy
     1.1 --- a/src/HOL/HOLCF/Bifinite.thy	Tue Dec 21 16:41:31 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Tue Dec 21 08:43:39 2010 -0800
     1.3 @@ -33,7 +33,7 @@
     1.4  apply (rule finite_deflation_approx)
     1.5  done
     1.6  
     1.7 -lemma compact_approx: "compact (approx n\<cdot>x)"
     1.8 +lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
     1.9  apply (rule finite_deflation.compact)
    1.10  apply (rule finite_deflation_approx)
    1.11  done
     2.1 --- a/src/HOL/HOLCF/Universal.thy	Tue Dec 21 16:41:31 2010 +0100
     2.2 +++ b/src/HOL/HOLCF/Universal.thy	Tue Dec 21 08:43:39 2010 -0800
     2.3 @@ -250,9 +250,13 @@
     2.4  typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}"
     2.5  by auto
     2.6  
     2.7 -lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
     2.8 +lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)"
     2.9  by (rule Rep_compact_basis [unfolded mem_Collect_eq])
    2.10  
    2.11 +lemma Abs_compact_basis_inverse' [simp]:
    2.12 +   "compact x \<Longrightarrow> Rep_compact_basis (Abs_compact_basis x) = x"
    2.13 +by (rule Abs_compact_basis_inverse [unfolded mem_Collect_eq])
    2.14 +
    2.15  instantiation compact_basis :: (pcpo) below
    2.16  begin
    2.17  
    2.18 @@ -276,7 +280,7 @@
    2.19    "compact_bot = Abs_compact_basis \<bottom>"
    2.20  
    2.21  lemma Rep_compact_bot [simp]: "Rep_compact_basis compact_bot = \<bottom>"
    2.22 -unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
    2.23 +unfolding compact_bot_def by simp
    2.24  
    2.25  lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
    2.26  unfolding compact_le_def Rep_compact_bot by simp
    2.27 @@ -419,7 +423,7 @@
    2.28  
    2.29  lemma Rep_cb_take:
    2.30    "Rep_compact_basis (cb_take (Suc n) a) = approx n\<cdot>(Rep_compact_basis a)"
    2.31 -by (simp add: Abs_compact_basis_inverse cb_take.simps(2) compact_approx)
    2.32 +by (simp add: cb_take.simps(2))
    2.33  
    2.34  lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric]
    2.35  
    2.36 @@ -428,7 +432,7 @@
    2.37  apply (simp add: Rep_compact_basis_inject [symmetric])
    2.38  apply (simp add: Rep_cb_take)
    2.39  apply (rule compact_eq_approx)
    2.40 -apply (rule compact_Rep_compact_basis)
    2.41 +apply (rule Rep_compact_basis')
    2.42  done
    2.43  
    2.44  lemma cb_take_less: "cb_take n x \<sqsubseteq> x"
    2.45 @@ -783,61 +787,49 @@
    2.46    fix w :: "'a"
    2.47    show "below.ideal (approximants w)"
    2.48    proof (rule below.idealI)
    2.49 -    show "\<exists>x. x \<in> approximants w"
    2.50 -      unfolding approximants_def
    2.51 -      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
    2.52 -      apply (simp add: Abs_compact_basis_inverse approx_below compact_approx)
    2.53 -      done
    2.54 +    have "Abs_compact_basis (approx 0\<cdot>w) \<in> approximants w"
    2.55 +      by (simp add: approximants_def approx_below)
    2.56 +    thus "\<exists>x. x \<in> approximants w" ..
    2.57    next
    2.58      fix x y :: "'a compact_basis"
    2.59 -    assume "x \<in> approximants w" "y \<in> approximants w"
    2.60 -    thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    2.61 -      unfolding approximants_def
    2.62 -      apply simp
    2.63 -      apply (cut_tac a=x in compact_Rep_compact_basis)
    2.64 -      apply (cut_tac a=y in compact_Rep_compact_basis)
    2.65 -      apply (drule compact_eq_approx)
    2.66 -      apply (drule compact_eq_approx)
    2.67 -      apply (clarify, rename_tac i j)
    2.68 -      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
    2.69 -      apply (simp add: compact_le_def)
    2.70 -      apply (simp add: Abs_compact_basis_inverse approx_below compact_approx)
    2.71 -      apply (erule subst, erule subst)
    2.72 -      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
    2.73 -      done
    2.74 +    assume x: "x \<in> approximants w" and y: "y \<in> approximants w"
    2.75 +    obtain i where i: "approx i\<cdot>(Rep_compact_basis x) = Rep_compact_basis x"
    2.76 +      using compact_eq_approx Rep_compact_basis' by fast
    2.77 +    obtain j where j: "approx j\<cdot>(Rep_compact_basis y) = Rep_compact_basis y"
    2.78 +      using compact_eq_approx Rep_compact_basis' by fast
    2.79 +    let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)"
    2.80 +    have "?z \<in> approximants w"
    2.81 +      by (simp add: approximants_def approx_below)
    2.82 +    moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z"
    2.83 +      by (simp add: approximants_def compact_le_def)
    2.84 +         (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2)
    2.85 +    ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
    2.86    next
    2.87      fix x y :: "'a compact_basis"
    2.88      assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
    2.89 -      unfolding approximants_def
    2.90 -      apply simp
    2.91 -      apply (simp add: compact_le_def)
    2.92 -      apply (erule (1) below_trans)
    2.93 -      done
    2.94 +      unfolding approximants_def compact_le_def
    2.95 +      by (auto elim: below_trans)
    2.96    qed
    2.97  next
    2.98    fix Y :: "nat \<Rightarrow> 'a"
    2.99 -  assume Y: "chain Y"
   2.100 -  show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
   2.101 +  assume "chain Y"
   2.102 +  thus "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
   2.103      unfolding approximants_def
   2.104 -    apply safe
   2.105 -    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
   2.106 -    apply (erule below_lub [OF Y])
   2.107 -    done
   2.108 +    by (auto simp add: compact_below_lub_iff)
   2.109  next
   2.110    fix a :: "'a compact_basis"
   2.111    show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
   2.112      unfolding approximants_def compact_le_def ..
   2.113  next
   2.114    fix x y :: "'a"
   2.115 -  assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
   2.116 -    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y")
   2.117 -    apply (simp add: lub_distribs)
   2.118 -    apply (rule admD, simp, simp)
   2.119 -    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
   2.120 -    apply (simp add: approximants_def Abs_compact_basis_inverse
   2.121 -                     approx_below compact_approx)
   2.122 -    apply (simp add: approximants_def Abs_compact_basis_inverse compact_approx)
   2.123 -    done
   2.124 +  assume "approximants x \<subseteq> approximants y"
   2.125 +  hence "\<forall>z. compact z \<longrightarrow> z \<sqsubseteq> x \<longrightarrow> z \<sqsubseteq> y"
   2.126 +    by (simp add: approximants_def subset_eq)
   2.127 +       (metis Abs_compact_basis_inverse')
   2.128 +  hence "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y"
   2.129 +    by (simp add: lub_below approx_below)
   2.130 +  thus "x \<sqsubseteq> y"
   2.131 +    by (simp add: lub_distribs)
   2.132  next
   2.133    show "\<exists>f::'a compact_basis \<Rightarrow> nat. inj f"
   2.134      by (rule exI, rule inj_place)