src/HOL/Hoare_Parallel/RG_Tran.thy
changeset 41842 d8f76db6a207
parent 35416 d8d7d1b785af
child 42174 d0be2722ce9f
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Fri Feb 25 08:46:52 2011 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Fri Feb 25 14:25:41 2011 +0100
     1.3 @@ -130,8 +130,6 @@
     1.4  lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
     1.5  apply simp
     1.6  apply(induct xs,simp+)
     1.7 -apply(case_tac xs)
     1.8 -apply simp_all
     1.9  done
    1.10  
    1.11  lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
    1.12 @@ -304,10 +302,10 @@
    1.13         apply(erule CptnEnv)
    1.14        apply(erule CptnComp,simp)
    1.15       apply(rule CptnComp)
    1.16 -     apply(erule CondT,simp)
    1.17 +      apply(erule CondT,simp)
    1.18      apply(rule CptnComp)
    1.19 -    apply(erule CondF,simp)
    1.20 ---{* Seq1 *}   
    1.21 +     apply(erule CondF,simp)
    1.22 +--{* Seq1 *}
    1.23  apply(erule cptn.cases,simp_all)
    1.24    apply(rule CptnOne)
    1.25   apply clarify
    1.26 @@ -332,37 +330,27 @@
    1.27    apply(drule_tac P=P1 in lift_is_cptn)
    1.28    apply(simp add:lift_def)
    1.29   apply simp
    1.30 -apply(case_tac "xs\<noteq>[]")
    1.31 - apply(drule_tac P=P1 in last_lift)
    1.32 -  apply(rule last_fst_esp)
    1.33 -  apply (simp add:last_length)
    1.34 - apply(simp add:Cons_lift del:map.simps)
    1.35 - apply(rule conjI, clarify, simp)
    1.36 - apply(case_tac "(((Some P0, s) # xs) ! length xs)")
    1.37 - apply clarify
    1.38 - apply (simp add:lift_def last_length)
    1.39 -apply (simp add:last_length)
    1.40 +apply(simp split: split_if_asm)
    1.41 +apply(frule_tac P=P1 in last_lift)
    1.42 + apply(rule last_fst_esp)
    1.43 + apply (simp add:last_length)
    1.44 +apply(simp add:Cons_lift lift_def split_def last_conv_nth)
    1.45  --{* While1 *}
    1.46  apply(rule CptnComp)
    1.47 -apply(rule WhileT,simp)
    1.48 + apply(rule WhileT,simp)
    1.49  apply(drule_tac P="While b P" in lift_is_cptn)
    1.50  apply(simp add:lift_def)
    1.51  --{* While2 *}
    1.52  apply(rule CptnComp)
    1.53 -apply(rule WhileT,simp)
    1.54 + apply(rule WhileT,simp)
    1.55  apply(rule cptn_append_is_cptn)
    1.56 -apply(drule_tac P="While b P" in lift_is_cptn)
    1.57 +  apply(drule_tac P="While b P" in lift_is_cptn)
    1.58    apply(simp add:lift_def)
    1.59   apply simp
    1.60 -apply(case_tac "xs\<noteq>[]")
    1.61 - apply(drule_tac P="While b P" in last_lift)
    1.62 -  apply(rule last_fst_esp,simp add:last_length)
    1.63 - apply(simp add:Cons_lift del:map.simps)
    1.64 - apply(rule conjI, clarify, simp)
    1.65 - apply(case_tac "(((Some P, s) # xs) ! length xs)")
    1.66 - apply clarify
    1.67 - apply (simp add:last_length lift_def)
    1.68 -apply simp
    1.69 +apply(simp split: split_if_asm)
    1.70 +apply(frule_tac P="While b P" in last_lift)
    1.71 + apply(rule last_fst_esp,simp add:last_length)
    1.72 +apply(simp add:Cons_lift lift_def split_def last_conv_nth)
    1.73  done
    1.74  
    1.75  theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)"