theory QuotScript+
−
imports Plain ATP_Linkup+
−
begin+
−
+
−
definition +
−
  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)" +
−
+
−
definition+
−
  "reflp E \<equiv> \<forall>x. E x x"+
−
+
−
definition +
−
  "symp E \<equiv> \<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"+
−
+
−
lemma equivp_reflp_symp_transp:+
−
  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"+
−
unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq+
−
by (blast)+
−
+
−
lemma equivp_refl:+
−
  shows "equivp R \<Longrightarrow> (\<And>x. R x x)"+
−
  by (simp add: equivp_reflp_symp_transp reflp_def)+
−
+
−
lemma equivp_reflp:+
−
  shows "equivp E \<Longrightarrow> (\<And>x. E x x)"+
−
  by (simp add: equivp_reflp_symp_transp reflp_def)+
−
+
−
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)))"+
−
+
−
lemma equivp_IMP_PART_equivp:+
−
  assumes a: "equivp E"+
−
  shows "PART_equivp E"+
−
using a unfolding equivp_def PART_equivp_def+
−
by auto+
−
+
−
definition+
−
  "Quotient E Abs Rep \<equiv> (\<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)))"+
−
+
−
lemma Quotient_ABS_REP:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows "Abs (Rep a) = a" +
−
using a unfolding Quotient_def+
−
by simp+
−
+
−
lemma Quotient_REP_reflp:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows "E (Rep a) (Rep a)" +
−
using a unfolding Quotient_def+
−
by blast+
−
+
−
lemma Quotient_REL:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"+
−
using a unfolding Quotient_def+
−
by blast+
−
+
−
lemma Quotient_REL_ABS:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows "E r s \<Longrightarrow> Abs r = Abs s"+
−
using a unfolding Quotient_def+
−
by blast+
−
+
−
lemma Quotient_REL_ABS_EQ:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"+
−
using a unfolding Quotient_def+
−
by blast+
−
+
−
lemma Quotient_REL_REP:+
−
  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 R Abs Rep"+
−
  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"+
−
using a unfolding Quotient_def+
−
by blast+
−
+
−
lemma IDENTITY_equivp:+
−
  shows "equivp (op =)"+
−
unfolding equivp_def+
−
by auto+
−
+
−
lemma IDENTITY_Quotient:+
−
  shows "Quotient (op =) id id"+
−
unfolding Quotient_def id_def+
−
by blast+
−
+
−
lemma Quotient_symp:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows "symp E"+
−
using a unfolding Quotient_def symp_def+
−
by metis+
−
+
−
lemma Quotient_transp:+
−
  assumes a: "Quotient E Abs Rep"+
−
  shows "transp E"+
−
using a unfolding Quotient_def transp_def+
−
by metis+
−
+
−
fun+
−
  prod_rel+
−
where+
−
  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"+
−
+
−
fun+
−
  fun_map+
−
where+
−
  "fun_map f g h x = g (h (f x))"+
−
+
−
+
−
abbreviation+
−
  fun_map_syn (infixr "--->" 55)+
−
where+
−
  "f ---> g \<equiv> fun_map f g"+
−
+
−
lemma FUN_MAP_I:+
−
  shows "(id ---> id) = id"+
−
by (simp add: expand_fun_eq id_def)+
−
+
−
lemma IN_FUN:+
−
  shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"+
−
by (simp add: mem_def)+
−
+
−
fun+
−
  FUN_REL +
−
where+
−
  "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"+
−
+
−
abbreviation+
−
  FUN_REL_syn (infixr "===>" 55)+
−
where+
−
  "E1 ===> E2 \<equiv> FUN_REL E1 E2"+
−
+
−
lemma FUN_REL_EQ:+
−
  "(op =) ===> (op =) \<equiv> (op =)"+
−
by (rule eq_reflection) (simp add: expand_fun_eq)+
−
+
−
lemma FUN_Quotient:+
−
  assumes q1: "Quotient R1 abs1 rep1"+
−
  and     q2: "Quotient R2 abs2 rep2"+
−
  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+
−
  moreover+
−
  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"+
−
    apply(auto)+
−
    using q1 q2 unfolding Quotient_def+
−
    apply(metis)+
−
    done+
−
  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)+
