# HG changeset patch
# User bulwahn
# Date 1327928126 -3600
# Node ID b2878f059f919b9fa604c8b5a300858c3173d990
# Parent  87d5d36a9005eb710b4f39759e580e2f4ddcd319
renaming all lemmas with name rel_pow to relpow

diff -r 87d5d36a9005 -r b2878f059f91 src/HOL/Hoare_Parallel/OG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Mon Jan 30 13:55:24 2012 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Mon Jan 30 13:55:26 2012 +0100
@@ -102,7 +102,7 @@
  "(Basic f, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> t = f s"
 apply(induct "n")
  apply(simp (no_asm))
-apply(fast dest: rel_pow_Suc_D2 Parallel_empty_lemma elim: transition_cases)
+apply(fast dest: relpow_Suc_D2 Parallel_empty_lemma elim: transition_cases)
 done
 
 lemma SEM_fwhile: "SEM S (p \<inter> b) \<subseteq> p \<Longrightarrow> SEM (fwhile b S k) p \<subseteq> (p \<inter> -b)"
@@ -112,7 +112,7 @@
 apply(rule conjI)
  apply (blast dest: L3_5i) 
 apply(simp add: SEM_def sem_def id_def)
-apply (blast dest: Basic_ntran rtrancl_imp_UN_rel_pow) 
+apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow) 
 done
 
 lemma atom_hoare_sound [rule_format]: 
@@ -122,7 +122,7 @@
 apply simp_all
 --{*Basic*}
     apply(simp add: SEM_def sem_def)
-    apply(fast dest: rtrancl_imp_UN_rel_pow Basic_ntran)
+    apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
 --{* Seq *}
    apply(rule impI)
    apply(rule subset_trans)
@@ -448,7 +448,7 @@
       apply(force dest: nth_mem simp add: All_None_def)
 --{* Basic *}
     apply(simp add: SEM_def sem_def)
-    apply(force dest: rtrancl_imp_UN_rel_pow Basic_ntran)
+    apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
 --{* Seq *}
    apply(rule subset_trans)
     prefer 2 apply assumption
diff -r 87d5d36a9005 -r b2878f059f91 src/HOL/Hoare_Parallel/OG_Tran.thy
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Mon Jan 30 13:55:24 2012 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Mon Jan 30 13:55:26 2012 +0100
@@ -120,7 +120,7 @@
 apply(induct n)
  apply(simp (no_asm))
 apply clarify
-apply(drule rel_pow_Suc_D2)
+apply(drule relpow_Suc_D2)
 apply(force elim:transition_cases)
 done
 
@@ -129,7 +129,7 @@
 apply(induct "n")
  apply(simp (no_asm))
 apply clarify
-apply(drule rel_pow_Suc_D2)
+apply(drule relpow_Suc_D2)
 apply clarify
 apply(erule transition_cases,simp_all)
 apply(force dest:nth_mem simp add:All_None_def)
@@ -138,7 +138,7 @@
 lemma Parallel_AllNone: "All_None Ts \<Longrightarrow> (SEM (Parallel Ts) X) = X"
 apply (unfold SEM_def sem_def)
 apply auto
-apply(drule rtrancl_imp_UN_rel_pow)
+apply(drule rtrancl_imp_UN_relpow)
 apply clarify
 apply(drule Parallel_AllNone_lemma)
 apply auto
@@ -171,18 +171,18 @@
   (All_None Rs) \<and> (c2, y) -Pm\<rightarrow> (Parallel Ts, t) \<and>  m \<le> n)"
 apply(induct "n")
  apply(force)
-apply(safe dest!: rel_pow_Suc_D2)
+apply(safe dest!: relpow_Suc_D2)
 apply(erule transition_cases,simp_all)
  apply (fast intro!: le_SucI)
