tuned proofs;
authorwenzelm
Tue Dec 13 19:32:05 2005 +0100 (2005-12-13)
changeset 183985d63a8b35688
parent 18397 2d94eb7ff17f
child 18399 651438736fa1
tuned proofs;
src/HOL/Relation_Power.thy
     1.1 --- a/src/HOL/Relation_Power.thy	Tue Dec 13 19:32:04 2005 +0100
     1.2 +++ b/src/HOL/Relation_Power.thy	Tue Dec 13 19:32:05 2005 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  begin
     1.5  
     1.6  instance
     1.7 -  set :: (type) power ..  
     1.8 +  set :: (type) power ..
     1.9        --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
    1.10  
    1.11  (*R^n = R O ... O R, the n-fold composition of R*)
    1.12 @@ -36,89 +36,90 @@
    1.13  constraints.*}
    1.14  
    1.15  lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    1.16 -by(induct m) simp_all
    1.17 +  by (induct m) simp_all
    1.18  
    1.19  lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
    1.20  proof -
    1.21    have "f((f^n) x) = (f^(n+1)) x" by simp
    1.22 -  also have "\<dots>  = (f^n o f^1) x" by (simp only:funpow_add)
    1.23 +  also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
    1.24    also have "\<dots> = (f^n)(f x)" by simp
    1.25    finally show ?thesis .
    1.26  qed
    1.27  
    1.28 -lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
    1.29 -by simp
    1.30 -declare rel_pow_1 [simp]
    1.31 +lemma rel_pow_1 [simp]:
    1.32 +  fixes R :: "('a*'a)set"
    1.33 +  shows "R^1 = R"
    1.34 +  by simp
    1.35  
    1.36  lemma rel_pow_0_I: "(x,x) : R^0"
    1.37 -by simp
    1.38 +  by simp
    1.39  
    1.40  lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
    1.41 -apply (auto ); 
    1.42 -done
    1.43 +  by auto
    1.44  
    1.45 -lemma rel_pow_Suc_I2 [rule_format]:
    1.46 -     "\<forall>z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)"
    1.47 -apply (induct_tac "n", simp_all)
    1.48 -apply blast
    1.49 -done
    1.50 +lemma rel_pow_Suc_I2:
    1.51 +    "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
    1.52 +  apply (induct n fixing: z)
    1.53 +   apply simp
    1.54 +  apply fastsimp
    1.55 +  done
    1.56  
    1.57  lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
    1.58 -by simp
    1.59 +  by simp
    1.60  
    1.61 -lemma rel_pow_Suc_E: 
    1.62 -     "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
    1.63 -by auto
    1.64 +lemma rel_pow_Suc_E:
    1.65 +    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
    1.66 +  by auto
    1.67  
    1.68 -lemma rel_pow_E: 
    1.69 -    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
    1.70 -        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P   
    1.71 +lemma rel_pow_E:
    1.72 +    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
    1.73 +        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
    1.74       |] ==> P"
    1.75 -by (case_tac "n", auto)
    1.76 +  by (cases n) auto
    1.77  
    1.78 -lemma rel_pow_Suc_D2 [rule_format]:
    1.79 -     "\<forall>x z. (x,z):R^(Suc n) --> (\<exists>y. (x,y):R & (y,z):R^n)"
    1.80 -apply (induct_tac "n")
    1.81 -apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
    1.82 -apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
    1.83 -done
    1.84 -
    1.85 +lemma rel_pow_Suc_D2:
    1.86 +    "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
    1.87 +  apply (induct n fixing: x z)
    1.88 +   apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
    1.89 +  apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
    1.90 +  done
    1.91  
    1.92  lemma rel_pow_Suc_D2':
    1.93 -     "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
    1.94 -by (induct_tac "n", simp_all, blast)
    1.95 +    "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
    1.96 +  by (induct n) (simp_all, blast)
    1.97  
    1.98 -lemma rel_pow_E2: 
    1.99 -    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
   1.100 -        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P   
   1.101 +lemma rel_pow_E2:
   1.102 +    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
   1.103 +        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
   1.104       |] ==> P"
   1.105 -apply (case_tac "n", simp) 
   1.106 -apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) 
   1.107 -done
   1.108 +  apply (case_tac n, simp)
   1.109 +  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   1.110 +  done
   1.111  
   1.112  lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
   1.113 -apply (simp only: split_tupled_all)
   1.114 -apply (erule rtrancl_induct)
   1.115 -apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
   1.116 -done
   1.117 +  apply (simp only: split_tupled_all)
   1.118 +  apply (erule rtrancl_induct)
   1.119 +   apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
   1.120 +  done
   1.121  
   1.122  lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
   1.123 -apply (simp only: split_tupled_all)
   1.124 -apply (induct "n")
   1.125 -apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
   1.126 -apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
   1.127 -done
   1.128 +  apply (simp only: split_tupled_all)
   1.129 +  apply (induct n)
   1.130 +   apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
   1.131 +  apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
   1.132 +  done
   1.133  
   1.134  lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
   1.135 -by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   1.136 +  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   1.137  
   1.138  
   1.139 -lemma single_valued_rel_pow [rule_format]:
   1.140 -     "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
   1.141 -apply (rule single_valuedI)
   1.142 -apply (induct_tac "n", simp)
   1.143 -apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   1.144 -done
   1.145 +lemma single_valued_rel_pow:
   1.146 +    "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
   1.147 +  apply (rule single_valuedI)
   1.148 +  apply (induct n)
   1.149 +   apply simp
   1.150 +  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   1.151 +  done
   1.152  
   1.153  ML
   1.154  {*