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