tuned proofs;
authorwenzelm
Sat Jun 02 22:40:03 2018 +0200 (16 months ago)
changeset 68358e761afd35baa
parent 68357 6bf71e776226
child 68360 0f19c98fa7be
child 68362 27237ee2e889
tuned proofs;
src/HOL/HOLCF/Map_Functions.thy
     1.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Sat Jun 02 22:39:45 2018 +0200
     1.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Sat Jun 02 22:40:03 2018 +0200
     1.3 @@ -188,14 +188,14 @@
     1.4  
     1.5  lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
     1.6    apply standard
     1.7 -  subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse)
     1.8 -  subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below)
     1.9 +  subgoal for x by (cases x) (simp_all add: ep_pair.e_inverse)
    1.10 +  subgoal for y by (cases y) (simp_all add: ep_pair.e_p_below)
    1.11    done
    1.12  
    1.13  lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
    1.14    apply standard
    1.15 -  subgoal for x by (cases x, simp, simp add: deflation.idem)
    1.16 -  subgoal for x by (cases x, simp, simp add: deflation.below)
    1.17 +  subgoal for x by (cases x) (simp_all add: deflation.idem)
    1.18 +  subgoal for x by (cases x) (simp_all add: deflation.below)
    1.19    done
    1.20  
    1.21  lemma finite_deflation_u_map:
    1.22 @@ -235,12 +235,17 @@
    1.23    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    1.24      sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.25       sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.26 -  apply (induct p)
    1.27 -   apply simp
    1.28 -  apply (case_tac "f2\<cdot>x = \<bottom>", simp)
    1.29 -  apply (case_tac "g2\<cdot>y = \<bottom>", simp)
    1.30 -  apply simp
    1.31 -  done
    1.32 +proof (induct p)
    1.33 +  case bottom
    1.34 +  then show ?case by simp
    1.35 +next
    1.36 +  case (spair x y)
    1.37 +  then show ?case
    1.38 +    apply (cases "f2\<cdot>x = \<bottom>", simp)
    1.39 +    apply (cases "g2\<cdot>y = \<bottom>", simp)
    1.40 +    apply simp
    1.41 +    done
    1.42 +qed
    1.43  
    1.44  lemma ep_pair_sprod_map:
    1.45    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.46 @@ -251,11 +256,17 @@
    1.47    show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
    1.48      by (induct x) simp_all
    1.49    show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
    1.50 -    apply (induct y)
    1.51 -     apply simp
    1.52 -    apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
    1.53 -    apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
    1.54 -    done
    1.55 +  proof (induct y)
    1.56 +    case bottom
    1.57 +    then show ?case by simp
    1.58 +  next
    1.59 +    case (spair x y)
    1.60 +    then show ?case
    1.61 +      apply simp
    1.62 +      apply (cases "p1\<cdot>x = \<bottom>", simp, cases "p2\<cdot>y = \<bottom>", simp)
    1.63 +      apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
    1.64 +      done
    1.65 +  qed
    1.66  qed
    1.67  
    1.68  lemma deflation_sprod_map:
    1.69 @@ -266,14 +277,24 @@
    1.70    interpret d2: deflation d2 by fact
    1.71    fix x
    1.72    show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    1.73 -    apply (induct x, simp)
    1.74 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
    1.75 -    apply (simp add: d1.idem d2.idem)
    1.76 -    done
    1.77 +  proof (induct x)
    1.78 +    case bottom
    1.79 +    then show ?case by simp
    1.80 +  next
    1.81 +    case (spair x y)
    1.82 +    then show ?case
    1.83 +      apply (cases "d1\<cdot>x = \<bottom>", simp, cases "d2\<cdot>y = \<bottom>", simp)
    1.84 +      apply (simp add: d1.idem d2.idem)
    1.85 +      done
    1.86 +  qed
    1.87    show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    1.88 -    apply (induct x, simp)
    1.89 -    apply (simp add: monofun_cfun d1.below d2.below)
    1.90 -    done
    1.91 +  proof (induct x)
    1.92 +    case bottom
    1.93 +    then show ?case by simp
    1.94 +  next
    1.95 +    case spair
    1.96 +    then show ?case by (simp add: monofun_cfun d1.below d2.below)
    1.97 +  qed
    1.98  qed
    1.99  
   1.100  lemma finite_deflation_sprod_map:
   1.101 @@ -319,11 +340,16 @@
   1.102    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
   1.103      ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
   1.104       ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   1.105 -  apply (induct p)
   1.106 -    apply simp
   1.107 -   apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
   1.108 -  apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
   1.109 -  done
   1.110 +proof (induct p)
   1.111 +  case bottom
   1.112 +  then show ?case by simp
   1.113 +next
   1.114 +  case (sinl x)
   1.115 +  then show ?case by (cases "f2\<cdot>x = \<bottom>") simp_all
   1.116 +next
   1.117 +  case (sinr y)
   1.118 +  then show ?case by (cases "g2\<cdot>y = \<bottom>") simp_all
   1.119 +qed
   1.120  
   1.121  lemma ep_pair_ssum_map:
   1.122    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   1.123 @@ -334,11 +360,16 @@
   1.124    show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
   1.125      by (induct x) simp_all
   1.126    show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
   1.127 -    apply (induct y)
   1.128 -      apply simp
   1.129 -     apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
   1.130 -    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
   1.131 -    done
   1.132 +  proof (induct y)
   1.133 +    case bottom
   1.134 +    then show ?case by simp
   1.135 +  next
   1.136 +    case (sinl x)
   1.137 +    then show ?case by (cases "p1\<cdot>x = \<bottom>") (simp_all add: e1p1.e_p_below)
   1.138 +  next
   1.139 +    case (sinr y)
   1.140 +    then show ?case by (cases "p2\<cdot>y = \<bottom>") (simp_all add: e2p2.e_p_below)
   1.141 +  qed
   1.142  qed
   1.143  
   1.144  lemma deflation_ssum_map:
   1.145 @@ -349,15 +380,27 @@
   1.146    interpret d2: deflation d2 by fact
   1.147    fix x
   1.148    show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
   1.149 -    apply (induct x, simp)
   1.150 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
   1.151 -    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
   1.152 -    done
   1.153 +  proof (induct x)
   1.154 +    case bottom
   1.155 +    then show ?case by simp
   1.156 +  next
   1.157 +    case (sinl x)
   1.158 +    then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.idem)
   1.159 +  next
   1.160 +    case (sinr y)
   1.161 +    then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.idem)
   1.162 +  qed
   1.163    show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   1.164 -    apply (induct x, simp)
   1.165 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
   1.166 -    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
   1.167 -    done
   1.168 +  proof (induct x)
   1.169 +    case bottom
   1.170 +    then show ?case by simp
   1.171 +  next
   1.172 +    case (sinl x)
   1.173 +    then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.below)
   1.174 +  next
   1.175 +    case (sinr y)
   1.176 +    then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.below)
   1.177 +  qed
   1.178  qed
   1.179  
   1.180  lemma finite_deflation_ssum_map: