--- a/src/HOL/Relation_Power.thy Tue Dec 13 19:32:04 2005 +0100
+++ b/src/HOL/Relation_Power.thy Tue Dec 13 19:32:05 2005 +0100
@@ -11,7 +11,7 @@
begin
instance
- set :: (type) power ..
+ set :: (type) power ..
--{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
(*R^n = R O ... O R, the n-fold composition of R*)
@@ -36,89 +36,90 @@
constraints.*}
lemma funpow_add: "f ^ (m+n) = f^m o f^n"
-by(induct m) simp_all
+ by (induct m) simp_all
lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
proof -
have "f((f^n) x) = (f^(n+1)) x" by simp
- also have "\<dots> = (f^n o f^1) x" by (simp only:funpow_add)
+ also have "\<dots> = (f^n o f^1) x" by (simp only: funpow_add)
also have "\<dots> = (f^n)(f x)" by simp
finally show ?thesis .
qed
-lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
-by simp
-declare rel_pow_1 [simp]
+lemma rel_pow_1 [simp]:
+ fixes R :: "('a*'a)set"
+ shows "R^1 = R"
+ by simp
lemma rel_pow_0_I: "(x,x) : R^0"
-by simp
+ by simp
lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
-apply (auto );
-done
+ by auto
-lemma rel_pow_Suc_I2 [rule_format]:
- "\<forall>z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"
-apply (induct_tac "n", simp_all)
-apply blast
-done
+lemma rel_pow_Suc_I2:
+ "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
+ apply (induct n fixing: z)
+ apply simp
+ apply fastsimp
+ done
lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
-by simp
+ by simp
-lemma rel_pow_Suc_E:
- "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
-by auto
+lemma rel_pow_Suc_E:
+ "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
+ by auto
-lemma rel_pow_E:
- "[| (x,z) : R^n; [| n=0; x = z |] ==> P;
- !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
+lemma rel_pow_E:
+ "[| (x,z) : R^n; [| n=0; x = z |] ==> P;
+ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
|] ==> P"
-by (case_tac "n", auto)
+ by (cases n) auto
-lemma rel_pow_Suc_D2 [rule_format]:
- "\<forall>x z. (x,z):R^(Suc n) --> (\<exists>y. (x,y):R & (y,z):R^n)"
-apply (induct_tac "n")
-apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
-apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
-done
-
+lemma rel_pow_Suc_D2:
+ "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
+ apply (induct n fixing: x z)
+ apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
+ apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
+ done
lemma rel_pow_Suc_D2':
- "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
-by (induct_tac "n", simp_all, blast)
+ "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
+ by (induct n) (simp_all, blast)
-lemma rel_pow_E2:
- "[| (x,z) : R^n; [| n=0; x = z |] ==> P;
- !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
+lemma rel_pow_E2:
+ "[| (x,z) : R^n; [| n=0; x = z |] ==> P;
+ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
|] ==> P"
-apply (case_tac "n", simp)
-apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
-done
+ apply (case_tac n, simp)
+ apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
+ done
lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
-apply (simp only: split_tupled_all)
-apply (erule rtrancl_induct)
-apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
-done
+ apply (simp only: split_tupled_all)
+ apply (erule rtrancl_induct)
+ apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
+ done
lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
-apply (simp only: split_tupled_all)
-apply (induct "n")
-apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
-apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
-done
+ apply (simp only: split_tupled_all)
+ apply (induct n)
+ apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
+ apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
+ done
lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
-by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
+ by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
-lemma single_valued_rel_pow [rule_format]:
- "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
-apply (rule single_valuedI)
-apply (induct_tac "n", simp)
-apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
-done
+lemma single_valued_rel_pow:
+ "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
+ apply (rule single_valuedI)
+ apply (induct n)
+ apply simp
+ apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
+ done
ML
{*