tuned proofs;
authorwenzelm
Sun Jun 03 23:30:53 2018 +0200 (13 months ago)
changeset 683696989752bba4b
parent 68368 b00b40dc41af
child 68370 bcdc47c9d4af
tuned proofs;
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Pcpo.thy
     1.1 --- a/src/HOL/HOLCF/Bifinite.thy	Sun Jun 03 22:18:27 2018 +0200
     1.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Sun Jun 03 23:30:53 2018 +0200
     1.3 @@ -112,18 +112,21 @@
     1.4  by (rule chainI, simp add: monofun_cfun monofun_LAM)
     1.5  
     1.6  lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
     1.7 -apply (rule cfun_eqI)
     1.8 -apply (simp add: contlub_cfun_fun)
     1.9 -apply (simp add: discr_approx_def)
    1.10 -apply (case_tac x, simp)
    1.11 -apply (rule lub_eqI)
    1.12 -apply (rule is_lubI)
    1.13 -apply (rule ub_rangeI, simp)
    1.14 -apply (drule ub_rangeD)
    1.15 -apply (erule rev_below_trans)
    1.16 -apply simp
    1.17 -apply (rule lessI)
    1.18 -done
    1.19 +  apply (rule cfun_eqI)
    1.20 +  apply (simp add: contlub_cfun_fun)
    1.21 +  apply (simp add: discr_approx_def)
    1.22 +  subgoal for x
    1.23 +    apply (cases x)
    1.24 +     apply simp
    1.25 +    apply (rule lub_eqI)
    1.26 +    apply (rule is_lubI)
    1.27 +     apply (rule ub_rangeI, simp)
    1.28 +    apply (drule ub_rangeD)
    1.29 +    apply (erule rev_below_trans)
    1.30 +    apply simp
    1.31 +    apply (rule lessI)
    1.32 +    done
    1.33 +  done
    1.34  
    1.35  lemma inj_on_undiscr [simp]: "inj_on undiscr A"
    1.36  using Discr_undiscr by (rule inj_on_inverseI)
    1.37 @@ -203,14 +206,21 @@
    1.38  definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
    1.39  
    1.40  lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
    1.41 -unfolding encode_prod_u_def decode_prod_u_def
    1.42 -by (case_tac x, simp, rename_tac y, case_tac y, simp)
    1.43 +  unfolding encode_prod_u_def decode_prod_u_def
    1.44 +  apply (cases x)
    1.45 +   apply simp
    1.46 +  subgoal for y by (cases y) simp
    1.47 +  done
    1.48  
    1.49  lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
    1.50 -unfolding encode_prod_u_def decode_prod_u_def
    1.51 -apply (case_tac y, simp, rename_tac a b)
    1.52 -apply (case_tac a, simp, case_tac b, simp, simp)
    1.53 -done
    1.54 +  unfolding encode_prod_u_def decode_prod_u_def
    1.55 +  apply (cases y)
    1.56 +   apply simp
    1.57 +  subgoal for a b
    1.58 +    apply (cases a, simp)
    1.59 +    apply (cases b, simp, simp)
    1.60 +    done
    1.61 +  done
    1.62  
    1.63  instance prod :: (profinite, profinite) profinite
    1.64  proof
     2.1 --- a/src/HOL/HOLCF/Pcpo.thy	Sun Jun 03 22:18:27 2018 +0200
     2.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Sun Jun 03 23:30:53 2018 +0200
     2.3 @@ -198,16 +198,20 @@
     2.4  begin
     2.5  
     2.6  subclass chfin
     2.7 -  apply standard
     2.8 -  apply (unfold max_in_chain_def)
     2.9 -  apply (case_tac "\<forall>i. Y i = \<bottom>")
    2.10 -   apply simp
    2.11 -  apply simp
    2.12 -  apply (erule exE)
    2.13 -  apply (rule_tac x="i" in exI)
    2.14 -  apply clarify
    2.15 -  apply (blast dest: chain_mono ax_flat)
    2.16 -  done
    2.17 +proof
    2.18 +  fix Y
    2.19 +  assume *: "chain Y"
    2.20 +  show "\<exists>n. max_in_chain n Y"
    2.21 +    apply (unfold max_in_chain_def)
    2.22 +    apply (cases "\<forall>i. Y i = \<bottom>")
    2.23 +     apply simp
    2.24 +    apply simp
    2.25 +    apply (erule exE)
    2.26 +    apply (rule_tac x="i" in exI)
    2.27 +    apply clarify
    2.28 +    using * apply (blast dest: chain_mono ax_flat)
    2.29 +    done
    2.30 +qed
    2.31  
    2.32  lemma flat_below_iff: "x \<sqsubseteq> y \<longleftrightarrow> x = \<bottom> \<or> x = y"
    2.33    by (safe dest!: ax_flat)