# HG changeset patch
# User wenzelm
# Date 1321128656 -3600
# Node ID 11d9c2768729f9296f47ed54ac150eef896524db
# Parent  6f9e24376ffd577eaef10fa49b4d9108aa708e25
tuned proofs;

diff -r 6f9e24376ffd -r 11d9c2768729 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Sat Nov 12 20:14:09 2011 +0100
+++ b/src/HOL/UNITY/Guar.thy	Sat Nov 12 21:10:56 2011 +0100
@@ -75,14 +75,14 @@
 
 subsection{*Existential Properties*}
 
-lemma ex1 [rule_format]: 
- "[| ex_prop X; finite GG |] ==>  
-     GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
-apply (unfold ex_prop_def)
-apply (erule finite_induct)
-apply (auto simp add: OK_insert_iff Int_insert_left)
-done
-
+lemma ex1:
+  assumes "ex_prop X" and "finite GG"
+  shows "GG \<inter> X \<noteq> {} \<Longrightarrow> OK GG (%G. G) \<Longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X"
+  apply (atomize (full))
+  using assms(2) apply induct
+   using assms(1) apply (unfold ex_prop_def)
+   apply (auto simp add: OK_insert_iff Int_insert_left)
+  done
 
 lemma ex2: 
      "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X 
@@ -112,13 +112,18 @@
 
 subsection{*Universal Properties*}
 
-lemma uv1 [rule_format]: 
-     "[| uv_prop X; finite GG |] 
-      ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
-apply (unfold uv_prop_def)
-apply (erule finite_induct)
-apply (auto simp add: Int_insert_left OK_insert_iff)
-done
+lemma uv1:
+  assumes "uv_prop X"
+    and "finite GG"
+    and "GG \<subseteq> X"
+    and "OK GG (%G. G)"
+  shows "(\<Squnion>G \<in> GG. G) \<in> X"
+  using assms(2-)
+  apply induct
+   using assms(1)
+   apply (unfold uv_prop_def)
+   apply (auto simp add: Int_insert_left OK_insert_iff)
+  done
 
 lemma uv2: 
      "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
diff -r 6f9e24376ffd -r 11d9c2768729 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Sat Nov 12 20:14:09 2011 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Sat Nov 12 21:10:56 2011 +0100
@@ -106,36 +106,39 @@
 (** Transitivity **)
 
 (*A lemma for proving genPrefix_trans_O*)
-lemma append_genPrefix [rule_format]:
-     "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
-by (induct_tac "xs", auto)
+lemma append_genPrefix:
+     "(xs @ ys, zs) : genPrefix r \<Longrightarrow> (xs, zs) : genPrefix r"
+  by (induct xs arbitrary: zs) auto
 
 (*Lemma proving transitivity and more*)
-lemma genPrefix_trans_O [rule_format]: 
-     "(x, y) : genPrefix r  
-      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
-apply (erule genPrefix.induct)
-  prefer 3 apply (blast dest: append_genPrefix)
- prefer 2 apply (blast intro: genPrefix.prepend, blast)
-done
+lemma genPrefix_trans_O:
+  assumes "(x, y) : genPrefix r"
+  shows "\<And>z. (y, z) : genPrefix s \<Longrightarrow> (x, z) : genPrefix (r O s)"
+  apply (atomize (full))
+  using assms
+  apply induct
+    apply blast
+   apply (blast intro: genPrefix.prepend)
+  apply (blast dest: append_genPrefix)
+  done
 
-lemma genPrefix_trans [rule_format]:
-     "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
-      ==> (x,z) : genPrefix r"
-apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
- apply assumption
-apply (blast intro: genPrefix_trans_O)
-done
+lemma genPrefix_trans:
+  "(x, y) : genPrefix r \<Longrightarrow> (y, z) : genPrefix r \<Longrightarrow> trans r
+    \<Longrightarrow> (x, z) : genPrefix r"
+  apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
+   apply assumption
+  apply (blast intro: genPrefix_trans_O)
+  done
 
