author wenzelm Sat Jun 02 22:40:03 2018 +0200 (16 months ago) changeset 68358 e761afd35baa parent 68357 6bf71e776226 child 68360 0f19c98fa7be child 68362 27237ee2e889
tuned proofs;
```     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:
```