--- 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
--- 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*}
--- 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))"
--- 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)"
--- 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)
--- 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)