-lemma prefix_genPrefix_trans [rule_format]: 
-     "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
+lemma prefix_genPrefix_trans:
+  "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
 apply (unfold prefix_def)
 apply (drule genPrefix_trans_O, assumption)
 apply simp
 done
 
-lemma genPrefix_prefix_trans [rule_format]: 
-     "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
+lemma genPrefix_prefix_trans:
+  "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
 apply (unfold prefix_def)
 apply (drule genPrefix_trans_O, assumption)
 apply simp
@@ -147,23 +150,30 @@
 
 (** Antisymmetry **)
 
-lemma genPrefix_antisym [rule_format]:
-     "[| (xs,ys) : genPrefix r;  antisym r |]  
-      ==> (ys,xs) : genPrefix r --> xs = ys"
-apply (erule genPrefix.induct)
-  txt{*Base case*}
-  apply blast
- txt{*prepend case*}
- apply (simp add: antisym_def)
-txt{*append case is the hardest*}
-apply clarify
-apply (subgoal_tac "length zs = 0", force)
-apply (drule genPrefix_length_le)+
-apply (simp del: length_0_conv)
-done
+lemma genPrefix_antisym:
+  assumes 1: "(xs, ys) : genPrefix r"
+    and 2: "antisym r"
+    and 3: "(ys, xs) : genPrefix r"
+  shows "xs = ys"
+  using 1 3
+proof induct
+  case Nil
+  then show ?case by blast
+next
+  case prepend
+  then show ?case using 2 by (simp add: antisym_def)
+next
+  case (append xs ys zs)
+  then show ?case
+    apply -
+    apply (subgoal_tac "length zs = 0", force)
+    apply (drule genPrefix_length_le)+
+    apply (simp del: length_0_conv)
+    done
+qed
 
 lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
-by (blast intro: antisymI genPrefix_antisym)
+  by (blast intro: antisymI genPrefix_antisym)
 
 
 subsection{*recursion equations*}