-apply (fast intro!: le_SucI elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
+apply (fast intro!: le_SucI elim!: relpow_imp_rtrancl converse_rtrancl_into_rtrancl)
 done
 
 lemma L3_5ii_lemma3: 
  "\<lbrakk>(Seq c1 c2,s) -P*\<rightarrow> (Parallel Ts,t); All_None Ts\<rbrakk> \<Longrightarrow> 
     (\<exists>y Rs. (c1,s) -P*\<rightarrow> (Parallel Rs,y) \<and> All_None Rs 
    \<and> (c2,y) -P*\<rightarrow> (Parallel Ts,t))"
-apply(drule rtrancl_imp_UN_rel_pow)
-apply(fast dest: L3_5ii_lemma2 rel_pow_imp_rtrancl)
+apply(drule rtrancl_imp_UN_relpow)
+apply(fast dest: L3_5ii_lemma2 relpow_imp_rtrancl)
 done
 
 lemma L3_5ii: "SEM (Seq c1 c2) X = SEM c2 (SEM c1 X)"
@@ -212,16 +212,16 @@
 apply (unfold UNIV_def)
 apply(rule nat_less_induct)
 apply safe
-apply(erule rel_pow_E2)
+apply(erule relpow_E2)
  apply simp_all
 apply(erule transition_cases)
  apply simp_all
-apply(erule rel_pow_E2)
+apply(erule relpow_E2)
  apply(simp add: Id_def)
 apply(erule transition_cases,simp_all)
 apply clarify
 apply(erule transition_cases,simp_all)
-apply(erule rel_pow_E2,simp)
+apply(erule relpow_E2,simp)
 apply clarify
 apply(erule transition_cases)
  apply simp+
@@ -231,7 +231,7 @@
 done
 
 lemma L3_5v_lemma2: "\<lbrakk>(\<Omega>, s) -P*\<rightarrow> (Parallel Ts, t); All_None Ts \<rbrakk> \<Longrightarrow> False"
-apply(fast dest: rtrancl_imp_UN_rel_pow L3_5v_lemma1)
+apply(fast dest: rtrancl_imp_UN_relpow L3_5v_lemma1)
 done
 
 lemma L3_5v_lemma3: "SEM (\<Omega>) S = {}"
@@ -244,7 +244,7 @@
   (\<exists>k. (fwhile b c k, s) -P*\<rightarrow> (Parallel Ts, t))"
 apply(rule nat_less_induct)
 apply safe
-apply(erule rel_pow_E2)
+apply(erule relpow_E2)
  apply safe
 apply(erule transition_cases,simp_all)
  apply (rule_tac x = "1" in exI)
@@ -275,9 +275,9 @@
  apply(rule converse_rtrancl_into_rtrancl)
   apply(fast)
  apply(fast elim!: L3_5ii_lemma1 dest: L3_5ii_lemma3)
-apply(drule rtrancl_imp_UN_rel_pow)
+apply(drule rtrancl_imp_UN_relpow)
 apply clarify
-apply(erule rel_pow_E2)
+apply(erule relpow_E2)
  apply simp_all
 apply(erule transition_cases,simp_all)
 apply(fast dest: Parallel_empty_lemma)
@@ -287,7 +287,7 @@
 apply(rule ext)
 apply (simp add: SEM_def sem_def)
 apply safe
- apply(drule rtrancl_imp_UN_rel_pow,simp)
+ apply(drule rtrancl_imp_UN_relpow,simp)
  apply clarify
  apply(fast dest:L3_5v_lemma4)
 apply(fast intro: L3_5v_lemma5)
diff -r 87d5d36a9005 -r b2878f059f91 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Jan 30 13:55:24 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Jan 30 13:55:26 2012 +0100
@@ -730,85 +730,85 @@
 
 hide_const (open) relpow
 
-lemma rel_pow_1 [simp]:
+lemma relpow_1 [simp]:
   fixes R :: "('a \<times> 'a) set"
   shows "R ^^ 1 = R"
   by simp
 
-lemma rel_pow_0_I: 
+lemma relpow_0_I: 
   "(x, x) \<in> R ^^ 0"
   by simp
 
-lemma rel_pow_Suc_I:
+lemma relpow_Suc_I:
   "(x, y) \<in>  R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
   by auto
 
-lemma rel_pow_Suc_I2:
+lemma relpow_Suc_I2:
   "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
   by (induct n arbitrary: z) (simp, fastforce)
 
-lemma rel_pow_0_E:
+lemma relpow_0_E:
   "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   by simp
 
-lemma rel_pow_Suc_E:
+lemma relpow_Suc_E:
   "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
   by auto
 
-lemma rel_pow_E:
+lemma relpow_E:
   "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
    \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
    \<Longrightarrow> P"
   by (cases n) auto
 
-lemma rel_pow_Suc_D2:
+lemma relpow_Suc_D2:
   "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
   apply (induct n arbitrary: 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)
+   apply (blast intro: relpow_0_I elim: relpow_0_E relpow_Suc_E)
+  apply (blast intro: relpow_Suc_I elim: relpow_0_E relpow_Suc_E)
   done
 
-lemma rel_pow_Suc_E2:
+lemma relpow_Suc_E2:
   "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast dest: rel_pow_Suc_D2)
+  by (blast dest: relpow_Suc_D2)
 
-lemma rel_pow_Suc_D2':
+lemma relpow_Suc_D2':
   "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)"
   by (induct n) (simp_all, blast)
 
-lemma rel_pow_E2:
+lemma relpow_E2:
   "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
      \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
    \<Longrightarrow> P"
   apply (cases n, simp)
-  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
+  apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)
   done
 
-lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
+lemma relpow_add: "R ^^ (m+n) = R^^m O R^^n"
   by (induct n) auto
 
-lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
+lemma relpow_commute: "R O R ^^ n = R ^^ n O R"
   by (induct n) (simp, simp add: O_assoc [symmetric])
 
-lemma rel_pow_empty:
+lemma relpow_empty:
   "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"
   by (cases n) auto
 
-lemma rtrancl_imp_UN_rel_pow:
+lemma rtrancl_imp_UN_relpow:
   assumes "p \<in> R^*"
   shows "p \<in> (\<Union>n. R ^^ n)"
 proof (cases p)
   case (Pair x y)
   with assms have "(x, y) \<in> R^*" by simp
   then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct
-    case base show ?case by (blast intro: rel_pow_0_I)
+    case base show ?case by (blast intro: relpow_0_I)
   next
-    case step then show ?case by (blast intro: rel_pow_Suc_I)
+    case step then show ?case by (blast intro: relpow_Suc_I)
   qed
   with Pair show ?thesis by simp
 qed
 
-lemma rel_pow_imp_rtrancl:
+lemma relpow_imp_rtrancl:
   assumes "p \<in> R ^^ n"
   shows "p \<in> R^*"
 proof (cases p)
@@ -818,18 +818,18 @@
     case 0 then show ?case by simp
   next
     case Suc then show ?case
-      by (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
+      by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl)
   qed
   with Pair show ?thesis by simp
 qed
 
-lemma rtrancl_is_UN_rel_pow:
+lemma rtrancl_is_UN_relpow:
   "R^* = (\<Union>n. R ^^ n)"
-  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
+  by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl)
 
 lemma rtrancl_power:
   "p \<in> R^* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)"
-  by (simp add: rtrancl_is_UN_rel_pow)
+  by (simp add: rtrancl_is_UN_relpow)
 
 lemma trancl_power:
   "p \<in> R^+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)"
@@ -837,23 +837,23 @@
   apply simp
   apply (rule iffI)
    apply (drule tranclD2)
-   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
+   apply (clarsimp simp: rtrancl_is_UN_relpow)
    apply (rule_tac x="Suc n" in exI)
    apply (clarsimp simp: rel_comp_def)
    apply fastforce
   apply clarsimp
   apply (case_tac n, simp)
   apply clarsimp
-  apply (drule rel_pow_imp_rtrancl)
+  apply (drule relpow_imp_rtrancl)
   apply (drule rtrancl_into_trancl1) apply auto
   done
 
