--- a/Quot/QuotBase.thy Wed Feb 10 17:22:18 2010 +0100
+++ b/Quot/QuotBase.thy Wed Feb 10 20:35:54 2010 +0100
@@ -67,6 +67,7 @@
by auto
text {* Composition of Relations *}
+
abbreviation
rel_conj (infixr "OOO" 75)
where
@@ -190,20 +191,20 @@
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
proof -
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
- apply(simp add: expand_fun_eq)
- using q1 q2
- apply(simp add: Quotient_def)
- done
+ using q1 q2
+ unfolding Quotient_def
+ unfolding expand_fun_eq
+ by simp
moreover
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
- apply(auto)
- using q1 q2 unfolding Quotient_def
- apply(metis)
- done
+ using q1 q2
+ unfolding Quotient_def
+ by (simp (no_asm)) (metis)
moreover
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
- apply(auto simp add: expand_fun_eq)
+ unfolding expand_fun_eq
+ apply(auto)
using q1 q2 unfolding Quotient_def
apply(metis)
using q1 q2 unfolding Quotient_def
@@ -221,16 +222,16 @@
lemma abs_o_rep:
assumes a: "Quotient R Abs Rep"
shows "Abs o Rep = id"
- apply(rule ext)
- apply(simp add: Quotient_abs_rep[OF a])
- done
+ unfolding expand_fun_eq
+ by (simp add: Quotient_abs_rep[OF a])
lemma equals_rsp:
assumes q: "Quotient R Abs Rep"
and a: "R xa xb" "R ya yb"
shows "R xa ya = R xb yb"
- using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def
- using a by blast
+ using a Quotient_symp[OF q] Quotient_transp[OF q]
+ unfolding symp_def transp_def
+ by blast
lemma lambda_prs:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -252,21 +253,23 @@
assumes q: "Quotient R Abs Rep"
and a: "R x1 x2"
shows "R x1 (Rep (Abs x2))"
- using a
- by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
+ using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
+ by metis
lemma rep_abs_rsp_left:
assumes q: "Quotient R Abs Rep"
and a: "R x1 x2"
shows "R (Rep (Abs x1)) x2"
- using a
- by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
+ using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
+ by metis
-(* In the following theorem R1 can be instantiated with anything,
- but we know some of the types of the Rep and Abs functions;
- so by solving Quotient assumptions we can get a unique R1 that
- will be provable; which is why we need to use apply_rsp and
- not the primed version *)
+text{*
+ In the following theorem R1 can be instantiated with anything,
+ but we know some of the types of the Rep and Abs functions;
+ so by solving Quotient assumptions we can get a unique R1 that
+ will be provable; which is why we need to use apply_rsp and
+ not the primed version *}
+
lemma apply_rsp:
fixes f g::"'a \<Rightarrow> 'c"
assumes q: "Quotient R1 Abs1 Rep1"
@@ -285,33 +288,37 @@
fixes P :: "'a \<Rightarrow> bool"
assumes a: "equivp R"
shows "Ball (Respects R) P = (All P)"
- by (metis equivp_def in_respects a)
+ using a
+ unfolding equivp_def
+ by (auto simp add: in_respects)
lemma bex_reg_eqv:
fixes P :: "'a \<Rightarrow> bool"
assumes a: "equivp R"
shows "Bex (Respects R) P = (Ex P)"
- by (metis equivp_def in_respects a)
+ using a
+ unfolding equivp_def
+ by (auto simp add: in_respects)
lemma ball_reg_right:
assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
shows "All P \<longrightarrow> Ball R Q"
- by (metis COMBC_def Collect_def Collect_mem_eq a)
+ using a by (metis COMBC_def Collect_def Collect_mem_eq)
lemma bex_reg_left:
assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
shows "Bex R Q \<longrightarrow> Ex P"
- by (metis COMBC_def Collect_def Collect_mem_eq a)
+ using a by (metis COMBC_def Collect_def Collect_mem_eq)
lemma ball_reg_left:
assumes a: "equivp R"
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
- by (metis equivp_reflp in_respects a)
+ using a by (metis equivp_reflp in_respects)
lemma bex_reg_right:
assumes a: "equivp R"
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
- by (metis equivp_reflp in_respects a)
+ using a by (metis equivp_reflp in_respects)
lemma ball_reg_eqv_range:
fixes P::"'a \<Rightarrow> bool"
@@ -351,7 +358,7 @@
assumes a: "!x :: 'a. (P x --> Q x)"
and b: "Ex P"
shows "Ex Q"
- using a b by (metis)
+ using a b by metis
lemma ball_reg:
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
@@ -366,12 +373,14 @@
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
lemma ball_all_comm:
- "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
- by auto
+ assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
+ shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
+ using assms by auto
lemma bex_ex_comm:
- "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
- by auto
+ assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
+ shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
+ using assms by auto
section {* Bounded abstraction *}
@@ -384,7 +393,7 @@
assumes q: "Quotient R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g"
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
- apply (auto simp add: Babs_def)
+ apply (auto simp add: Babs_def in_respects)
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
using a apply (simp add: Babs_def)
apply (simp add: in_respects)