--- 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
--- 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)
--- 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 *}