−
    using q1 q2 unfolding Quotient_def+
−
    apply(metis)+
−
    using q1 q2 unfolding Quotient_def+
−
    apply(metis)+
−
    using q1 q2 unfolding Quotient_def+
−
    apply(metis)+
−
    using q1 q2 unfolding Quotient_def+
−
    apply(metis)+
−
    done+
−
  ultimately+
−
  show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"+
−
    unfolding Quotient_def by blast+
−
qed+
−
+
−
definition+
−
  Respects+
−
where+
−
  "Respects R x \<equiv> (R x x)"+
−
+
−
lemma IN_RESPECTS:+
−
  shows "(x \<in> Respects R) = R x x"+
−
unfolding mem_def Respects_def by simp+
−
+
−
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_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_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_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+
−
+
−
(*+
−
definition+
−
  "RES_EXISTS_EQUIV 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)"+
−
*)+
−
+
−
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+
−
+
−
(* 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"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"+
−
by simp+
−
+
−
lemma FUN_REL_IMP:+
−
  shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"+
−
by simp+
−
+
−
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)+
−
using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def+
−
apply(metis FUN_REL_IMP)+
−
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)+
−
+
−
(* 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 (rule Quotient_REL_REP[OF q, symmetric])+
−
+
−
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+
−
+
−
lemma lambda_prs:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"+
−
unfolding expand_fun_eq+
−
using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]+
−
by simp+
−
+
−
lemma lambda_prs1:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"+
−
unfolding expand_fun_eq+
−
using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]+
−
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"+
−
  shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"+
−
unfolding expand_fun_eq+
−
using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]+
−
by simp+
−
+
−
(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)+
−
lemma LAMBDA_RSP:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  and     a: "(R1 ===> R2) f1 f2"+
−
  shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"+
−
by (rule a)+
−
+
−
(* ASK Peter about next four lemmas in quotientScript+
−
lemma ABSTRACT_PRS:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  shows "f = (Rep1 ---> Abs2) ???"+
−
*)+
−
+
−
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+
−
+
−
lemma REP_ABS_RSP:+
−
  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_reflp[OF q])+
−
+
−
(* Not used *)+
−
lemma REP_ABS_RSP_LEFT:+
−
  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_reflp[OF q])+
−
+
−
(* ----------------------------------------------------- *)+
−
(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)+
−
(*              Ball, Bex, RES_EXISTS_EQUIV              *)+
−
(* ----------------------------------------------------- *)+
−
+
−
(* bool theory: COND, LET *)+
−
+
−
lemma IF_PRS:+
−
  assumes q: "Quotient R Abs Rep"+
−
  shows "If a b c = Abs (If a (Rep b) (Rep c))"+
−
using Quotient_ABS_REP[OF q] by auto+
−
+
−
(* ask peter: no use of q *)+
−
lemma IF_RSP:+
−
  assumes q: "Quotient R Abs Rep"+
−
  and     a: "a1 = a2" "R b1 b2" "R c1 c2"+
−
  shows "R (If a1 b1 c1) (If a2 b2 c2)"+
−
using a by auto+
−
+
−
lemma LET_PRS:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"+
−
using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto+
−
+
−
lemma LET_RSP:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  and     a1: "(R1 ===> R2) f g"+
−
  and     a2: "R1 x y"+
−
  shows "R2 (Let x f) (Let y g)"+
−
using FUN_REL_MP[OF q1 q2 a1] a2+
−
by auto+
−
+
−
+
−
(* ask peter what are literal_case *)+
−
(* literal_case_PRS *)+
−
(* literal_case_RSP *)+
−
+
−
+
−
(* FUNCTION APPLICATION *)+
−
+
−
(* Not used *)+
−
lemma APPLY_PRS:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"+
−
using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto+
−
+
−
(* 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 R2 that+
−
   will be provable; which is why we need to use APPLY_RSP *)+
−
lemma apply_rsp:+
−
  assumes q: "Quotient R1 Abs1 Rep1"+
−
  and     a: "(R1 ===> R2) f g" "R1 x y"+
−
  shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"+
−
using a by (rule FUN_REL_IMP)+
−
+
−
lemma apply_rsp':+
−
  assumes a: "(R1 ===> R2) f g" "R1 x y"+
