--- a/src/HOL/Bali/Decl.thy Wed Jan 12 15:38:57 2011 +0100
+++ b/src/HOL/Bali/Decl.thy Wed Jan 12 15:53:37 2011 +0100
@@ -64,30 +64,26 @@
definition
le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b"
-instance proof
+instance
+proof
fix x y z::acc_modi
show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
- {
show "x \<le> x" \<spacespace>\<spacespace> -- reflexivity
by (auto simp add: le_acc_def)
- next
- assume "x \<le> y" "y \<le> z" -- transitivity
- thus "x \<le> z"
- by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
+ {
+ assume "x \<le> y" "y \<le> z" -- transitivity
+ then show "x \<le> z"
+ by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
next
- assume "x \<le> y" "y \<le> x" -- antisymmetry
- thus "x = y"
- proof -
- have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
+ assume "x \<le> y" "y \<le> x" -- antisymmetry
+ moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
by (auto simp add: less_acc_def split add: acc_modi.split)
- with prems show ?thesis
- by (unfold le_acc_def) iprover
- qed
+ ultimately show "x = y" by (unfold le_acc_def) iprover
next
- fix x y:: acc_modi
- show "x \<le> y \<or> y \<le> x"
- by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
+ fix x y:: acc_modi
+ show "x \<le> y \<or> y \<le> x"
+ by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
}
qed