@@ -229,23 +239,23 @@
 
 (** Proving the equivalence with Charpentier's definition **)
 
-lemma genPrefix_imp_nth [rule_format]:
-     "ALL i ys. i < length xs  
-                --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
-apply (induct_tac "xs", auto)
-apply (case_tac "i", auto)
-done
+lemma genPrefix_imp_nth:
+    "i < length xs \<Longrightarrow> (xs, ys) : genPrefix r \<Longrightarrow> (xs ! i, ys ! i) : r"
+  apply (induct xs arbitrary: i ys)
+   apply auto
+  apply (case_tac i)
+   apply auto
+  done
 
-lemma nth_imp_genPrefix [rule_format]:
-     "ALL ys. length xs <= length ys   
-      --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
-      --> (xs, ys) : genPrefix r"
-apply (induct_tac "xs")
-apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
-apply clarify
-apply (case_tac "ys")
-apply (force+)
-done
+lemma nth_imp_genPrefix:
+  "length xs <= length ys \<Longrightarrow>
+     (\<forall>i. i < length xs --> (xs ! i, ys ! i) : r) \<Longrightarrow>
+     (xs, ys) : genPrefix r"
+  apply (induct xs arbitrary: ys)
+   apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
+  apply (case_tac ys)
+   apply (force+)
+  done
 
 lemma genPrefix_iff_nth:
      "((xs,ys) : genPrefix r) =  
@@ -371,10 +381,10 @@
 
 (*Although the prefix ordering is not linear, the prefixes of a list
   are linearly ordered.*)
-lemma common_prefix_linear [rule_format]:
-     "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
-by (rule_tac xs = zs in rev_induct, auto)
-
+lemma common_prefix_linear:
+  fixes xs ys zs :: "'a list"
+  shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"
+  by (induct zs rule: rev_induct) auto
 
 subsection{*pfixLe, pfixGe: properties inherited from the translations*}
 
diff -r 6f9e24376ffd -r 11d9c2768729 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Sat Nov 12 20:14:09 2011 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy	Sat Nov 12 21:10:56 2011 +0100
@@ -527,15 +527,14 @@
 text{*From Meier's thesis, section 4.5.6*}
 lemma commutativity2_lemma:
   assumes dcommutes: 
-        "\<forall>act \<in> Acts F. 
-         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
-                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
-      and determ: "!!act. act \<in> Acts F ==> single_valued act"
-      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
-      and lattice:  "lattice L"
-      and BL: "B \<in> L"
-      and TL: "T \<in> L"
-      and Fstable: "F \<in> stable T"
+      "\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow>
+        s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
+    and determ: "!!act. act \<in> Acts F ==> single_valued act"
+    and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
+    and lattice:  "lattice L"
+    and BL: "B \<in> L"
+    and TL: "T \<in> L"
+    and Fstable: "F \<in> stable T"
   shows  "commutes F T B L"
 apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
 proof -
@@ -555,7 +554,7 @@
     by (force intro!: funof_in 
       simp add: wp_def stable_def constrains_def determ total)
   with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
-    by (intro dcommutes [rule_format]) assumption+ 
+    by (intro dcommutes) assumption+ 
   with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
     by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
   with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
diff -r 6f9e24376ffd -r 11d9c2768729 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Sat Nov 12 20:14:09 2011 +0100
+++ b/src/HOL/UNITY/Project.thy	Sat Nov 12 21:10:56 2011 +0100
@@ -35,7 +35,7 @@
 subsection{*Safety*}
 
 (*used below to prove Join_project_ensures*)
-lemma (in Extend) project_unless [rule_format]:
+lemma (in Extend) project_unless:
      "[| G \<in> stable C;  project h C G \<in> A unless B |]  
       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
 apply (simp add: unless_def project_constrains)
@@ -460,7 +460,7 @@
   apply (blast intro!: rev_bexI )+
 done
 
-lemma (in Extend) project_unless2 [rule_format]:
+lemma (in Extend) project_unless2:
      "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
 by (auto dest: stable_constrains_Int intro: constrains_weaken
@@ -479,7 +479,7 @@
 done
 
 (*Used to prove project_leadsETo_D*)
-lemma (in Extend) Join_project_ensures [rule_format]:
+lemma (in Extend) Join_project_ensures:
      "[| extend h F\<squnion>G \<in> stable C;   
          F\<squnion>project h C G \<in> A ensures B |]  
       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
diff -r 6f9e24376ffd -r 11d9c2768729 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Sat Nov 12 20:14:09 2011 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Sat Nov 12 21:10:56 2011 +0100
@@ -106,13 +106,13 @@
 
 lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
 
-lemma LeadsTo_weaken_R [rule_format]:
+lemma LeadsTo_weaken_R:
      "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
 apply (simp add: LeadsTo_def)
 apply (blast intro: leadsTo_weaken_R)
 done
 
-lemma LeadsTo_weaken_L [rule_format]:
+lemma LeadsTo_weaken_L:
      "[| F \<in> A LeadsTo A';  B \<subseteq> A |]   
       ==> F \<in> B LeadsTo A'"
 apply (simp add: LeadsTo_def)
diff -r 6f9e24376ffd -r 11d9c2768729 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Sat Nov 12 20:14:09 2011 +0100
+++ b/src/HOL/UNITY/WFair.thy	Sat Nov 12 21:10:56 2011 +0100
@@ -280,7 +280,7 @@
 lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'"
 by (blast intro: subset_imp_leadsTo leadsTo_Trans)
 
-lemma leadsTo_weaken_L [rule_format]:
+lemma leadsTo_weaken_L:
      "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
 by (blast intro: leadsTo_Trans subset_imp_leadsTo)