-lemma rtrancl_imp_rel_pow:
+lemma rtrancl_imp_relpow:
   "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n"
-  by (auto dest: rtrancl_imp_UN_rel_pow)
+  by (auto dest: rtrancl_imp_UN_relpow)
 
 text{* By Sternagel/Thiemann: *}
-lemma rel_pow_fun_conv:
+lemma relpow_fun_conv:
   "((a,b) \<in> R ^^ n) = (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f(Suc i)) \<in> R))"
 proof (induct n arbitrary: b)
   case 0 show ?case by auto
@@ -877,7 +877,7 @@
   qed
 qed
 
-lemma rel_pow_finite_bounded1:
+lemma relpow_finite_bounded1:
 assumes "finite(R :: ('a*'a)set)" and "k>0"
 shows "R^^k \<subseteq> (UN n:{n. 0<n & n <= card R}. R^^n)" (is "_ \<subseteq> ?r")
 proof-
@@ -898,7 +898,7 @@
         hence ?case using `(a,b): R^^(Suc n)` Suc_leI[OF `n < card R`] by blast
       } moreover
       { assume "n = card R"
-        from `(a,b) \<in> R ^^ (Suc n)`[unfolded rel_pow_fun_conv]
+        from `(a,b) \<in> R ^^ (Suc n)`[unfolded relpow_fun_conv]
         obtain f where "f 0 = a" and "f(Suc n) = b"
           and steps: "\<And>i. i <= n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto
         let ?p = "%i. (f i, f(Suc i))"
@@ -918,7 +918,7 @@
           and pij: "?p i = ?p j" by blast
         let ?g = "\<lambda> l. if l \<le> i then f l else f (l + (j - i))"
         let ?n = "Suc(n - (j - i))"
-        have abl: "(a,b) \<in> R ^^ ?n" unfolding rel_pow_fun_conv
+        have abl: "(a,b) \<in> R ^^ ?n" unfolding relpow_fun_conv
         proof (rule exI[of _ ?g], intro conjI impI allI)
           show "?g ?n = b" using `f(Suc n) = b` j ij by auto
         next
@@ -952,21 +952,21 @@
   thus ?thesis using gr0_implies_Suc[OF `k>0`] by auto
 qed
 
-lemma rel_pow_finite_bounded:
+lemma relpow_finite_bounded:
 assumes "finite(R :: ('a*'a)set)"
 shows "R^^k \<subseteq> (UN n:{n. n <= card R}. R^^n)"
 apply(cases k)
  apply force
-using rel_pow_finite_bounded1[OF assms, of k] by auto
+using relpow_finite_bounded1[OF assms, of k] by auto
 
-lemma rtrancl_finite_eq_rel_pow:
+lemma rtrancl_finite_eq_relpow:
   "finite R \<Longrightarrow> R^* = (UN n : {n. n <= card R}. R^^n)"
-by(fastforce simp: rtrancl_power dest: rel_pow_finite_bounded)
+by(fastforce simp: rtrancl_power dest: relpow_finite_bounded)
 
-lemma trancl_finite_eq_rel_pow:
+lemma trancl_finite_eq_relpow:
   "finite R \<Longrightarrow> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)"
 apply(auto simp add: trancl_power)
-apply(auto dest: rel_pow_finite_bounded1)
+apply(auto dest: relpow_finite_bounded1)
 done
 
 lemma finite_rel_comp[simp,intro]:
@@ -986,13 +986,13 @@
  apply(simp_all add: assms)
 done
 
-lemma single_valued_rel_pow:
+lemma single_valued_relpow:
   fixes R :: "('a * 'a) set"
   shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
 apply (induct n arbitrary: R)
 apply simp_all
 apply (rule single_valuedI)
-apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
+apply (fast dest: single_valuedD elim: relpow_Suc_E)
 done
 
 
@@ -1052,7 +1052,7 @@
 
 lemma finite_trancl_ntranl:
   "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"
-  by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
+  by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def)
 
 
 subsection {* Acyclic relations *}