src/ZF/ex/Commutation.thy

--- a/src/ZF/ex/Commutation.thy	Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/ex/Commutation.thy	Tue Nov 07 19:40:13 2006 +0100
@@ -4,41 +4,41 @@
     Copyright   1995  TU Muenchen
 
 Commutation theory for proving the Church Rosser theorem
-	ported from Isabelle/HOL  by Sidi Ould Ehmety
+        ported from Isabelle/HOL  by Sidi Ould Ehmety
 *)
 
 theory Commutation imports Main begin
 
-constdefs
+definition
   square  :: "[i, i, i, i] => o"
-   "square(r,s,t,u) ==
-     (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
+  "square(r,s,t,u) ==
+    (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
 
   commute :: "[i, i] => o"
-   "commute(r,s) == square(r,s,s,r)"
+  "commute(r,s) == square(r,s,s,r)"
 
   diamond :: "i=>o"
-   "diamond(r)   == commute(r, r)"
+  "diamond(r)   == commute(r, r)"
 
   strip :: "i=>o"
-   "strip(r) == commute(r^*, r)"
+  "strip(r) == commute(r^*, r)"
 
   Church_Rosser :: "i => o"
-   "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r Un converse(r))^* -->
-	 	 	 (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
+  "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r Un converse(r))^* -->
+                        (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
   confluent :: "i=>o"
-   "confluent(r) == diamond(r^*)"
+  "confluent(r) == diamond(r^*)"
 
 
 lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)"
-by (unfold square_def, blast)
+  unfolding square_def by blast
 
 lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)"
-by (unfold square_def, blast)
+  unfolding square_def by blast
 
 
-lemma square_rtrancl [rule_format]: 
-     "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)"
+lemma square_rtrancl:
+  "square(r,s,s,t) ==> field(s)<=field(t) ==> square(r^*,s,s,t^*)"
 apply (unfold square_def, clarify)
 apply (erule rtrancl_induct)
 apply (blast intro: rtrancl_refl)
@@ -46,23 +46,22 @@
 done
 
 (* A special case of square_rtrancl_on *)
-lemma diamond_strip: 
- "diamond(r) ==> strip(r)"
+lemma diamond_strip:
+  "diamond(r) ==> strip(r)"
 apply (unfold diamond_def commute_def strip_def)
 apply (rule square_rtrancl, simp_all)
 done
 
 (*** commute ***)
 
-lemma commute_sym: 
-    "commute(r,s) ==> commute(s,r)"
-by (unfold commute_def, blast intro: square_sym)
+lemma commute_sym: "commute(r,s) ==> commute(s,r)"
+  unfolding commute_def by (blast intro: square_sym)
 
-lemma commute_rtrancl [rule_format]: 
-    "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"
-apply (unfold commute_def, clarify)
+lemma commute_rtrancl:
+  "commute(r,s) ==> field(r)=field(s) ==> commute(r^*,s^*)"
+apply (unfold commute_def)
 apply (rule square_rtrancl)
-apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) 
+apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
 apply (simp_all add: rtrancl_field)
 done
 
@@ -77,20 +76,20 @@
 done
 
 lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
-by (unfold commute_def square_def, blast)
+  unfolding commute_def square_def by blast
 
-lemma diamond_Un: 
+lemma diamond_Un:
      "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
-by (unfold diamond_def, blast intro: commute_Un commute_sym) 
+  unfolding diamond_def by (blast intro: commute_Un commute_sym)
 
-lemma diamond_confluent: 
+lemma diamond_confluent:
     "diamond(r) ==> confluent(r)"
 apply (unfold diamond_def confluent_def)
 apply (erule commute_rtrancl, simp)
 done
 
-lemma confluent_Un: 
- "[| confluent(r); confluent(s); commute(r^*, s^*); 
+lemma confluent_Un:
+ "[| confluent(r); confluent(s); commute(r^*, s^*);
      relation(r); relation(s) |] ==> confluent(r Un s)"
 apply (unfold confluent_def)
 apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
@@ -98,7 +97,7 @@
 done
 
 
-lemma diamond_to_confluence: 
+lemma diamond_to_confluence:
      "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
 apply (drule rtrancl_subset [symmetric], assumption)
 apply (simp_all add: confluent_def)
@@ -108,9 +107,9 @@
 
 (*** Church_Rosser ***)
 
-lemma Church_Rosser1: 
+lemma Church_Rosser1:
      "Church_Rosser(r) ==> confluent(r)"
-apply (unfold confluent_def Church_Rosser_def square_def 
+apply (unfold confluent_def Church_Rosser_def square_def
               commute_def diamond_def, auto)
 apply (drule converseI)
 apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
@@ -121,9 +120,9 @@
 done
 
 
-lemma Church_Rosser2: 
+lemma Church_Rosser2:
      "confluent(r) ==> Church_Rosser(r)"
-apply (unfold confluent_def Church_Rosser_def square_def 
+apply (unfold confluent_def Church_Rosser_def square_def
               commute_def diamond_def, auto)
 apply (frule fieldI1)
 apply (simp add: rtrancl_field)
@@ -134,6 +133,6 @@
 
 
 lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
-by (blast intro: Church_Rosser1 Church_Rosser2)
+  by (blast intro: Church_Rosser1 Church_Rosser2)
 
-end          
+end