432 (* TODO: Put the following lemmas in proper places *)

   432 

   433 

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

   434 lemma equiv_res_forall:

   434 lemma ball_reg_eqv:

   436   assumes a: "EQUIV E"

   436   assumes a: "EQUIV R"

   437   shows "Ball (Respects E) P = (All P)"

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

   438   using a by (metis EQUIV_def IN_RESPECTS a)

   438   by (metis EQUIV_def IN_RESPECTS a)

   439 

   439 

   440 lemma equiv_res_exists:

   440 lemma bex_reg_eqv:

   442   assumes a: "EQUIV E"

   442   assumes a: "EQUIV R"

   443   shows "Bex (Respects E) P = (Ex P)"

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

   444   using a by (metis EQUIV_def IN_RESPECTS a)

   444   by (metis EQUIV_def IN_RESPECTS a)

   445 

   445 

   446 lemma FORALL_REGULAR:

   446 lemma ball_reg_right:

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

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

   449   by (metis COMBC_def Collect_def Collect_mem_eq a)

   450 

   451 lemma bex_reg_left:

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

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

   454   by (metis COMBC_def Collect_def Collect_mem_eq a)

   455 

   456 lemma ball_reg_left:

   457   assumes a: "EQUIV R"

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

   459   by (metis EQUIV_REFL IN_RESPECTS a)

   460 

   461 lemma bex_reg_right:

   462   assumes a: "EQUIV R"

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

   464   by (metis EQUIV_REFL IN_RESPECTS a)

   465 

   466 lemma ball_reg_eqv_range:

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

   468   and x::"'a"

   469   assumes a: "EQUIV R2"

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

   471   apply(rule iffI)

   472   apply(rule allI)

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

   474   apply(simp add: Respects_def IN_RESPECTS)

   475   apply(rule impI)

   476   using a EQUIV_REFL_SYM_TRANS[of "R2"]

   477   apply(simp add: REFL_def)

   478   apply(simp)

   479   apply(simp)

   480   done

   481 

   482 lemma bex_reg_eqv_range:

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

   484   and x::"'a"

   485   assumes a: "EQUIV R2"

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

   487   apply(auto)

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

   489   apply(simp)

   490   apply(simp add: Respects_def IN_RESPECTS)

   491   apply(rule impI)

   492   using a EQUIV_REFL_SYM_TRANS[of "R2"]

   493   apply(simp add: REFL_def)

   494   done

   495 

   496 lemma all_reg:

   452 lemma EXISTS_REGULAR:

   502 lemma ex_reg:

   458 lemma RES_FORALL_REGULAR:

   508 lemma ball_reg:

   464 lemma RES_EXISTS_REGULAR:

   514 lemma bex_reg:

   470 lemma LEFT_RES_FORALL_REGULAR:

   520 

   471   assumes a: "\<And>x. (R x \<and> (Q x \<longrightarrow> P x))"

   521 

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

   473   using a

   474   apply (metis COMBC_def Collect_def Collect_mem_eq a)

   475   done

   476 

   477 lemma RIGHT_RES_FORALL_REGULAR:

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

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

   480   using a

   481   apply (metis COMBC_def Collect_def Collect_mem_eq a)

   482   done

   483 

   484 lemma LEFT_RES_EXISTS_REGULAR:

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

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

   487   using a by (metis COMBC_def Collect_def Collect_mem_eq)

   488 

   489 lemma RIGHT_RES_EXISTS_REGULAR:

   490   assumes a: "\<And>x. (R x \<and> (P x \<longrightarrow> Q x))"

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

   492   using a by (metis COMBC_def Collect_def Collect_mem_eq)