--- a/QuotScript.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/QuotScript.thy Mon Nov 30 13:58:05 2009 +0100
@@ -68,14 +68,14 @@
by blast
lemma QUOTIENT_REL_REP:
- assumes a: "QUOTIENT E Abs Rep"
- shows "E (Rep a) (Rep b) = (a = b)"
+ assumes a: "QUOTIENT R Abs Rep"
+ shows "R (Rep a) (Rep b) = (a = b)"
using a unfolding QUOTIENT_def
by metis
lemma QUOTIENT_REP_ABS:
- assumes a: "QUOTIENT E Abs Rep"
- shows "E r r \<Longrightarrow> E (Rep (Abs r)) r"
+ assumes a: "QUOTIENT R Abs Rep"
+ shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
using a unfolding QUOTIENT_def
by blast
@@ -223,6 +223,7 @@
using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
by blast
+(* TODO: it is the same as APPLY_RSP *)
(* q1 and q2 not used; see next lemma *)
lemma FUN_REL_MP:
assumes q1: "QUOTIENT R1 Abs1 Rep1"
@@ -259,10 +260,11 @@
using q1 q2 r1 r2 a
by (simp add: FUN_REL_EQUALS)
+(* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *)
lemma EQUALS_PRS:
assumes q: "QUOTIENT R Abs Rep"
shows "(x = y) = R (Rep x) (Rep y)"
-by (simp add: QUOTIENT_REL_REP[OF q])
+by (rule QUOTIENT_REL_REP[OF q, symmetric])
lemma EQUALS_RSP:
assumes q: "QUOTIENT R Abs Rep"
@@ -285,8 +287,9 @@
shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
unfolding expand_fun_eq
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
-by (simp)
+by simp
+(* Not used since applic_prs proves a version for an arbitrary number of arguments *)
lemma APP_PRS:
assumes q1: "QUOTIENT R1 abs1 rep1"
and q2: "QUOTIENT R2 abs2 rep2"
@@ -320,25 +323,21 @@
assumes q: "QUOTIENT R Abs Rep"
and a: "R x1 x2"
shows "R x1 (Rep (Abs x2))"
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+
+(* Not used *)
+lemma REP_ABS_RSP_LEFT:
+ assumes q: "QUOTIENT R Abs Rep"
+ and a: "R x1 x2"
and "R (Rep (Abs x1)) x2"
-proof -
- show "R x1 (Rep (Abs x2))"
- using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
-next
- show "R (Rep (Abs x1)) x2"
- using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
-qed
+ shows "R x1 (Rep (Abs x2))"
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
(* ----------------------------------------------------- *)
(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *)
(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
(* ----------------------------------------------------- *)
-(* what is RES_FORALL *)
-(*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
- !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*)
-(*as peter here *)
-
(* bool theory: COND, LET *)
lemma IF_PRS:
@@ -398,6 +397,7 @@
(* combinators: I, K, o, C, W *)
+(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
lemma I_PRS:
assumes q: "QUOTIENT R Abs Rep"
shows "id e = Abs (id (Rep e))"
@@ -430,6 +430,17 @@
+
+
+lemma COND_PRS:
+ assumes a: "QUOTIENT R absf repf"
+ shows "(if a then b else c) = absf (if a then repf b else repf c)"
+ using a unfolding QUOTIENT_def by auto
+
+
+
+
+
(* Set of lemmas for regularisation of ball and bex *)
lemma ball_reg_eqv:
fixes P :: "'a \<Rightarrow> bool"
@@ -525,49 +536,29 @@
"((\<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
-
-
-(* TODO: Add similar *)
-lemma RES_FORALL_RSP:
- shows "\<And>f g. (R ===> (op =)) f g ==>
- (Ball (Respects R) f = Ball (Respects R) g)"
- apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
- done
+(* 2 lemmas needed for proving repabs_inj *)
+lemma ball_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "Ball (Respects R) f = Ball (Respects R) g"
+ using a by (simp add: Ball_def IN_RESPECTS)
-lemma RES_EXISTS_RSP:
- shows "\<And>f g. (R ===> (op =)) f g ==>
- (Bex (Respects R) f = Bex (Respects R) g)"
- apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
- done
+lemma bex_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "(Bex (Respects R) f = Bex (Respects R) g)"
+ using a by (simp add: Bex_def IN_RESPECTS)
-
-lemma FORALL_PRS:
+(* 2 lemmas needed for cleaning of quantifiers *)
+lemma all_prs:
assumes a: "QUOTIENT R absf repf"
- shows "All f = Ball (Respects R) ((absf ---> id) f)"
- using a
- unfolding QUOTIENT_def
+ shows "Ball (Respects R) ((absf ---> id) f) = All f"
+ using a unfolding QUOTIENT_def
by (metis IN_RESPECTS fun_map.simps id_apply)
-lemma EXISTS_PRS:
- assumes a: "QUOTIENT R absf repf"
- shows "Ex f = Bex (Respects R) ((absf ---> id) f)"
- using a
- unfolding QUOTIENT_def
- by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
-
-lemma COND_PRS:
+lemma ex_prs:
assumes a: "QUOTIENT R absf repf"
- shows "(if a then b else c) = absf (if a then repf b else repf c)"
- using a unfolding QUOTIENT_def by auto
-
-(* These are the fixed versions, general ones need to be proved. *)
-lemma ho_all_prs:
- shows "((op = ===> op =) ===> op =) All All"
- by auto
-
-lemma ho_ex_prs:
- shows "((op = ===> op =) ===> op =) Ex Ex"
- by auto
+ shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+ using a unfolding QUOTIENT_def
+ by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
end