--- a/Quot/QuotBase.thy Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotBase.thy Wed Feb 10 17:02:29 2010 +0100
@@ -3,7 +3,7 @@
*)
theory QuotBase
-imports Plain ATP_Linkup Predicate
+imports Plain ATP_Linkup
begin
text {*
@@ -11,17 +11,18 @@
that are represented by predicates.
*}
+(* TODO check where definitions can be changed to \<longleftrightarrow> *)
definition
- "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
+ "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
definition
- "reflp E \<equiv> \<forall>x. E x x"
+ "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
definition
- "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+ "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
definition
- "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+ "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
lemma equivp_reflp_symp_transp:
shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
@@ -29,15 +30,15 @@
by blast
lemma equivp_reflp:
- shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
+ shows "equivp E \<Longrightarrow> E x x"
by (simp only: equivp_reflp_symp_transp reflp_def)
lemma equivp_symp:
- shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
+ shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
by (metis equivp_reflp_symp_transp symp_def)
lemma equivp_transp:
- shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
+ shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
by (metis equivp_reflp_symp_transp transp_def)
lemma equivpI:
@@ -57,7 +58,7 @@
text {* Partial equivalences: not yet used anywhere *}
definition
- "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
+ "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))"
lemma equivp_implies_part_equivp:
assumes a: "equivp E"
@@ -81,7 +82,7 @@
definition
Respects
where
- "Respects R x \<equiv> (R x x)"
+ "Respects R x \<longleftrightarrow> (R x x)"
lemma in_respects:
shows "(x \<in> Respects R) = R x x"
@@ -123,7 +124,7 @@
section {* Quotient Predicate *}
definition
- "Quotient E Abs Rep \<equiv>
+ "Quotient E Abs Rep \<longleftrightarrow>
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
@@ -378,7 +379,7 @@
definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
- "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+ "x \<in> p \<Longrightarrow> Babs p m x = m x"
lemma babs_rsp:
assumes q: "Quotient R1 Abs1 Rep1"
@@ -456,7 +457,7 @@
definition
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
where
- "Bex1_rel R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+ "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
lemma bex1_rel_aux:
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
@@ -613,102 +614,5 @@
shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
using apply_rsp[OF q1 a1] a2 by auto
-
-(*** REST OF THE FILE IS UNUSED (until now) ***)
-
-text {*
-lemma in_fun:
- shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
- by (simp add: mem_def)
-
-lemma respects_thm:
- shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
- unfolding Respects_def
- by (simp add: expand_fun_eq)
-
-lemma respects_rep_abs:
- assumes a: "Quotient R1 Abs1 Rep1"
- and b: "Respects (R1 ===> R2) f"
- and c: "R1 x x"
- shows "R2 (f (Rep1 (Abs1 x))) (f x)"
- using a b[simplified respects_thm] c unfolding Quotient_def
- by blast
-
-lemma respects_mp:
- assumes a: "Respects (R1 ===> R2) f"
- and b: "R1 x y"
- shows "R2 (f x) (f y)"
- using a b unfolding Respects_def
- by simp
-
-lemma respects_o:
- assumes a: "Respects (R2 ===> R3) f"
- and b: "Respects (R1 ===> R2) g"
- shows "Respects (R1 ===> R3) (f o g)"
- using a b unfolding Respects_def
- by simp
-
-lemma fun_rel_eq_rel:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
- \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
- using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
- by blast
-
-lemma let_babs:
- "v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"
- by (simp add: Babs_def)
-
-lemma fun_rel_equals:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- and r1: "Respects (R1 ===> R2) f"
- and r2: "Respects (R1 ===> R2) g"
- shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
- apply(rule_tac iffI)
- apply(rule)+
- apply (rule apply_rsp'[of "R1" "R2"])
- apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
- apply auto
- using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
- apply (metis let_rsp q1)
- apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
- using r1 unfolding Respects_def expand_fun_eq
- apply(simp (no_asm_use))
- apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
- done
-
-(* ask Peter: fun_rel_IMP used twice *)
-lemma fun_rel_IMP2:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- and r1: "Respects (R1 ===> R2) f"
- and r2: "Respects (R1 ===> R2) g"
- and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
- shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
- using q1 q2 r1 r2 a
- by (simp add: fun_rel_equals)
-
-lemma lambda_rep_abs_rsp:
- assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
- and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
- shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
- using r1 r2 by auto
-
-(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
-lemma id_prs:
- assumes q: "Quotient R Abs Rep"
- shows "Abs (id (Rep e)) = id e"
- using Quotient_abs_rep[OF q] by auto
-
-lemma id_rsp:
- assumes q: "Quotient R Abs Rep"
- and a: "R e1 e2"
- shows "R (id e1) (id e2)"
- using a by auto
-
-*}
-
end