tuned proofs;
authorwenzelm
Tue Jun 05 18:08:13 2018 +0200 (11 months ago)
changeset 6838393a42bd62ede
parent 68382 b10ae73f0bab
child 68384 4a3fc3420747
tuned proofs;
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/Domain_Aux.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Jun 05 18:08:13 2018 +0200
     1.3 @@ -394,7 +394,7 @@
     1.4  
     1.5  lemma flat_codom: "f\<cdot>x = c \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
     1.6    for c :: "'b::flat"
     1.7 -  apply (case_tac "f\<cdot>x = \<bottom>")
     1.8 +  apply (cases "f\<cdot>x = \<bottom>")
     1.9     apply (rule disjI1)
    1.10     apply (rule bottomI)
    1.11     apply (erule_tac t="\<bottom>" in subst)
     2.1 --- a/src/HOL/HOLCF/Completion.thy	Tue Jun 05 16:35:52 2018 +0200
     2.2 +++ b/src/HOL/HOLCF/Completion.thy	Tue Jun 05 18:08:13 2018 +0200
     2.3 @@ -41,13 +41,13 @@
     2.4  unfolding ideal_def by fast
     2.5  
     2.6  lemma ideal_principal: "ideal {x. x \<preceq> z}"
     2.7 -apply (rule idealI)
     2.8 -apply (rule_tac x=z in exI)
     2.9 -apply (fast intro: r_refl)
    2.10 -apply (rule_tac x=z in bexI, fast)
    2.11 -apply (fast intro: r_refl)
    2.12 -apply (fast intro: r_trans)
    2.13 -done
    2.14 +  apply (rule idealI)
    2.15 +    apply (rule exI [where x = z])
    2.16 +    apply (fast intro: r_refl)
    2.17 +   apply (rule bexI [where x = z], fast)
    2.18 +   apply (fast intro: r_refl)
    2.19 +  apply (fast intro: r_trans)
    2.20 +  done
    2.21  
    2.22  lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
    2.23  by (fast intro: ideal_principal)
    2.24 @@ -59,17 +59,19 @@
    2.25    assumes ideal_A: "\<And>i. ideal (A i)"
    2.26    assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j"
    2.27    shows "ideal (\<Union>i. A i)"
    2.28 - apply (rule idealI)
    2.29 -   apply (cut_tac idealD1 [OF ideal_A], fast)
    2.30 -  apply (clarify, rename_tac i j)
    2.31 -  apply (drule subsetD [OF chain_A [OF max.cobounded1]])
    2.32 -  apply (drule subsetD [OF chain_A [OF max.cobounded2]])
    2.33 -  apply (drule (1) idealD2 [OF ideal_A])
    2.34 -  apply blast
    2.35 - apply clarify
    2.36 - apply (drule (1) idealD3 [OF ideal_A])
    2.37 - apply fast
    2.38 -done
    2.39 +  apply (rule idealI)
    2.40 +  using idealD1 [OF ideal_A] apply fast
    2.41 +   apply (clarify)
    2.42 +  subgoal for i j
    2.43 +    apply (drule subsetD [OF chain_A [OF max.cobounded1]])
    2.44 +    apply (drule subsetD [OF chain_A [OF max.cobounded2]])
    2.45 +    apply (drule (1) idealD2 [OF ideal_A])
    2.46 +    apply blast
    2.47 +    done
    2.48 +  apply clarify
    2.49 +  apply (drule (1) idealD3 [OF ideal_A])
    2.50 +  apply fast
    2.51 +  done
    2.52  
    2.53  lemma typedef_ideal_po:
    2.54    fixes Abs :: "'a set \<Rightarrow> 'b::below"
    2.55 @@ -208,10 +210,10 @@
    2.56    have a_mem: "enum a \<in> rep x"
    2.57      unfolding a_def
    2.58      apply (rule LeastI_ex)
    2.59 -    apply (cut_tac ideal_rep [of x])
    2.60 +    apply (insert ideal_rep [of x])
    2.61      apply (drule idealD1)
    2.62 -    apply (clarify, rename_tac a)
    2.63 -    apply (rule_tac x="count a" in exI, simp)
    2.64 +    apply (clarify)
    2.65 +    subgoal for a by (rule exI [where x="count a"]) simp
    2.66      done
    2.67    have b: "\<And>i. P i \<Longrightarrow> enum i \<in> rep x
    2.68      \<Longrightarrow> enum (b i) \<in> rep x \<and> \<not> enum (b i) \<preceq> enum i"
    2.69 @@ -220,50 +222,63 @@
    2.70      \<Longrightarrow> enum (c i j) \<in> rep x \<and> enum i \<preceq> enum (c i j) \<and> enum j \<preceq> enum (c i j)"
    2.71      unfolding c_def
    2.72      apply (drule (1) idealD2 [OF ideal_rep], clarify)
    2.73 -    apply (rule_tac a="count z" in LeastI2, simp, simp)
    2.74 +    subgoal for \<dots> z by (rule LeastI2 [where a="count z"], simp, simp)
    2.75      done
    2.76 -  have X_mem: "\<And>n. enum (X n) \<in> rep x"
    2.77 -    apply (induct_tac n)
    2.78 -    apply (simp add: X_0 a_mem)
    2.79 -    apply (clarsimp simp add: X_Suc, rename_tac n)
    2.80 -    apply (simp add: b c)
    2.81 -    done
    2.82 +  have X_mem: "enum (X n) \<in> rep x" for n
    2.83 +  proof (induct n)
    2.84 +    case 0
    2.85 +    then show ?case by (simp add: X_0 a_mem)
    2.86 +  next
    2.87 +    case (Suc n)
    2.88 +    with b c show ?case by (auto simp: X_Suc)
    2.89 +  qed
    2.90    have X_chain: "\<And>n. enum (X n) \<preceq> enum (X (Suc n))"
    2.91      apply (clarsimp simp add: X_Suc r_refl)
    2.92      apply (simp add: b c X_mem)
    2.93      done
    2.94    have less_b: "\<And>n i. n < b i \<Longrightarrow> enum n \<in> rep x \<Longrightarrow> enum n \<preceq> enum i"
    2.95      unfolding b_def by (drule not_less_Least, simp)
    2.96 -  have X_covers: "\<And>n. \<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)"
    2.97 -    apply (induct_tac n)
    2.98 -    apply (clarsimp simp add: X_0 a_def)
    2.99 -    apply (drule_tac k=0 in Least_le, simp add: r_refl)
   2.100 -    apply (clarsimp, rename_tac n k)
   2.101 -    apply (erule le_SucE)
   2.102 -    apply (rule r_trans [OF _ X_chain], simp)
   2.103 -    apply (case_tac "P (X n)", simp add: X_Suc)
   2.104 -    apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases)
   2.105 -    apply (simp only: less_Suc_eq_le)
   2.106 -    apply (drule spec, drule (1) mp, simp add: b X_mem)
   2.107 -    apply (simp add: c X_mem)
   2.108 -    apply (drule (1) less_b)
   2.109 -    apply (erule r_trans)
   2.110 -    apply (simp add: b c X_mem)
   2.111 -    apply (simp add: X_Suc)
   2.112 -    apply (simp add: P_def)
   2.113 -    done
   2.114 +  have X_covers: "\<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)" for n
   2.115 +  proof (induct n)
   2.116 +    case 0
   2.117 +    then show ?case
   2.118 +      apply (clarsimp simp add: X_0 a_def)
   2.119 +      apply (drule Least_le [where k=0], simp add: r_refl)
   2.120 +      done
   2.121 +  next
   2.122 +    case (Suc n)
   2.123 +    then show ?case
   2.124 +      apply clarsimp
   2.125 +      apply (erule le_SucE)
   2.126 +       apply (rule r_trans [OF _ X_chain], simp)
   2.127 +      apply (cases "P (X n)", simp add: X_Suc)
   2.128 +       apply (rule linorder_cases [where x="b (X n)" and y="Suc n"])
   2.129 +         apply (simp only: less_Suc_eq_le)
   2.130 +         apply (drule spec, drule (1) mp, simp add: b X_mem)
   2.131 +        apply (simp add: c X_mem)
   2.132 +       apply (drule (1) less_b)
   2.133 +       apply (erule r_trans)
   2.134 +       apply (simp add: b c X_mem)
   2.135 +      apply (simp add: X_Suc)
   2.136 +      apply (simp add: P_def)
   2.137 +      done
   2.138 +  qed
   2.139    have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))"
   2.140      by (simp add: X_chain)
   2.141 -  have 2: "x = (\<Squnion>n. principal (enum (X n)))"
   2.142 +  have "x = (\<Squnion>n. principal (enum (X n)))"
   2.143      apply (simp add: eq_iff rep_lub 1 rep_principal)
   2.144 -    apply (auto, rename_tac a)
   2.145 -    apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
   2.146 -    apply (rule_tac x=i in exI, simp add: X_covers)
   2.147 -    apply (rule_tac x="count a" in exI, simp)
   2.148 -    apply (erule idealD3 [OF ideal_rep])
   2.149 -    apply (rule X_mem)
   2.150 +    apply auto
   2.151 +    subgoal for a
   2.152 +      apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
   2.153 +       apply (rule_tac x=i in exI, simp add: X_covers)
   2.154 +      apply (rule_tac x="count a" in exI, simp)
   2.155 +      done
   2.156 +    subgoal
   2.157 +      apply (erule idealD3 [OF ideal_rep])
   2.158 +      apply (rule X_mem)
   2.159 +      done
   2.160      done
   2.161 -  from 1 2 show ?thesis ..
   2.162 +  with 1 show ?thesis ..
   2.163  qed
   2.164  
   2.165  lemma principal_induct:
   2.166 @@ -301,16 +316,20 @@
   2.167      by (simp add: x rep_lub Y rep_principal)
   2.168    have "f ` rep x <<| (\<Squnion>n. f (Y n))"
   2.169      apply (rule is_lubI)
   2.170 -    apply (rule ub_imageI, rename_tac a)
   2.171 -    apply (clarsimp simp add: rep_x)
   2.172 -    apply (drule f_mono)
   2.173 -    apply (erule below_lub [OF chain])
   2.174 +     apply (rule ub_imageI)
   2.175 +    subgoal for a
   2.176 +      apply (clarsimp simp add: rep_x)
   2.177 +      apply (drule f_mono)
   2.178 +      apply (erule below_lub [OF chain])
   2.179 +      done
   2.180      apply (rule lub_below [OF chain])
   2.181 -    apply (drule_tac x="Y n" in ub_imageD)
   2.182 -    apply (simp add: rep_x, fast intro: r_refl)
   2.183 -    apply assumption
   2.184 +    subgoal for \<dots> n
   2.185 +      apply (drule ub_imageD [where x="Y n"])
   2.186 +       apply (simp add: rep_x, fast intro: r_refl)
   2.187 +      apply assumption
   2.188 +      done
   2.189      done
   2.190 -  thus ?thesis ..
   2.191 +  then show ?thesis ..
   2.192  qed
   2.193  
   2.194  lemma extension_beta:
   2.195 @@ -353,16 +372,18 @@
   2.196    assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
   2.197    assumes below: "\<And>a. f a \<sqsubseteq> g a"
   2.198    shows "extension f \<sqsubseteq> extension g"
   2.199 - apply (rule cfun_belowI)
   2.200 - apply (simp only: extension_beta f_mono g_mono)
   2.201 - apply (rule is_lub_thelub_ex)
   2.202 -  apply (rule extension_lemma, erule f_mono)
   2.203 - apply (rule ub_imageI, rename_tac a)
   2.204 - apply (rule below_trans [OF below])
   2.205 - apply (rule is_ub_thelub_ex)
   2.206 -  apply (rule extension_lemma, erule g_mono)
   2.207 - apply (erule imageI)
   2.208 -done
   2.209 +  apply (rule cfun_belowI)
   2.210 +  apply (simp only: extension_beta f_mono g_mono)
   2.211 +  apply (rule is_lub_thelub_ex)
   2.212 +   apply (rule extension_lemma, erule f_mono)
   2.213 +  apply (rule ub_imageI)
   2.214 +  subgoal for x a
   2.215 +    apply (rule below_trans [OF below])
   2.216 +    apply (rule is_ub_thelub_ex)
   2.217 +     apply (rule extension_lemma, erule g_mono)
   2.218 +    apply (erule imageI)
   2.219 +    done
   2.220 +  done
   2.221  
   2.222  lemma cont_extension:
   2.223    assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
     3.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Tue Jun 05 16:35:52 2018 +0200
     3.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Tue Jun 05 18:08:13 2018 +0200
     3.3 @@ -199,32 +199,40 @@
     3.4    assumes f: "decisive f"
     3.5    assumes g: "decisive g"
     3.6    shows "decisive (ssum_map\<cdot>f\<cdot>g)"
     3.7 -apply (rule decisiveI, rename_tac s)
     3.8 -apply (case_tac s, simp_all)
     3.9 -apply (rule_tac x=x in decisive_cases [OF f], simp_all)
    3.10 -apply (rule_tac x=y in decisive_cases [OF g], simp_all)
    3.11 -done
    3.12 +  apply (rule decisiveI)
    3.13 +  subgoal for s
    3.14 +    apply (cases s, simp_all)
    3.15 +     apply (rule_tac x=x in decisive_cases [OF f], simp_all)
    3.16 +    apply (rule_tac x=y in decisive_cases [OF g], simp_all)
    3.17 +    done
    3.18 +  done
    3.19  
    3.20  lemma decisive_sprod_map:
    3.21    assumes f: "decisive f"
    3.22    assumes g: "decisive g"
    3.23    shows "decisive (sprod_map\<cdot>f\<cdot>g)"
    3.24 -apply (rule decisiveI, rename_tac s)
    3.25 -apply (case_tac s, simp_all)
    3.26 -apply (rule_tac x=x in decisive_cases [OF f], simp_all)
    3.27 -apply (rule_tac x=y in decisive_cases [OF g], simp_all)
    3.28 -done
    3.29 +  apply (rule decisiveI)
    3.30 +  subgoal for s
    3.31 +    apply (cases s, simp)
    3.32 +    subgoal for x y
    3.33 +      apply (rule decisive_cases [OF f, where x = x], simp_all)
    3.34 +      apply (rule decisive_cases [OF g, where x = y], simp_all)
    3.35 +      done
    3.36 +    done
    3.37 +  done
    3.38  
    3.39  lemma decisive_abs_rep:
    3.40    fixes abs rep
    3.41    assumes iso: "iso abs rep"
    3.42    assumes d: "decisive d"
    3.43    shows "decisive (abs oo d oo rep)"
    3.44 -apply (rule decisiveI)
    3.45 -apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
    3.46 -apply (simp add: iso.rep_iso [OF iso])
    3.47 -apply (simp add: iso.abs_strict [OF iso])
    3.48 -done
    3.49 +  apply (rule decisiveI)
    3.50 +  subgoal for s
    3.51 +    apply (rule decisive_cases [OF d, where x="rep\<cdot>s"])
    3.52 +     apply (simp add: iso.rep_iso [OF iso])
    3.53 +    apply (simp add: iso.abs_strict [OF iso])
    3.54 +    done
    3.55 +  done
    3.56  
    3.57  lemma lub_ID_finite:
    3.58    assumes chain: "chain d"