Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotScript.thy
changeset 528 f51e2b3e3149
parent 527 9b1ad366827f
child 530 5e92ce8f306d
equal deleted inserted replaced
527:9b1ad366827f 528:f51e2b3e3149 
     1 theory QuotScript
 
     1 theory QuotScript
 
     2 imports Main
 
     2 imports Main
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 definition 
     5 definition 
     6   "EQUIV E \<equiv> \<forall>x y. E x y = (E x = E y)" 
     6   "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)" 
     7 
     7 
     8 definition
 
     8 definition
 
     9   "REFL E \<equiv> \<forall>x. E x x"
 
     9   "reflp E \<equiv> \<forall>x. E x x"
 
    10 
    10 
    11 definition 
    11 definition 
    12   "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
 
    12   "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
 
    13 
    13 
    14 definition
 
    14 definition
 
    15   "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
 
    15   "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
 
    16 
    16 
    17 lemma EQUIV_REFL_SYM_TRANS:
 
    17 lemma equivp_reflp_symp_transp:
 
    18   shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)"
 
    18   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
 
    19 unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq
 
    19 unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
 
    20 by (blast)
 
    20 by (blast)
 
    21 
    21 
    22 lemma EQUIV_REFL:
 
    22 lemma equivp_refl:
 
    23   shows "EQUIV E \<Longrightarrow> (\<And>x. E x x)"
 
    23   shows "equivp R \<Longrightarrow> (\<And>x. R x x)"
 
    24   by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
 
    24   by (simp add: equivp_reflp_symp_transp reflp_def)
 
       
    25 
       
    26 lemma equivp_reflp:
 
       
    27   shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
 
       
    28   by (simp add: equivp_reflp_symp_transp reflp_def)
 
    25 
    29 
    26 definition
 
    30 definition
 
    27   "PART_EQUIV 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)))"
 
    31   "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)))"
 
    28 
    32 
    29 lemma EQUIV_IMP_PART_EQUIV:
 
    33 lemma equivp_IMP_PART_equivp:
 
    30   assumes a: "EQUIV E"
 
    34   assumes a: "equivp E"
 
    31   shows "PART_EQUIV E"
 
    35   shows "PART_equivp E"
 
    32 using a unfolding EQUIV_def PART_EQUIV_def
 
    36 using a unfolding equivp_def PART_equivp_def
 
    33 by auto
 
    37 by auto
 
    34 
    38 
    35 definition
 
    39 definition
 
    36   "QUOTIENT E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
    40   "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
    37                         (\<forall>a. E (Rep a) (Rep a)) \<and> 
    41                         (\<forall>a. E (Rep a) (Rep a)) \<and> 
    38                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
    42                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
    39 
    43 
    40 lemma QUOTIENT_ABS_REP:
 
    44 lemma Quotient_ABS_REP:
 
    41   assumes a: "QUOTIENT E Abs Rep"
 
    45   assumes a: "Quotient E Abs Rep"
 
    42   shows "Abs (Rep a) = a" 
    46   shows "Abs (Rep a) = a" 
    43 using a unfolding QUOTIENT_def
 
    47 using a unfolding Quotient_def
 
    44 by simp
 
    48 by simp
 
    45 
    49 
    46 lemma QUOTIENT_REP_REFL:
 
    50 lemma Quotient_REP_reflp:
 
    47   assumes a: "QUOTIENT E Abs Rep"
 
    51   assumes a: "Quotient E Abs Rep"
 
    48   shows "E (Rep a) (Rep a)" 
    52   shows "E (Rep a) (Rep a)" 
    49 using a unfolding QUOTIENT_def
 
    53 using a unfolding Quotient_def
 
    50 by blast
 
    54 by blast
 
    51 
    55 
    52 lemma QUOTIENT_REL:
 
    56 lemma Quotient_REL:
 
    53   assumes a: "QUOTIENT E Abs Rep"
 
    57   assumes a: "Quotient E Abs Rep"
 
    54   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
 
    58   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
 
    55 using a unfolding QUOTIENT_def
 
    59 using a unfolding Quotient_def
 
    56 by blast
 
    60 by blast
 
    57 
    61 
    58 lemma QUOTIENT_REL_ABS:
 
    62 lemma Quotient_REL_ABS:
 
    59   assumes a: "QUOTIENT E Abs Rep"
 
    63   assumes a: "Quotient E Abs Rep"
 
    60   shows "E r s \<Longrightarrow> Abs r = Abs s"
 
    64   shows "E r s \<Longrightarrow> Abs r = Abs s"
 
    61 using a unfolding QUOTIENT_def
 
    65 using a unfolding Quotient_def
 
    62 by blast
 
    66 by blast
 
    63 
    67 
    64 lemma QUOTIENT_REL_ABS_EQ:
 
    68 lemma Quotient_REL_ABS_EQ:
 
    65   assumes a: "QUOTIENT E Abs Rep"
 
    69   assumes a: "Quotient E Abs Rep"
 
    66   shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
 
    70   shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
 
    67 using a unfolding QUOTIENT_def
 
    71 using a unfolding Quotient_def
 
    68 by blast
 
    72 by blast
 
    69 
    73 
    70 lemma QUOTIENT_REL_REP:
 
    74 lemma Quotient_REL_REP:
 
    71   assumes a: "QUOTIENT R Abs Rep"
 
    75   assumes a: "Quotient R Abs Rep"
 
    72   shows "R (Rep a) (Rep b) = (a = b)"
 
    76   shows "R (Rep a) (Rep b) = (a = b)"
 
    73 using a unfolding QUOTIENT_def
 
    77 using a unfolding Quotient_def
 
    74 by metis
 
    78 by metis
 
    75 
    79 
    76 lemma QUOTIENT_REP_ABS:
 
    80 lemma Quotient_REP_ABS:
 
    77   assumes a: "QUOTIENT R Abs Rep"
 
    81   assumes a: "Quotient R Abs Rep"
 
    78   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
 
    82   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
 
    79 using a unfolding QUOTIENT_def
 
    83 using a unfolding Quotient_def
 
    80 by blast
 
    84 by blast
 
    81 
    85 
    82 lemma IDENTITY_EQUIV:
 
    86 lemma IDENTITY_equivp:
 
    83   shows "EQUIV (op =)"
 
    87   shows "equivp (op =)"
 
    84 unfolding EQUIV_def
 
    88 unfolding equivp_def
 
    85 by auto
 
    89 by auto
 
    86 
    90 
    87 lemma IDENTITY_QUOTIENT:
 
    91 lemma IDENTITY_Quotient:
 
    88   shows "QUOTIENT (op =) id id"
 
    92   shows "Quotient (op =) id id"
 
    89 unfolding QUOTIENT_def id_def
 
    93 unfolding Quotient_def id_def
 
    90 by blast
 
    94 by blast
 
    91 
    95 
    92 lemma QUOTIENT_SYM:
 
    96 lemma Quotient_symp:
 
    93   assumes a: "QUOTIENT E Abs Rep"
 
    97   assumes a: "Quotient E Abs Rep"
 
    94   shows "SYM E"
 
    98   shows "symp E"
 
    95 using a unfolding QUOTIENT_def SYM_def
 
    99 using a unfolding Quotient_def symp_def
 
    96 by metis
 
   100 by metis
 
    97 
   101 
    98 lemma QUOTIENT_TRANS:
 
   102 lemma Quotient_transp:
 
    99   assumes a: "QUOTIENT E Abs Rep"
 
   103   assumes a: "Quotient E Abs Rep"
 
   100   shows "TRANS E"
 
   104   shows "transp E"
 
   101 using a unfolding QUOTIENT_def TRANS_def
 
   105 using a unfolding Quotient_def transp_def
 
   102 by metis
 
   106 by metis
 
   103 
   107 
   104 fun
 
   108 fun
 
   105   prod_rel
 
   109   prod_rel
 
   106 where
 
   110 where
 
   137 
   141 
   138 lemma FUN_REL_EQ:
 
   142 lemma FUN_REL_EQ:
 
   139   "(op =) ===> (op =) \<equiv> (op =)"
 
   143   "(op =) ===> (op =) \<equiv> (op =)"
 
   140 by (rule eq_reflection) (simp add: expand_fun_eq)
 
   144 by (rule eq_reflection) (simp add: expand_fun_eq)
 
   141 
   145 
   142 lemma FUN_QUOTIENT:
 
   146 lemma FUN_Quotient:
 
   143   assumes q1: "QUOTIENT R1 abs1 rep1"
 
   147   assumes q1: "Quotient R1 abs1 rep1"
 
   144   and     q2: "QUOTIENT R2 abs2 rep2"
 
   148   and     q2: "Quotient R2 abs2 rep2"
 
   145   shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
 
   149   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
 
   146 proof -
 
   150 proof -
 
   147   have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
 
   151   have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
 
   148     apply(simp add: expand_fun_eq)
 
   152     apply(simp add: expand_fun_eq)
 
   149     using q1 q2
 
   153     using q1 q2
 
   150     apply(simp add: QUOTIENT_def)
 
   154     apply(simp add: Quotient_def)
 
   151     done
 
   155     done
 
   152   moreover
 
   156   moreover
 
   153   have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
 
   157   have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
 
   154     apply(auto)
 
   158     apply(auto)
 
   155     using q1 q2 unfolding QUOTIENT_def
 
   159     using q1 q2 unfolding Quotient_def
 
   156     apply(metis)
 
   160     apply(metis)
 
   157     done
 
   161     done
 
   158   moreover
 
   162   moreover
 
   159   have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 
   163   have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 
   160         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
 
   164         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
 
   161     apply(auto simp add: expand_fun_eq)
 
   165     apply(auto simp add: expand_fun_eq)
 
   162     using q1 q2 unfolding QUOTIENT_def
 
   166     using q1 q2 unfolding Quotient_def
 
   163     apply(metis)
 
   167     apply(metis)
 
   164     using q1 q2 unfolding QUOTIENT_def
 
   168     using q1 q2 unfolding Quotient_def
 
   165     apply(metis)
 
   169     apply(metis)
 
   166     using q1 q2 unfolding QUOTIENT_def
 
   170     using q1 q2 unfolding Quotient_def
 
   167     apply(metis)
 
   171     apply(metis)
 
   168     using q1 q2 unfolding QUOTIENT_def
 
   172     using q1 q2 unfolding Quotient_def
 
   169     apply(metis)
 
   173     apply(metis)
 
   170     done
 
   174     done
 
   171   ultimately
 
   175   ultimately
 
   172   show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
 
   176   show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
 
   173     unfolding QUOTIENT_def by blast
 
   177     unfolding Quotient_def by blast
 
   174 qed
 
   178 qed
 
   175 
   179 
   176 definition
 
   180 definition
 
   177   Respects
 
   181   Respects
 
   178 where
 
   182 where
 
   193   shows "R2 (f x) (f y)"
 
   197   shows "R2 (f x) (f y)"
 
   194 using a b unfolding Respects_def
 
   198 using a b unfolding Respects_def
 
   195 by simp
 
   199 by simp
 
   196 
   200 
   197 lemma RESPECTS_REP_ABS:
 
   201 lemma RESPECTS_REP_ABS:
 
   198   assumes a: "QUOTIENT R1 Abs1 Rep1"
 
   202   assumes a: "Quotient R1 Abs1 Rep1"
 
   199   and     b: "Respects (R1 ===> R2) f"
 
   203   and     b: "Respects (R1 ===> R2) f"
 
   200   and     c: "R1 x x"
 
   204   and     c: "R1 x x"
 
   201   shows "R2 (f (Rep1 (Abs1 x))) (f x)"
 
   205   shows "R2 (f (Rep1 (Abs1 x))) (f x)"
 
   202 using a b[simplified RESPECTS_THM] c unfolding QUOTIENT_def
 
   206 using a b[simplified RESPECTS_THM] c unfolding Quotient_def
 
   203 by blast
 
   207 by blast
 
   204 
   208 
   205 lemma RESPECTS_o:
 
   209 lemma RESPECTS_o:
 
   206   assumes a: "Respects (R2 ===> R3) f"
 
   210   assumes a: "Respects (R2 ===> R3) f"
 
   207   and     b: "Respects (R1 ===> R2) g"
 
   211   and     b: "Respects (R1 ===> R2) g"
 
   214   "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> 
   218   "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> 
   215                           (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
 
   219                           (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
 
   216 *)
 
   220 *)
 
   217 
   221 
   218 lemma FUN_REL_EQ_REL:
 
   222 lemma FUN_REL_EQ_REL:
 
   219   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   223   assumes q1: "Quotient R1 Abs1 Rep1"
 
   220   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   224   and     q2: "Quotient R2 Abs2 Rep2"
 
   221   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 
   225   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 
   222                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
 
   226                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
 
   223 using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
 
   227 using FUN_Quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
 
   224 by blast
 
   228 by blast
 
   225 
   229 
   226 (* TODO: it is the same as APPLY_RSP *)
 
   230 (* TODO: it is the same as APPLY_RSP *)
 
   227 (* q1 and q2 not used; see next lemma *)
 
   231 (* q1 and q2 not used; see next lemma *)
 
   228 lemma FUN_REL_MP:
 
   232 lemma FUN_REL_MP:
 
   229   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   233   assumes q1: "Quotient R1 Abs1 Rep1"
 
   230   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   234   and     q2: "Quotient R2 Abs2 Rep2"
 
   231   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
   235   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
   232 by simp
 
   236 by simp
 
   233 
   237 
   234 lemma FUN_REL_IMP:
 
   238 lemma FUN_REL_IMP:
 
   235   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
   239   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
   236 by simp
 
   240 by simp
 
   237 
   241 
   238 lemma FUN_REL_EQUALS:
 
   242 lemma FUN_REL_EQUALS:
 
   239   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   243   assumes q1: "Quotient R1 Abs1 Rep1"
 
   240   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   244   and     q2: "Quotient R2 Abs2 Rep2"
 
   241   and     r1: "Respects (R1 ===> R2) f"
 
   245   and     r1: "Respects (R1 ===> R2) f"
 
   242   and     r2: "Respects (R1 ===> R2) g" 
   246   and     r2: "Respects (R1 ===> R2) g" 
   243   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 
   247   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 
   244 apply(rule_tac iffI)
 
   248 apply(rule_tac iffI)
 
   245 using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def
 
   249 using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
 
   246 apply(metis FUN_REL_IMP)
 
   250 apply(metis FUN_REL_IMP)
 
   247 using r1 unfolding Respects_def expand_fun_eq
 
   251 using r1 unfolding Respects_def expand_fun_eq
 
   248 apply(simp (no_asm_use))
 
   252 apply(simp (no_asm_use))
 
   249 apply(metis QUOTIENT_REL[OF q2] QUOTIENT_REL_REP[OF q1])
 
   253 apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1])
 
   250 done
 
   254 done
 
   251 
   255 
   252 (* ask Peter: FUN_REL_IMP used twice *) 
   256 (* ask Peter: FUN_REL_IMP used twice *) 
   253 lemma FUN_REL_IMP2:
 
   257 lemma FUN_REL_IMP2:
 
   254   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   258   assumes q1: "Quotient R1 Abs1 Rep1"
 
   255   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   259   and     q2: "Quotient R2 Abs2 Rep2"
 
   256   and     r1: "Respects (R1 ===> R2) f"
 
   260   and     r1: "Respects (R1 ===> R2) f"
 
   257   and     r2: "Respects (R1 ===> R2) g" 
   261   and     r2: "Respects (R1 ===> R2) g" 
   258   and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
 
   262   and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
 
   259   shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
   263   shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
   260 using q1 q2 r1 r2 a
 
   264 using q1 q2 r1 r2 a
 
   261 by (simp add: FUN_REL_EQUALS)
 
   265 by (simp add: FUN_REL_EQUALS)
 
   262 
   266 
   263 (* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *)
 
   267 (* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *)
 
   264 lemma EQUALS_PRS:
 
   268 lemma EQUALS_PRS:
 
   265   assumes q: "QUOTIENT R Abs Rep"
 
   269   assumes q: "Quotient R Abs Rep"
 
   266   shows "(x = y) = R (Rep x) (Rep y)"
 
   270   shows "(x = y) = R (Rep x) (Rep y)"
 
   267 by (rule QUOTIENT_REL_REP[OF q, symmetric])
 
   271 by (rule Quotient_REL_REP[OF q, symmetric])
 
   268 
   272 
   269 lemma equals_rsp:
 
   273 lemma equals_rsp:
 
   270   assumes q: "QUOTIENT R Abs Rep"
 
   274   assumes q: "Quotient R Abs Rep"
 
   271   and     a: "R xa xb" "R ya yb"
 
   275   and     a: "R xa xb" "R ya yb"
 
   272   shows "R xa ya = R xb yb"
 
   276   shows "R xa ya = R xb yb"
 
   273 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
 
   277 using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def
 
   274 using a by blast
 
   278 using a by blast
 
   275 
   279 
   276 lemma lambda_prs:
 
   280 lemma lambda_prs:
 
   277   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   281   assumes q1: "Quotient R1 Abs1 Rep1"
 
   278   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   282   and     q2: "Quotient R2 Abs2 Rep2"
 
   279   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
 
   283   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
 
   280 unfolding expand_fun_eq
 
   284 unfolding expand_fun_eq
 
   281 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
 
   285 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
 
   282 by simp
 
   286 by simp
 
   283 
   287 
   284 lemma lambda_prs1:
 
   288 lemma lambda_prs1:
 
   285   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   289   assumes q1: "Quotient R1 Abs1 Rep1"
 
   286   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   290   and     q2: "Quotient R2 Abs2 Rep2"
 
   287   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
 
   291   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
 
   288 unfolding expand_fun_eq
 
   292 unfolding expand_fun_eq
 
   289 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
 
   293 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
 
   290 by simp
 
   294 by simp
 
   291 
   295 
   292 (* Not used since applic_prs proves a version for an arbitrary number of arguments *)
 
   296 (* Not used since applic_prs proves a version for an arbitrary number of arguments *)
 
   293 lemma APP_PRS:
 
   297 lemma APP_PRS:
 
   294   assumes q1: "QUOTIENT R1 abs1 rep1"
 
   298   assumes q1: "Quotient R1 abs1 rep1"
 
   295   and     q2: "QUOTIENT R2 abs2 rep2"
 
   299   and     q2: "Quotient R2 abs2 rep2"
 
   296   shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
 
   300   shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
 
   297 unfolding expand_fun_eq
 
   301 unfolding expand_fun_eq
 
   298 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
 
   302 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
 
   299 by simp
 
   303 by simp
 
   300 
   304 
   301 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
 
   305 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
 
   302 lemma LAMBDA_RSP:
 
   306 lemma LAMBDA_RSP:
 
   303   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   307   assumes q1: "Quotient R1 Abs1 Rep1"
 
   304   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   308   and     q2: "Quotient R2 Abs2 Rep2"
 
   305   and     a: "(R1 ===> R2) f1 f2"
 
   309   and     a: "(R1 ===> R2) f1 f2"
 
   306   shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"
 
   310   shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"
 
   307 by (rule a)
 
   311 by (rule a)
 
   308 
   312 
   309 (* ASK Peter about next four lemmas in quotientScript
 
   313 (* ASK Peter about next four lemmas in quotientScript
 
   310 lemma ABSTRACT_PRS:
 
   314 lemma ABSTRACT_PRS:
 
   311   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   315   assumes q1: "Quotient R1 Abs1 Rep1"
 
   312   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   316   and     q2: "Quotient R2 Abs2 Rep2"
 
   313   shows "f = (Rep1 ---> Abs2) ???"
 
   317   shows "f = (Rep1 ---> Abs2) ???"
 
   314 *)
 
   318 *)
 
   315 
   319 
   316 lemma LAMBDA_REP_ABS_RSP:
 
   320 lemma LAMBDA_REP_ABS_RSP:
 
   317   assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
 
   321   assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
 
   318   and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
 
   322   and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
 
   319   shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
 
   323   shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
 
   320 using r1 r2 by auto
 
   324 using r1 r2 by auto
 
   321 
   325 
   322 lemma REP_ABS_RSP:
 
   326 lemma REP_ABS_RSP:
 
   323   assumes q: "QUOTIENT R Abs Rep"
 
   327   assumes q: "Quotient R Abs Rep"
 
   324   and     a: "R x1 x2"
 
   328   and     a: "R x1 x2"
 
   325   shows "R x1 (Rep (Abs x2))"
 
   329   shows "R x1 (Rep (Abs x2))"
 
   326 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
 
   330 using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
 
   327 
   331 
   328 (* Not used *)
 
   332 (* Not used *)
 
   329 lemma REP_ABS_RSP_LEFT:
 
   333 lemma REP_ABS_RSP_LEFT:
 
   330   assumes q: "QUOTIENT R Abs Rep"
 
   334   assumes q: "Quotient R Abs Rep"
 
   331   and     a: "R x1 x2"
 
   335   and     a: "R x1 x2"
 
   332   shows "R x1 (Rep (Abs x2))"
 
   336   shows "R x1 (Rep (Abs x2))"
 
   333 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
 
   337 using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
 
   334 
   338 
   335 (* ----------------------------------------------------- *)
 
   339 (* ----------------------------------------------------- *)
 
   336 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
 
   340 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
 
   337 (*              Ball, Bex, RES_EXISTS_EQUIV              *)
 
   341 (*              Ball, Bex, RES_EXISTS_EQUIV              *)
 
   338 (* ----------------------------------------------------- *)
 
   342 (* ----------------------------------------------------- *)
 
   339 
   343 
   340 (* bool theory: COND, LET *)
 
   344 (* bool theory: COND, LET *)
 
   341 
   345 
   342 lemma IF_PRS:
 
   346 lemma IF_PRS:
 
   343   assumes q: "QUOTIENT R Abs Rep"
 
   347   assumes q: "Quotient R Abs Rep"
 
   344   shows "If a b c = Abs (If a (Rep b) (Rep c))"
 
   348   shows "If a b c = Abs (If a (Rep b) (Rep c))"
 
   345 using QUOTIENT_ABS_REP[OF q] by auto
 
   349 using Quotient_ABS_REP[OF q] by auto
 
   346 
   350 
   347 (* ask peter: no use of q *)
 
   351 (* ask peter: no use of q *)
 
   348 lemma IF_RSP:
 
   352 lemma IF_RSP:
 
   349   assumes q: "QUOTIENT R Abs Rep"
 
   353   assumes q: "Quotient R Abs Rep"
 
   350   and     a: "a1 = a2" "R b1 b2" "R c1 c2"
 
   354   and     a: "a1 = a2" "R b1 b2" "R c1 c2"
 
   351   shows "R (If a1 b1 c1) (If a2 b2 c2)"
 
   355   shows "R (If a1 b1 c1) (If a2 b2 c2)"
 
   352 using a by auto
 
   356 using a by auto
 
   353 
   357 
   354 lemma LET_PRS:
 
   358 lemma LET_PRS:
 
   355   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   359   assumes q1: "Quotient R1 Abs1 Rep1"
 
   356   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   360   and     q2: "Quotient R2 Abs2 Rep2"
 
   357   shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"
 
   361   shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"
 
   358 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
 
   362 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto
 
   359 
   363 
   360 lemma LET_RSP:
 
   364 lemma LET_RSP:
 
   361   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   365   assumes q1: "Quotient R1 Abs1 Rep1"
 
   362   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   366   and     q2: "Quotient R2 Abs2 Rep2"
 
   363   and     a1: "(R1 ===> R2) f g"
 
   367   and     a1: "(R1 ===> R2) f g"
 
   364   and     a2: "R1 x y"
 
   368   and     a2: "R1 x y"
 
   365   shows "R2 (Let x f) (Let y g)"
 
   369   shows "R2 (Let x f) (Let y g)"
 
   366 using FUN_REL_MP[OF q1 q2 a1] a2
 
   370 using FUN_REL_MP[OF q1 q2 a1] a2
 
   367 by auto
 
   371 by auto
 
   374 
   378 
   375 (* FUNCTION APPLICATION *)
 
   379 (* FUNCTION APPLICATION *)
 
   376 
   380 
   377 (* Not used *)
 
   381 (* Not used *)
 
   378 lemma APPLY_PRS:
 
   382 lemma APPLY_PRS:
 
   379   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   383   assumes q1: "Quotient R1 Abs1 Rep1"
 
   380   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   384   and     q2: "Quotient R2 Abs2 Rep2"
 
   381   shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
 
   385   shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
 
   382 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
 
   386 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto
 
   383 
   387 
   384 (* In the following theorem R1 can be instantiated with anything,
 
   388 (* In the following theorem R1 can be instantiated with anything,
 
   385    but we know some of the types of the Rep and Abs functions;
 
   389    but we know some of the types of the Rep and Abs functions;
 
   386    so by solving QUOTIENT assumptions we can get a unique R2 that
 
   390    so by solving Quotient assumptions we can get a unique R2 that
 
   387    will be provable; which is why we need to use APPLY_RSP *)
 
   391    will be provable; which is why we need to use APPLY_RSP *)
 
   388 lemma apply_rsp:
 
   392 lemma apply_rsp:
 
   389   assumes q: "QUOTIENT R1 Abs1 Rep1"
 
   393   assumes q: "Quotient R1 Abs1 Rep1"
 
   390   and     a: "(R1 ===> R2) f g" "R1 x y"
 
   394   and     a: "(R1 ===> R2) f g" "R1 x y"
 
   391   shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
 
   395   shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
 
   392 using a by (rule FUN_REL_IMP)
 
   396 using a by (rule FUN_REL_IMP)
 
   393 
   397 
   394 lemma apply_rsp':
 
   398 lemma apply_rsp':
 
   399 
   403 
   400 (* combinators: I, K, o, C, W *)
 
   404 (* combinators: I, K, o, C, W *)
 
   401 
   405 
   402 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
 
   406 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
 
   403 lemma I_PRS:
 
   407 lemma I_PRS:
 
   404   assumes q: "QUOTIENT R Abs Rep"
 
   408   assumes q: "Quotient R Abs Rep"
 
   405   shows "id e = Abs (id (Rep e))"
 
   409   shows "id e = Abs (id (Rep e))"
 
   406 using QUOTIENT_ABS_REP[OF q] by auto
 
   410 using Quotient_ABS_REP[OF q] by auto
 
   407 
   411 
   408 lemma I_RSP:
 
   412 lemma I_RSP:
 
   409   assumes q: "QUOTIENT R Abs Rep"
 
   413   assumes q: "Quotient R Abs Rep"
 
   410   and     a: "R e1 e2"
 
   414   and     a: "R e1 e2"
 
   411   shows "R (id e1) (id e2)"
 
   415   shows "R (id e1) (id e2)"
 
   412 using a by auto
 
   416 using a by auto
 
   413 
   417 
   414 lemma o_PRS:
 
   418 lemma o_PRS:
 
   415   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   419   assumes q1: "Quotient R1 Abs1 Rep1"
 
   416   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   420   and     q2: "Quotient R2 Abs2 Rep2"
 
   417   and     q3: "QUOTIENT R3 Abs3 Rep3"
 
   421   and     q3: "Quotient R3 Abs3 Rep3"
 
   418   shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"
 
   422   shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"
 
   419 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3]
 
   423 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] Quotient_ABS_REP[OF q3]
 
   420 unfolding o_def expand_fun_eq
 
   424 unfolding o_def expand_fun_eq
 
   421 by simp
 
   425 by simp
 
   422 
   426 
   423 lemma o_RSP:
 
   427 lemma o_RSP:
 
   424   assumes q1: "QUOTIENT R1 Abs1 Rep1"
 
   428   assumes q1: "Quotient R1 Abs1 Rep1"
 
   425   and     q2: "QUOTIENT R2 Abs2 Rep2"
 
   429   and     q2: "Quotient R2 Abs2 Rep2"
 
   426   and     q3: "QUOTIENT R3 Abs3 Rep3"
 
   430   and     q3: "Quotient R3 Abs3 Rep3"
 
   427   and     a1: "(R2 ===> R3) f1 f2"
 
   431   and     a1: "(R2 ===> R3) f1 f2"
 
   428   and     a2: "(R1 ===> R2) g1 g2"
 
   432   and     a2: "(R1 ===> R2) g1 g2"
 
   429   shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
 
   433   shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
 
   430 using a1 a2 unfolding o_def expand_fun_eq
 
   434 using a1 a2 unfolding o_def expand_fun_eq
 
   431 by (auto)
 
   435 by (auto)
 
   433 
   437 
   434 
   438 
   435 
   439 
   436 
   440 
   437 lemma COND_PRS:
 
   441 lemma COND_PRS:
 
   438   assumes a: "QUOTIENT R absf repf"
 
   442   assumes a: "Quotient R absf repf"
 
   439   shows "(if a then b else c) = absf (if a then repf b else repf c)"
 
   443   shows "(if a then b else c) = absf (if a then repf b else repf c)"
 
   440   using a unfolding QUOTIENT_def by auto
 
   444   using a unfolding Quotient_def by auto
 
   441 
   445 
   442 
   446 
   443 
   447 
   444 
   448 
   445 
   449 
   446 (* Set of lemmas for regularisation of ball and bex *)
 
   450 (* Set of lemmas for regularisation of ball and bex *)
 
   447 lemma ball_reg_eqv:
 
   451 lemma ball_reg_eqv:
 
   448   fixes P :: "'a \<Rightarrow> bool"
 
   452   fixes P :: "'a \<Rightarrow> bool"
 
   449   assumes a: "EQUIV R"
 
   453   assumes a: "equivp R"
 
   450   shows "Ball (Respects R) P = (All P)"
 
   454   shows "Ball (Respects R) P = (All P)"
 
   451   by (metis EQUIV_def IN_RESPECTS a)
 
   455   by (metis equivp_def IN_RESPECTS a)
 
   452 
   456 
   453 lemma bex_reg_eqv:
 
   457 lemma bex_reg_eqv:
 
   454   fixes P :: "'a \<Rightarrow> bool"
 
   458   fixes P :: "'a \<Rightarrow> bool"
 
   455   assumes a: "EQUIV R"
 
   459   assumes a: "equivp R"
 
   456   shows "Bex (Respects R) P = (Ex P)"
 
   460   shows "Bex (Respects R) P = (Ex P)"
 
   457   by (metis EQUIV_def IN_RESPECTS a)
 
   461   by (metis equivp_def IN_RESPECTS a)
 
   458 
   462 
   459 lemma ball_reg_right:
 
   463 lemma ball_reg_right:
 
   460   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
 
   464   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
 
   461   shows "All P \<longrightarrow> Ball R Q"
 
   465   shows "All P \<longrightarrow> Ball R Q"
 
   462   by (metis COMBC_def Collect_def Collect_mem_eq a)
 
   466   by (metis COMBC_def Collect_def Collect_mem_eq a)
 
   465   assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
 
   469   assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
 
   466   shows "Bex R Q \<longrightarrow> Ex P"
 
   470   shows "Bex R Q \<longrightarrow> Ex P"
 
   467   by (metis COMBC_def Collect_def Collect_mem_eq a)
 
   471   by (metis COMBC_def Collect_def Collect_mem_eq a)
 
   468 
   472 
   469 lemma ball_reg_left:
 
   473 lemma ball_reg_left:
 
   470   assumes a: "EQUIV R"
 
   474   assumes a: "equivp R"
 
   471   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
 
   475   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
 
   472   by (metis EQUIV_REFL IN_RESPECTS a)
 
   476   by (metis equivp_reflp IN_RESPECTS a)
 
   473 
   477 
   474 lemma bex_reg_right:
 
   478 lemma bex_reg_right:
 
   475   assumes a: "EQUIV R"
 
   479   assumes a: "equivp R"
 
   476   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
 
   480   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
 
   477   by (metis EQUIV_REFL IN_RESPECTS a)
 
   481   by (metis equivp_reflp IN_RESPECTS a)
 
   478 
   482 
   479 lemma ball_reg_eqv_range:
 
   483 lemma ball_reg_eqv_range:
 
   480   fixes P::"'a \<Rightarrow> bool"
 
   484   fixes P::"'a \<Rightarrow> bool"
 
   481   and x::"'a"
 
   485   and x::"'a"
 
   482   assumes a: "EQUIV R2"
 
   486   assumes a: "equivp R2"
 
   483   shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
 
   487   shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
 
   484   apply(rule iffI)
 
   488   apply(rule iffI)
 
   485   apply(rule allI)
 
   489   apply(rule allI)
 
   486   apply(drule_tac x="\<lambda>y. f x" in bspec)
 
   490   apply(drule_tac x="\<lambda>y. f x" in bspec)
 
   487   apply(simp add: Respects_def IN_RESPECTS)
 
   491   apply(simp add: Respects_def IN_RESPECTS)
 
   488   apply(rule impI)
 
   492   apply(rule impI)
 
   489   using a EQUIV_REFL_SYM_TRANS[of "R2"]
 
   493   using a equivp_reflp_symp_transp[of "R2"]
 
   490   apply(simp add: REFL_def)
 
   494   apply(simp add: reflp_def)
 
   491   apply(simp)
 
   495   apply(simp)
 
   492   apply(simp)
 
   496   apply(simp)
 
   493   done
 
   497   done
 
   494 
   498 
   495 lemma bex_reg_eqv_range:
 
   499 lemma bex_reg_eqv_range:
 
   496   fixes P::"'a \<Rightarrow> bool"
 
   500   fixes P::"'a \<Rightarrow> bool"
 
   497   and x::"'a"
 
   501   and x::"'a"
 
   498   assumes a: "EQUIV R2"
 
   502   assumes a: "equivp R2"
 
   499   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
 
   503   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
 
   500   apply(auto)
 
   504   apply(auto)
 
   501   apply(rule_tac x="\<lambda>y. f x" in bexI)
 
   505   apply(rule_tac x="\<lambda>y. f x" in bexI)
 
   502   apply(simp)
 
   506   apply(simp)
 
   503   apply(simp add: Respects_def IN_RESPECTS)
 
   507   apply(simp add: Respects_def IN_RESPECTS)
 
   504   apply(rule impI)
 
   508   apply(rule impI)
 
   505   using a EQUIV_REFL_SYM_TRANS[of "R2"]
 
   509   using a equivp_reflp_symp_transp[of "R2"]
 
   506   apply(simp add: REFL_def)
 
   510   apply(simp add: reflp_def)
 
   507   done
 
   511   done
 
   508 
   512 
   509 lemma all_reg:
 
   513 lemma all_reg:
 
   510   assumes a: "!x :: 'a. (P x --> Q x)"
 
   514   assumes a: "!x :: 'a. (P x --> Q x)"
 
   511   and     b: "All P"
 
   515   and     b: "All P"
 
   549   shows "(Bex (Respects R) f = Bex (Respects R) g)"
 
   553   shows "(Bex (Respects R) f = Bex (Respects R) g)"
 
   550   using a by (simp add: Bex_def IN_RESPECTS)
 
   554   using a by (simp add: Bex_def IN_RESPECTS)
 
   551 
   555 
   552 (* 2 lemmas needed for cleaning of quantifiers *)
 
   556 (* 2 lemmas needed for cleaning of quantifiers *)
 
   553 lemma all_prs:
 
   557 lemma all_prs:
 
   554   assumes a: "QUOTIENT R absf repf"
 
   558   assumes a: "Quotient R absf repf"
 
   555   shows "Ball (Respects R) ((absf ---> id) f) = All f"
 
   559   shows "Ball (Respects R) ((absf ---> id) f) = All f"
 
   556   using a unfolding QUOTIENT_def
 
   560   using a unfolding Quotient_def
 
   557   by (metis IN_RESPECTS fun_map.simps id_apply)
 
   561   by (metis IN_RESPECTS fun_map.simps id_apply)
 
   558 
   562 
   559 lemma ex_prs:
 
   563 lemma ex_prs:
 
   560   assumes a: "QUOTIENT R absf repf"
 
   564   assumes a: "Quotient R absf repf"
 
   561   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
 
   565   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
 
   562   using a unfolding QUOTIENT_def
 
   566   using a unfolding Quotient_def
 
   563   by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
 
   567   by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
 
   564 
   568 
   565 end
 
   569 end
 
   566 
   570
nominal2