src/HOL/Hoare_Parallel/RG_Tran.thy
changeset 51119 6b2352111017
parent 42174 d0be2722ce9f
child 51120 4b3a062b6538
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Thu Feb 14 15:34:33 2013 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Thu Feb 14 16:17:36 2013 +0100
     1.3 @@ -128,9 +128,7 @@
     1.4  subsection {* Equivalence of Both Definitions.*}
     1.5  
     1.6  lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
     1.7 -apply simp
     1.8 -apply(induct xs,simp+)
     1.9 -done
    1.10 +  by (induct xs) auto
    1.11  
    1.12  lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
    1.13   (\<forall>s P Q zs. list=(Some (Seq P Q), s)#zs \<longrightarrow>
    1.14 @@ -261,13 +259,10 @@
    1.15  
    1.16  lemma last_lift: "\<lbrakk>xs\<noteq>[]; fst(xs!(length xs - (Suc 0)))=None\<rbrakk> 
    1.17   \<Longrightarrow> fst((map (lift P) xs)!(length (map (lift P) xs)- (Suc 0)))=(Some P)"
    1.18 -apply(case_tac "(xs ! (length xs - (Suc 0)))")
    1.19 -apply (simp add:lift_def)
    1.20 -done
    1.21 +  by (cases "(xs ! (length xs - (Suc 0)))") (simp add:lift_def)
    1.22  
    1.23  lemma last_fst [rule_format]: "P((a#x)!length x) \<longrightarrow> \<not>P a \<longrightarrow> P (x!(length x - (Suc 0)))" 
    1.24 -apply(induct x,simp+)
    1.25 -done
    1.26 +  by (induct x) simp_all
    1.27  
    1.28  lemma last_fst_esp: 
    1.29   "fst(((Some a,s)#xs)!(length xs))=None \<Longrightarrow> fst(xs!(length xs - (Suc 0)))=None" 
    1.30 @@ -277,24 +272,20 @@
    1.31  
    1.32  lemma last_snd: "xs\<noteq>[] \<Longrightarrow> 
    1.33    snd(((map (lift P) xs))!(length (map (lift P) xs) - (Suc 0)))=snd(xs!(length xs - (Suc 0)))"
    1.34 -apply(case_tac "(xs ! (length xs - (Suc 0)))",simp)
    1.35 -apply (simp add:lift_def)
    1.36 -done
    1.37 +  by (cases "(xs ! (length xs - (Suc 0)))") (simp_all add:lift_def)
    1.38  
    1.39  lemma Cons_lift: "(Some (Seq P Q), s) # (map (lift Q) xs) = map (lift Q) ((Some P, s) # xs)"
    1.40 -by(simp add:lift_def)
    1.41 +  by (simp add:lift_def)
    1.42  
    1.43  lemma Cons_lift_append: 
    1.44    "(Some (Seq P Q), s) # (map (lift Q) xs) @ ys = map (lift Q) ((Some P, s) # xs)@ ys "
    1.45 -by(simp add:lift_def)
    1.46 +  by (simp add:lift_def)
    1.47  
    1.48  lemma lift_nth: "i<length xs \<Longrightarrow> map (lift Q) xs ! i = lift Q  (xs! i)"
    1.49 -by (simp add:lift_def)
    1.50 +  by (simp add:lift_def)
    1.51  
    1.52  lemma snd_lift: "i< length xs \<Longrightarrow> snd(lift Q (xs ! i))= snd (xs ! i)"
    1.53 -apply(case_tac "xs!i")
    1.54 -apply(simp add:lift_def)
    1.55 -done
    1.56 +  by (cases "xs!i") (simp add:lift_def)
    1.57  
    1.58  lemma cptn_if_cptn_mod: "c \<in> cptn_mod \<Longrightarrow> c \<in> cptn"
    1.59  apply(erule cptn_mod.induct)
    1.60 @@ -425,10 +416,7 @@
    1.61  
    1.62  lemma list_eq_if [rule_format]: 
    1.63    "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
    1.64 -apply (induct xs)
    1.65 - apply simp
    1.66 -apply clarify
    1.67 -done
    1.68 +  by (induct xs) auto
    1.69  
    1.70  lemma list_eq: "(length xs = length ys \<and> (\<forall>i<length xs. xs!i=ys!i)) = (xs=ys)"
    1.71  apply(rule iffI)
    1.72 @@ -438,43 +426,25 @@
    1.73  done
    1.74  
    1.75  lemma nth_tl: "\<lbrakk> ys!0=a; ys\<noteq>[] \<rbrakk> \<Longrightarrow> ys=(a#(tl ys))"
    1.76 -apply(case_tac ys)
    1.77 - apply simp+
    1.78 -done
    1.79 +  by (cases ys) simp_all
    1.80  
    1.81  lemma nth_tl_if [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P ys \<longrightarrow> P (a#(tl ys))"
    1.82 -apply(induct ys)
    1.83 - apply simp+
    1.84 -done
    1.85 +  by (induct ys) simp_all
    1.86  
    1.87  lemma nth_tl_onlyif [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P (a#(tl ys)) \<longrightarrow> P ys"
    1.88 -apply(induct ys)
    1.89 - apply simp+
    1.90 -done
    1.91 +  by (induct ys) simp_all
    1.92  
    1.93  lemma seq_not_eq1: "Seq c1 c2\<noteq>c1"
    1.94 -apply(rule com.induct)
    1.95 -apply simp_all
    1.96 -apply clarify
    1.97 -done
    1.98 +  by (induct c1) auto
    1.99  
   1.100  lemma seq_not_eq2: "Seq c1 c2\<noteq>c2"
   1.101 -apply(rule com.induct)
   1.102 -apply simp_all
   1.103 -apply clarify
   1.104 -done
   1.105 +  by (induct c2) auto
   1.106  
   1.107  lemma if_not_eq1: "Cond b c1 c2 \<noteq>c1"
   1.108 -apply(rule com.induct)
   1.109 -apply simp_all
   1.110 -apply clarify
   1.111 -done
   1.112 +  by (induct c1) auto
   1.113  
   1.114  lemma if_not_eq2: "Cond b c1 c2\<noteq>c2"
   1.115 -apply(rule com.induct)
   1.116 -apply simp_all
   1.117 -apply clarify
   1.118 -done
   1.119 +  by (induct c2) auto
   1.120  
   1.121  lemmas seq_and_if_not_eq [simp] = seq_not_eq1 seq_not_eq2 
   1.122  seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] 
   1.123 @@ -507,14 +477,11 @@
   1.124  done
   1.125  
   1.126  lemma tl_in_cptn: "\<lbrakk> a#xs \<in>cptn; xs\<noteq>[] \<rbrakk> \<Longrightarrow> xs\<in>cptn"
   1.127 -apply(force elim:cptn.cases)
   1.128 -done
   1.129 +  by (force elim: cptn.cases)
   1.130  
   1.131  lemma tl_zero[rule_format]: 
   1.132    "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
   1.133 -apply(induct ys)
   1.134 - apply simp_all
   1.135 -done
   1.136 +  by (induct ys) simp_all
   1.137  
   1.138  subsection {* The Semantics is Compositional *}
   1.139