tuned proofs;
authorwenzelm
Sat Nov 12 21:10:56 2011 +0100 (2011-11-12)
changeset 4547711d9c2768729
parent 45476 6f9e24376ffd
child 45478 8e299034eab4
child 45480 a39bb6d42ace
tuned proofs;
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Project.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/UNITY/Guar.thy	Sat Nov 12 20:14:09 2011 +0100
     1.2 +++ b/src/HOL/UNITY/Guar.thy	Sat Nov 12 21:10:56 2011 +0100
     1.3 @@ -75,14 +75,14 @@
     1.4  
     1.5  subsection{*Existential Properties*}
     1.6  
     1.7 -lemma ex1 [rule_format]: 
     1.8 - "[| ex_prop X; finite GG |] ==>  
     1.9 -     GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
    1.10 -apply (unfold ex_prop_def)
    1.11 -apply (erule finite_induct)
    1.12 -apply (auto simp add: OK_insert_iff Int_insert_left)
    1.13 -done
    1.14 -
    1.15 +lemma ex1:
    1.16 +  assumes "ex_prop X" and "finite GG"
    1.17 +  shows "GG \<inter> X \<noteq> {} \<Longrightarrow> OK GG (%G. G) \<Longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X"
    1.18 +  apply (atomize (full))
    1.19 +  using assms(2) apply induct
    1.20 +   using assms(1) apply (unfold ex_prop_def)
    1.21 +   apply (auto simp add: OK_insert_iff Int_insert_left)
    1.22 +  done
    1.23  
    1.24  lemma ex2: 
    1.25       "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X 
    1.26 @@ -112,13 +112,18 @@
    1.27  
    1.28  subsection{*Universal Properties*}
    1.29  
    1.30 -lemma uv1 [rule_format]: 
    1.31 -     "[| uv_prop X; finite GG |] 
    1.32 -      ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
    1.33 -apply (unfold uv_prop_def)
    1.34 -apply (erule finite_induct)
    1.35 -apply (auto simp add: Int_insert_left OK_insert_iff)
    1.36 -done
    1.37 +lemma uv1:
    1.38 +  assumes "uv_prop X"
    1.39 +    and "finite GG"
    1.40 +    and "GG \<subseteq> X"
    1.41 +    and "OK GG (%G. G)"
    1.42 +  shows "(\<Squnion>G \<in> GG. G) \<in> X"
    1.43 +  using assms(2-)
    1.44 +  apply induct
    1.45 +   using assms(1)
    1.46 +   apply (unfold uv_prop_def)
    1.47 +   apply (auto simp add: Int_insert_left OK_insert_iff)
    1.48 +  done
    1.49  
    1.50  lemma uv2: 
    1.51       "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
     2.1 --- a/src/HOL/UNITY/ListOrder.thy	Sat Nov 12 20:14:09 2011 +0100
     2.2 +++ b/src/HOL/UNITY/ListOrder.thy	Sat Nov 12 21:10:56 2011 +0100
     2.3 @@ -106,36 +106,39 @@
     2.4  (** Transitivity **)
     2.5  
     2.6  (*A lemma for proving genPrefix_trans_O*)
     2.7 -lemma append_genPrefix [rule_format]:
     2.8 -     "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
     2.9 -by (induct_tac "xs", auto)
    2.10 +lemma append_genPrefix:
    2.11 +     "(xs @ ys, zs) : genPrefix r \<Longrightarrow> (xs, zs) : genPrefix r"
    2.12 +  by (induct xs arbitrary: zs) auto
    2.13  
    2.14  (*Lemma proving transitivity and more*)
    2.15 -lemma genPrefix_trans_O [rule_format]: 
    2.16 -     "(x, y) : genPrefix r  
    2.17 -      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
    2.18 -apply (erule genPrefix.induct)
    2.19 -  prefer 3 apply (blast dest: append_genPrefix)
    2.20 - prefer 2 apply (blast intro: genPrefix.prepend, blast)
    2.21 -done
    2.22 +lemma genPrefix_trans_O:
    2.23 +  assumes "(x, y) : genPrefix r"
    2.24 +  shows "\<And>z. (y, z) : genPrefix s \<Longrightarrow> (x, z) : genPrefix (r O s)"
    2.25 +  apply (atomize (full))
    2.26 +  using assms
    2.27 +  apply induct
    2.28 +    apply blast
    2.29 +   apply (blast intro: genPrefix.prepend)
    2.30 +  apply (blast dest: append_genPrefix)
    2.31 +  done
    2.32  
    2.33 -lemma genPrefix_trans [rule_format]:
    2.34 -     "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
    2.35 -      ==> (x,z) : genPrefix r"
    2.36 -apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
    2.37 - apply assumption
    2.38 -apply (blast intro: genPrefix_trans_O)
    2.39 -done
    2.40 +lemma genPrefix_trans:
    2.41 +  "(x, y) : genPrefix r \<Longrightarrow> (y, z) : genPrefix r \<Longrightarrow> trans r
    2.42 +    \<Longrightarrow> (x, z) : genPrefix r"
    2.43 +  apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
    2.44 +   apply assumption
    2.45 +  apply (blast intro: genPrefix_trans_O)
    2.46 +  done
    2.47  
    2.48 -lemma prefix_genPrefix_trans [rule_format]: 
    2.49 -     "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    2.50 +lemma prefix_genPrefix_trans:
    2.51 +  "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    2.52  apply (unfold prefix_def)
    2.53  apply (drule genPrefix_trans_O, assumption)
    2.54  apply simp
    2.55  done
    2.56  
    2.57 -lemma genPrefix_prefix_trans [rule_format]: 
    2.58 -     "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    2.59 +lemma genPrefix_prefix_trans:
    2.60 +  "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    2.61  apply (unfold prefix_def)
    2.62  apply (drule genPrefix_trans_O, assumption)
    2.63  apply simp
    2.64 @@ -147,23 +150,30 @@
    2.65  
    2.66  (** Antisymmetry **)
    2.67  
    2.68 -lemma genPrefix_antisym [rule_format]:
    2.69 -     "[| (xs,ys) : genPrefix r;  antisym r |]  
    2.70 -      ==> (ys,xs) : genPrefix r --> xs = ys"
    2.71 -apply (erule genPrefix.induct)
    2.72 -  txt{*Base case*}
    2.73 -  apply blast
    2.74 - txt{*prepend case*}
    2.75 - apply (simp add: antisym_def)
    2.76 -txt{*append case is the hardest*}
    2.77 -apply clarify
    2.78 -apply (subgoal_tac "length zs = 0", force)
    2.79 -apply (drule genPrefix_length_le)+
    2.80 -apply (simp del: length_0_conv)
    2.81 -done
    2.82 +lemma genPrefix_antisym:
    2.83 +  assumes 1: "(xs, ys) : genPrefix r"
    2.84 +    and 2: "antisym r"
    2.85 +    and 3: "(ys, xs) : genPrefix r"
    2.86 +  shows "xs = ys"
    2.87 +  using 1 3
    2.88 +proof induct
    2.89 +  case Nil
    2.90 +  then show ?case by blast
    2.91 +next
    2.92 +  case prepend
    2.93 +  then show ?case using 2 by (simp add: antisym_def)
    2.94 +next
    2.95 +  case (append xs ys zs)
    2.96 +  then show ?case
    2.97 +    apply -
    2.98 +    apply (subgoal_tac "length zs = 0", force)
    2.99 +    apply (drule genPrefix_length_le)+
   2.100 +    apply (simp del: length_0_conv)
   2.101 +    done
   2.102 +qed
   2.103  
   2.104  lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
   2.105 -by (blast intro: antisymI genPrefix_antisym)
   2.106 +  by (blast intro: antisymI genPrefix_antisym)
   2.107  
   2.108  
   2.109  subsection{*recursion equations*}
   2.110 @@ -229,23 +239,23 @@
   2.111  
   2.112  (** Proving the equivalence with Charpentier's definition **)
   2.113  
   2.114 -lemma genPrefix_imp_nth [rule_format]:
   2.115 -     "ALL i ys. i < length xs  
   2.116 -                --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
   2.117 -apply (induct_tac "xs", auto)
   2.118 -apply (case_tac "i", auto)
   2.119 -done
   2.120 +lemma genPrefix_imp_nth:
   2.121 +    "i < length xs \<Longrightarrow> (xs, ys) : genPrefix r \<Longrightarrow> (xs ! i, ys ! i) : r"
   2.122 +  apply (induct xs arbitrary: i ys)
   2.123 +   apply auto
   2.124 +  apply (case_tac i)
   2.125 +   apply auto
   2.126 +  done
   2.127  
   2.128 -lemma nth_imp_genPrefix [rule_format]:
   2.129 -     "ALL ys. length xs <= length ys   
   2.130 -      --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
   2.131 -      --> (xs, ys) : genPrefix r"
   2.132 -apply (induct_tac "xs")
   2.133 -apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
   2.134 -apply clarify
   2.135 -apply (case_tac "ys")
   2.136 -apply (force+)
   2.137 -done
   2.138 +lemma nth_imp_genPrefix:
   2.139 +  "length xs <= length ys \<Longrightarrow>
   2.140 +     (\<forall>i. i < length xs --> (xs ! i, ys ! i) : r) \<Longrightarrow>
   2.141 +     (xs, ys) : genPrefix r"
   2.142 +  apply (induct xs arbitrary: ys)
   2.143 +   apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
   2.144 +  apply (case_tac ys)
   2.145 +   apply (force+)
   2.146 +  done
   2.147  
   2.148  lemma genPrefix_iff_nth:
   2.149       "((xs,ys) : genPrefix r) =  
   2.150 @@ -371,10 +381,10 @@
   2.151  
   2.152  (*Although the prefix ordering is not linear, the prefixes of a list
   2.153    are linearly ordered.*)
   2.154 -lemma common_prefix_linear [rule_format]:
   2.155 -     "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
   2.156 -by (rule_tac xs = zs in rev_induct, auto)
   2.157 -
   2.158 +lemma common_prefix_linear:
   2.159 +  fixes xs ys zs :: "'a list"
   2.160 +  shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"
   2.161 +  by (induct zs rule: rev_induct) auto
   2.162  
   2.163  subsection{*pfixLe, pfixGe: properties inherited from the translations*}
   2.164  
     3.1 --- a/src/HOL/UNITY/ProgressSets.thy	Sat Nov 12 20:14:09 2011 +0100
     3.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Sat Nov 12 21:10:56 2011 +0100
     3.3 @@ -527,15 +527,14 @@
     3.4  text{*From Meier's thesis, section 4.5.6*}
     3.5  lemma commutativity2_lemma:
     3.6    assumes dcommutes: 
     3.7 -        "\<forall>act \<in> Acts F. 
     3.8 -         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
     3.9 -                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
    3.10 -      and determ: "!!act. act \<in> Acts F ==> single_valued act"
    3.11 -      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
    3.12 -      and lattice:  "lattice L"
    3.13 -      and BL: "B \<in> L"
    3.14 -      and TL: "T \<in> L"
    3.15 -      and Fstable: "F \<in> stable T"
    3.16 +      "\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow>
    3.17 +        s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
    3.18 +    and determ: "!!act. act \<in> Acts F ==> single_valued act"
    3.19 +    and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
    3.20 +    and lattice:  "lattice L"
    3.21 +    and BL: "B \<in> L"
    3.22 +    and TL: "T \<in> L"
    3.23 +    and Fstable: "F \<in> stable T"
    3.24    shows  "commutes F T B L"
    3.25  apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
    3.26  proof -
    3.27 @@ -555,7 +554,7 @@
    3.28      by (force intro!: funof_in 
    3.29        simp add: wp_def stable_def constrains_def determ total)
    3.30    with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
    3.31 -    by (intro dcommutes [rule_format]) assumption+ 
    3.32 +    by (intro dcommutes) assumption+ 
    3.33    with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
    3.34      by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
    3.35    with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
     4.1 --- a/src/HOL/UNITY/Project.thy	Sat Nov 12 20:14:09 2011 +0100
     4.2 +++ b/src/HOL/UNITY/Project.thy	Sat Nov 12 21:10:56 2011 +0100
     4.3 @@ -35,7 +35,7 @@
     4.4  subsection{*Safety*}
     4.5  
     4.6  (*used below to prove Join_project_ensures*)
     4.7 -lemma (in Extend) project_unless [rule_format]:
     4.8 +lemma (in Extend) project_unless:
     4.9       "[| G \<in> stable C;  project h C G \<in> A unless B |]  
    4.10        ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
    4.11  apply (simp add: unless_def project_constrains)
    4.12 @@ -460,7 +460,7 @@
    4.13    apply (blast intro!: rev_bexI )+
    4.14  done
    4.15  
    4.16 -lemma (in Extend) project_unless2 [rule_format]:
    4.17 +lemma (in Extend) project_unless2:
    4.18       "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
    4.19        ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
    4.20  by (auto dest: stable_constrains_Int intro: constrains_weaken
    4.21 @@ -479,7 +479,7 @@
    4.22  done
    4.23  
    4.24  (*Used to prove project_leadsETo_D*)
    4.25 -lemma (in Extend) Join_project_ensures [rule_format]:
    4.26 +lemma (in Extend) Join_project_ensures:
    4.27       "[| extend h F\<squnion>G \<in> stable C;   
    4.28           F\<squnion>project h C G \<in> A ensures B |]  
    4.29        ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
     5.1 --- a/src/HOL/UNITY/SubstAx.thy	Sat Nov 12 20:14:09 2011 +0100
     5.2 +++ b/src/HOL/UNITY/SubstAx.thy	Sat Nov 12 21:10:56 2011 +0100
     5.3 @@ -106,13 +106,13 @@
     5.4  
     5.5  lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
     5.6  
     5.7 -lemma LeadsTo_weaken_R [rule_format]:
     5.8 +lemma LeadsTo_weaken_R:
     5.9       "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
    5.10  apply (simp add: LeadsTo_def)
    5.11  apply (blast intro: leadsTo_weaken_R)
    5.12  done
    5.13  
    5.14 -lemma LeadsTo_weaken_L [rule_format]:
    5.15 +lemma LeadsTo_weaken_L:
    5.16       "[| F \<in> A LeadsTo A';  B \<subseteq> A |]   
    5.17        ==> F \<in> B LeadsTo A'"
    5.18  apply (simp add: LeadsTo_def)
     6.1 --- a/src/HOL/UNITY/WFair.thy	Sat Nov 12 20:14:09 2011 +0100
     6.2 +++ b/src/HOL/UNITY/WFair.thy	Sat Nov 12 21:10:56 2011 +0100
     6.3 @@ -280,7 +280,7 @@
     6.4  lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'"
     6.5  by (blast intro: subset_imp_leadsTo leadsTo_Trans)
     6.6  
     6.7 -lemma leadsTo_weaken_L [rule_format]:
     6.8 +lemma leadsTo_weaken_L:
     6.9       "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
    6.10  by (blast intro: leadsTo_Trans subset_imp_leadsTo)
    6.11