−
  shows "R2 (f x) (g y)"+
−
using a by (rule FUN_REL_IMP)+
−
+
−
+
−
(* 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))"+
−
using Quotient_ABS_REP[OF q] by auto+
−
+
−
lemma I_RSP:+
−
  assumes q: "Quotient R Abs Rep"+
−
  and     a: "R e1 e2"+
−
  shows "R (id e1) (id e2)"+
−
using a by auto+
−
+
−
lemma o_PRS:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  and     q3: "Quotient R3 Abs3 Rep3"+
−
  shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"+
−
using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] Quotient_ABS_REP[OF q3]+
−
unfolding o_def expand_fun_eq+
−
by simp+
−
+
−
lemma o_RSP:+
−
  assumes q1: "Quotient R1 Abs1 Rep1"+
−
  and     q2: "Quotient R2 Abs2 Rep2"+
−
  and     q3: "Quotient R3 Abs3 Rep3"+
−
  and     a1: "(R2 ===> R3) f1 f2"+
−
  and     a2: "(R1 ===> R2) g1 g2"+
−
  shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"+
−
using a1 a2 unfolding o_def expand_fun_eq+
−
by (auto)+
−
+
−
+
−
+
−
+
−
+
−
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"+
−
  assumes a: "equivp R"+
−
  shows "Ball (Respects R) P = (All P)"+
−
  by (metis equivp_def IN_RESPECTS a)+
−
+
−
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)+
−
+
−
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)+
−
+
−
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)+
−
+
−
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)+
−
+
−
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)+
−
+
−
lemma ball_reg_eqv_range:+
−
  fixes P::"'a \<Rightarrow> bool"+
−
  and x::"'a"+
−
  assumes a: "equivp R2"+
−
  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"+
−
  apply(rule iffI)+
−
  apply(rule allI)+
−
  apply(drule_tac x="\<lambda>y. f x" in bspec)+
−
  apply(simp add: Respects_def IN_RESPECTS)+
−
  apply(rule impI)+
−
  using a equivp_reflp_symp_transp[of "R2"]+
−
  apply(simp add: reflp_def)+
−
  apply(simp)+
−
  apply(simp)+
−
  done+
−
+
−
lemma bex_reg_eqv_range:+
−
  fixes P::"'a \<Rightarrow> bool"+
−
  and x::"'a"+
−
  assumes a: "equivp R2"+
−
  shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"+
−
  apply(auto)+
−
  apply(rule_tac x="\<lambda>y. f x" in bexI)+
−
  apply(simp)+
−
  apply(simp add: Respects_def IN_RESPECTS)+
−
  apply(rule impI)+
−
  using a equivp_reflp_symp_transp[of "R2"]+
−
  apply(simp add: reflp_def)+
−
  done+
−
+
−
lemma all_reg:+
−
  assumes a: "!x :: 'a. (P x --> Q x)"+
−
  and     b: "All P"+
−
  shows "All Q"+
−
  using a b by (metis)+
−
+
−
lemma ex_reg:+
−
  assumes a: "!x :: 'a. (P x --> Q x)"+
−
  and     b: "Ex P"+
−
  shows "Ex Q"+
−
  using a b by (metis)+
−
+
−
lemma ball_reg:+
−
  assumes a: "!x :: 'a. (R x --> P x --> Q x)"+
−
  and     b: "Ball R P"+
−
  shows "Ball R Q"+
−
  using a b by (metis COMBC_def Collect_def Collect_mem_eq)+
−
+
−
lemma bex_reg:+
−
  assumes a: "!x :: 'a. (R x --> P x --> Q x)"+
−
  and     b: "Bex R P"+
−
  shows "Bex R Q"+
−
  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+
−
+
−
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+
−
+
−
(* 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 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)+
−
+
−
(* 2 lemmas needed for cleaning of quantifiers *)+
−
lemma all_prs:+
−
  assumes a: "Quotient R absf repf"+
−
  shows "Ball (Respects R) ((absf ---> id) f) = All f"+
−
  using a unfolding Quotient_def+
−
  by (metis IN_RESPECTS fun_map.simps id_apply)+
−
+
−
lemma ex_prs:+
−
  assumes a: "Quotient R absf repf"+
−
  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+
−
+
−