1 theory QuotScript

     2 imports Plain ATP_Linkup

     3 begin

     4 

     5 definition

     6   "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"

     7 

     8 definition

     9   "reflp E \<equiv> \<forall>x. E x x"

    10 

    11 definition

    12   "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"

    13 

    14 definition

    15   "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"

    16 

    17 lemma equivp_reflp_symp_transp:

    18   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"

    19   unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq

    20   by (blast)

    21 

    22 lemma equivp_reflp:

    23   shows "equivp E \<Longrightarrow> (\<And>x. E x x)"

    24   by (simp only: equivp_reflp_symp_transp reflp_def)

    25 

    26 lemma equivp_symp:

    27   shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"

    28   by (metis equivp_reflp_symp_transp symp_def)

    29 

    30 lemma equivp_transp:

    31   shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"

    32 by (metis equivp_reflp_symp_transp transp_def)

    33 

    34 definition

    35   "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)))"

    36 

    37 lemma equivp_IMP_part_equivp:

    38   assumes a: "equivp E"

    39   shows "part_equivp E"

    40   using a unfolding equivp_def part_equivp_def

    41   by auto

    42 

    43 definition

    44   "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and>

    45                         (\<forall>a. E (Rep a) (Rep a)) \<and>

    46                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"

    47 

    48 lemma Quotient_abs_rep:

    49   assumes a: "Quotient E Abs Rep"

    50   shows "Abs (Rep a) \<equiv> a"

    51   using a unfolding Quotient_def

    52   by simp

    53 

    54 lemma Quotient_rep_reflp:

    55   assumes a: "Quotient E Abs Rep"

    56   shows "E (Rep a) (Rep a)"

    57   using a unfolding Quotient_def

    58   by blast

    59 

    60 lemma Quotient_rel:

    61   assumes a: "Quotient E Abs Rep"

    62   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"

    63   using a unfolding Quotient_def

    64   by blast

    65 

    66 lemma Quotient_rel_rep:

    67   assumes a: "Quotient R Abs Rep"

    68   shows "R (Rep a) (Rep b) \<equiv> (a = b)"

    69   apply (rule eq_reflection)

    70   using a unfolding Quotient_def

    71   by metis

    72 

    73 lemma Quotient_rep_abs:

    74   assumes a: "Quotient R Abs Rep"

    75   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"

    76   using a unfolding Quotient_def

    77   by blast

    78 

    79 lemma identity_equivp:

    80   shows "equivp (op =)"

    81   unfolding equivp_def

    82   by auto

    83 

    84 lemma identity_quotient:

    85   shows "Quotient (op =) id id"

    86   unfolding Quotient_def id_def

    87   by blast

    88 

    89 lemma Quotient_symp:

    90   assumes a: "Quotient E Abs Rep"

    91   shows "symp E"

    92   using a unfolding Quotient_def symp_def

    93   by metis

    94 

    95 lemma Quotient_transp:

    96   assumes a: "Quotient E Abs Rep"

    97   shows "transp E"

    98   using a unfolding Quotient_def transp_def

    99   by metis

   100 

   101 fun

   102   fun_map

   103 where

   104   "fun_map f g h x = g (h (f x))"

   105 

   106 abbreviation

   107   fun_map_syn (infixr "--->" 55)

   108 where

   109   "f ---> g \<equiv> fun_map f g"

   110 

   111 lemma fun_map_id:

   112   shows "(id ---> id) = id"

   113   by (simp add: expand_fun_eq id_def)

   114 

   115 fun

   116   fun_rel

   117 where

   118   "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"

   119 

   120 abbreviation

   121   fun_rel_syn (infixr "===>" 55)

   122 where

   123   "E1 ===> E2 \<equiv> fun_rel E1 E2"

   124 

   125 lemma fun_rel_eq:

   126   "(op =) ===> (op =) \<equiv> (op =)"

   127 by (rule eq_reflection) (simp add: expand_fun_eq)

   128 

   129 lemma fun_quotient:

   130   assumes q1: "Quotient R1 abs1 rep1"

   131   and     q2: "Quotient R2 abs2 rep2"

   132   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"

   133 proof -

   134   have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"

   135     apply(simp add: expand_fun_eq)

   136     using q1 q2

   137     apply(simp add: Quotient_def)

   138     done

   139   moreover

   140   have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"

   141     apply(auto)

   142     using q1 q2 unfolding Quotient_def

   143     apply(metis)

   144     done

   145   moreover

   146   have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 

   147         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"

   148     apply(auto simp add: expand_fun_eq)

   149     using q1 q2 unfolding Quotient_def

   150     apply(metis)

   151     using q1 q2 unfolding Quotient_def

   152     apply(metis)

   153     using q1 q2 unfolding Quotient_def

   154     apply(metis)

   155     using q1 q2 unfolding Quotient_def

   156     apply(metis)

   157     done

   158   ultimately

   159   show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"

   160     unfolding Quotient_def by blast

   161 qed

   162 

   163 definition

   164   Respects

   165 where

   166   "Respects R x \<equiv> (R x x)"

   167 

   168 lemma in_respects:

   169   shows "(x \<in> Respects R) = R x x"

   170   unfolding mem_def Respects_def by simp

   171 

   172 lemma equals_rsp:

   173   assumes q: "Quotient R Abs Rep"

   174   and     a: "R xa xb" "R ya yb"

   175   shows "R xa ya = R xb yb"

   176   using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def

   177   using a by blast

   178 

   179 lemma lambda_prs:

   180   assumes q1: "Quotient R1 Abs1 Rep1"

   181   and     q2: "Quotient R2 Abs2 Rep2"

   182   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"

   183   unfolding expand_fun_eq

   184   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]

   185   by simp

   186 

   187 lemma lambda_prs1:

   188   assumes q1: "Quotient R1 Abs1 Rep1"

   189   and     q2: "Quotient R2 Abs2 Rep2"

   190   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"

   191   unfolding expand_fun_eq

   192   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]

   193   by simp

   194 

   195 lemma rep_abs_rsp:

   196   assumes q: "Quotient R Abs Rep"

   197   and     a: "R x1 x2"

   198   shows "R x1 (Rep (Abs x2))"

   199   using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])

   200 

   201 (* In the following theorem R1 can be instantiated with anything,

   202    but we know some of the types of the Rep and Abs functions;

   203    so by solving Quotient assumptions we can get a unique R1 that

   204    will be provable; which is why we need to use apply_rsp and

   205    not the primed version *)

   206 lemma apply_rsp:

   207   assumes q: "Quotient R1 Abs1 Rep1"

   208   and     a: "(R1 ===> R2) f g" "R1 x y"

   209   shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"

   210   using a by simp

   211 

   212 lemma apply_rsp':

   213   assumes a: "(R1 ===> R2) f g" "R1 x y"

   214   shows "R2 (f x) (g y)"

   215   using a by simp

   216 

   217 (* Set of lemmas for regularisation of ball and bex *)

   218 

   219 lemma ball_reg_eqv:

   220   fixes P :: "'a \<Rightarrow> bool"

   221   assumes a: "equivp R"

   222   shows "Ball (Respects R) P = (All P)"

   223   by (metis equivp_def in_respects a)

   224 

   225 lemma bex_reg_eqv:

   226   fixes P :: "'a \<Rightarrow> bool"

   227   assumes a: "equivp R"

   228   shows "Bex (Respects R) P = (Ex P)"

   229   by (metis equivp_def in_respects a)

   230 

   231 lemma ball_reg_right:

   232   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"

   233   shows "All P \<longrightarrow> Ball R Q"

   234   by (metis COMBC_def Collect_def Collect_mem_eq a)

   235 

   236 lemma bex_reg_left:

   237   assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"

   238   shows "Bex R Q \<longrightarrow> Ex P"

   239   by (metis COMBC_def Collect_def Collect_mem_eq a)

   240 

   241 lemma ball_reg_left:

   242   assumes a: "equivp R"

   243   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"

   244   by (metis equivp_reflp in_respects a)

   245 

   246 lemma bex_reg_right:

   247   assumes a: "equivp R"

   248   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"

   249   by (metis equivp_reflp in_respects a)

   250 

   251 lemma ball_reg_eqv_range:

   252   fixes P::"'a \<Rightarrow> bool"

   253   and x::"'a"

   254   assumes a: "equivp R2"

   255   shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"

   256   apply(rule iffI)

   257   apply(rule allI)

   258   apply(drule_tac x="\<lambda>y. f x" in bspec)

   259   apply(simp add: Respects_def in_respects)

   260   apply(rule impI)

   261   using a equivp_reflp_symp_transp[of "R2"]

   262   apply(simp add: reflp_def)

   263   apply(simp)

   264   apply(simp)

   265   done

   266 

   267 lemma bex_reg_eqv_range:

   268   fixes P::"'a \<Rightarrow> bool"

   269   and x::"'a"

   270   assumes a: "equivp R2"

   271   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"

   272   apply(auto)

   273   apply(rule_tac x="\<lambda>y. f x" in bexI)

   274   apply(simp)

   275   apply(simp add: Respects_def in_respects)

   276   apply(rule impI)

   277   using a equivp_reflp_symp_transp[of "R2"]

   278   apply(simp add: reflp_def)

   279   done

   280 

   281 lemma all_reg:

   282   assumes a: "!x :: 'a. (P x --> Q x)"

   283   and     b: "All P"

   284   shows "All Q"

   285   using a b by (metis)

   286 

   287 lemma ex_reg:

   288   assumes a: "!x :: 'a. (P x --> Q x)"

   289   and     b: "Ex P"

   290   shows "Ex Q"

   291   using a b by (metis)

   292 

   293 lemma ball_reg:

   294   assumes a: "!x :: 'a. (R x --> P x --> Q x)"

   295   and     b: "Ball R P"

   296   shows "Ball R Q"

   297   using a b by (metis COMBC_def Collect_def Collect_mem_eq)

   298 

   299 lemma bex_reg:

   300   assumes a: "!x :: 'a. (R x --> P x --> Q x)"

   301   and     b: "Bex R P"

   302   shows "Bex R Q"

   303   using a b by (metis COMBC_def Collect_def Collect_mem_eq)

   304 

   305 lemma ball_all_comm:

   306   "(\<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))"

   307 by auto

   308 

   309 lemma bex_ex_comm:

   310   "((\<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))"

   311 by auto

   312 

   313 (* Bounded abstraction *)

   314 definition

   315   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"

   316 where

   317   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"

   318 

   319 (* 3 lemmas needed for proving repabs_inj *)

   320 lemma ball_rsp:

   321   assumes a: "(R ===> (op =)) f g"

   322   shows "Ball (Respects R) f = Ball (Respects R) g"

   323   using a by (simp add: Ball_def in_respects)

   324 

   325 lemma bex_rsp:

   326   assumes a: "(R ===> (op =)) f g"

   327   shows "(Bex (Respects R) f = Bex (Respects R) g)"

   328   using a by (simp add: Bex_def in_respects)

   329 

   330 lemma babs_rsp:

   331   assumes q: "Quotient R1 Abs1 Rep1"

   332   and     a: "(R1 ===> R2) f g"

   333   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"

   334   apply (auto simp add: Babs_def)

   335   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")

   336   using a apply (simp add: Babs_def)

   337   apply (simp add: in_respects)

   338   using Quotient_rel[OF q]

   339   by metis

   340 

   341 (* 2 lemmas needed for cleaning of quantifiers *)

   342 lemma all_prs:

   343   assumes a: "Quotient R absf repf"

   344   shows "Ball (Respects R) ((absf ---> id) f) = All f"

   345   using a unfolding Quotient_def

   346   by (metis in_respects fun_map.simps id_apply)

   347 

   348 lemma ex_prs:

   349   assumes a: "Quotient R absf repf"

   350   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"

   351   using a unfolding Quotient_def

   352   by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)

   353 

   354 lemma fun_rel_id:

   355   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"

   356   shows "(R1 ===> R2) f g"

   357 using a by simp

   358 

   359 lemma quot_rel_rsp:

   360   assumes a: "Quotient R Abs Rep"

   361   shows "(R ===> R ===> op =) R R"

   362   apply(rule fun_rel_id)+

   363   apply(rule equals_rsp[OF a])

   364   apply(assumption)+

   365   done

   366 

   367 

   368 

   369 

   370 

   371 

   372 (******************************************)

   373 (* REST OF THE FILE IS UNUSED (until now) *)

   374 (******************************************)

   375 lemma Quotient_rel_abs:

   376   assumes a: "Quotient E Abs Rep"

   377   shows "E r s \<Longrightarrow> Abs r = Abs s"

   378 using a unfolding Quotient_def

   379 by blast

   380 

   381 lemma Quotient_rel_abs_eq:

   382   assumes a: "Quotient E Abs Rep"

   383   shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"

   384 using a unfolding Quotient_def

   385 by blast

   386 

   387 lemma in_fun:

   388   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"

   389 by (simp add: mem_def)

   390 

   391 lemma RESPECTS_THM:

   392   shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"

   393 unfolding Respects_def

   394 by (simp add: expand_fun_eq) 

   395 

   396 lemma RESPECTS_REP_ABS:

   397   assumes a: "Quotient R1 Abs1 Rep1"

   398   and     b: "Respects (R1 ===> R2) f"

   399   and     c: "R1 x x"

   400   shows "R2 (f (Rep1 (Abs1 x))) (f x)"

   401 using a b[simplified RESPECTS_THM] c unfolding Quotient_def

   402 by blast

   403 

   404 lemma RESPECTS_MP:

   405   assumes a: "Respects (R1 ===> R2) f"

   406   and     b: "R1 x y"

   407   shows "R2 (f x) (f y)"

   408 using a b unfolding Respects_def

   409 by simp

   410 

   411 lemma RESPECTS_o:

   412   assumes a: "Respects (R2 ===> R3) f"

   413   and     b: "Respects (R1 ===> R2) g"

   414   shows "Respects (R1 ===> R3) (f o g)"

   415 using a b unfolding Respects_def

   416 by simp

   417 

   418 lemma fun_rel_EQ_REL:

   419   assumes q1: "Quotient R1 Abs1 Rep1"

   420   and     q2: "Quotient R2 Abs2 Rep2"

   421   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 

   422                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"

   423 using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq

   424 by blast

   425 

   426 (* Not used since in the end we just unfold fun_map *)

   427 lemma APP_PRS:

   428   assumes q1: "Quotient R1 abs1 rep1"

   429   and     q2: "Quotient R2 abs2 rep2"

   430   shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"

   431 unfolding expand_fun_eq

   432 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]

   433 by simp

   434 

   435 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)

   436 lemma LAMBDA_RSP:

   437   assumes q1: "Quotient R1 Abs1 Rep1"

   438   and     q2: "Quotient R2 Abs2 Rep2"

   439   and     a: "(R1 ===> R2) f1 f2"

   440   shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"

   441 by (rule a)

   442 

   443 (* ASK Peter about next four lemmas in quotientScript

   444 lemma ABSTRACT_PRS:

   445   assumes q1: "Quotient R1 Abs1 Rep1"

   446   and     q2: "Quotient R2 Abs2 Rep2"

   447   shows "f = (Rep1 ---> Abs2) ???"

   448 *)

   449 

   450 

   451 lemma fun_rel_EQUALS:

   452   assumes q1: "Quotient R1 Abs1 Rep1"

   453   and     q2: "Quotient R2 Abs2 Rep2"

   454   and     r1: "Respects (R1 ===> R2) f"

   455   and     r2: "Respects (R1 ===> R2) g" 

   456   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"

   457 apply(rule_tac iffI)

   458 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def

   459 apply(metis apply_rsp')

   460 using r1 unfolding Respects_def expand_fun_eq

   461 apply(simp (no_asm_use))

   462 apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])

   463 done

   464 

   465 (* ask Peter: fun_rel_IMP used twice *) 

   466 lemma fun_rel_IMP2:

   467   assumes q1: "Quotient R1 Abs1 Rep1"

   468   and     q2: "Quotient R2 Abs2 Rep2"

   469   and     r1: "Respects (R1 ===> R2) f"

   470   and     r2: "Respects (R1 ===> R2) g" 

   471   and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"

   472   shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"

   473 using q1 q2 r1 r2 a

   474 by (simp add: fun_rel_EQUALS)

   475 

   476 lemma LAMBDA_REP_ABS_RSP:

   477   assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"

   478   and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"

   479   shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"

   480 using r1 r2 by auto

   481 

   482 (* Not used *)

   483 lemma rep_abs_rsp_left:

   484   assumes q: "Quotient R Abs Rep"

   485   and     a: "R x1 x2"

   486   shows "R x1 (Rep (Abs x2))"

   487 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])

   488 

   489 

   490 

   491 (* bool theory: COND, LET *)

   492 lemma IF_PRS:

   493   assumes q: "Quotient R Abs Rep"

   494   shows "If a b c = Abs (If a (Rep b) (Rep c))"

   495 using Quotient_abs_rep[OF q] by auto

   496 

   497 (* ask peter: no use of q *)

   498 lemma IF_RSP:

   499   assumes q: "Quotient R Abs Rep"

   500   and     a: "a1 = a2" "R b1 b2" "R c1 c2"

   501   shows "R (If a1 b1 c1) (If a2 b2 c2)"

   502 using a by auto

   503 

   504 lemma LET_PRS:

   505   assumes q1: "Quotient R1 Abs1 Rep1"

   506   and     q2: "Quotient R2 Abs2 Rep2"

   507   shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"

   508 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto

   509 

   510 lemma LET_RSP:

   511   assumes q1: "Quotient R1 Abs1 Rep1"

   512   and     a1: "(R1 ===> R2) f g"

   513   and     a2: "R1 x y"

   514   shows "R2 ((Let x f)::'c) ((Let y g)::'c)"

   515 using apply_rsp[OF q1 a1] a2

   516 by auto

   517 

   518 

   519 

   520 (* ask peter what are literal_case *)

   521 (* literal_case_PRS *)

   522 (* literal_case_RSP *)

   523 

   524 

   525 

   526 

   527 

   528 (* combinators: I, K, o, C, W *)

   529 

   530 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *)

   531 

   532 lemma I_PRS:

   533   assumes q: "Quotient R Abs Rep"

   534   shows "id e = Abs (id (Rep e))"

   535 using Quotient_abs_rep[OF q] by auto

   536 

   537 lemma I_RSP:

   538   assumes q: "Quotient R Abs Rep"

   539   and     a: "R e1 e2"

   540   shows "R (id e1) (id e2)"

   541 using a by auto

   542 

   543 lemma o_PRS:

   544   assumes q1: "Quotient R1 Abs1 Rep1"

   545   and     q2: "Quotient R2 Abs2 Rep2"

   546   and     q3: "Quotient R3 Abs3 Rep3"

   547   shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"

   548 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]

   549 unfolding o_def expand_fun_eq

   550 by simp

   551 

   552 lemma o_RSP:

   553   assumes q1: "Quotient R1 Abs1 Rep1"

   554   and     q2: "Quotient R2 Abs2 Rep2"

   555   and     q3: "Quotient R3 Abs3 Rep3"

   556   and     a1: "(R2 ===> R3) f1 f2"

   557   and     a2: "(R1 ===> R2) g1 g2"

   558   shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"

   559 using a1 a2 unfolding o_def expand_fun_eq

   560 by (auto)

   561 

   562 lemma COND_PRS:

   563   assumes a: "Quotient R absf repf"

   564   shows "(if a then b else c) = absf (if a then repf b else repf c)"

   565   using a unfolding Quotient_def by auto

   566 

   567 

   568 end

   569