hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
theory QuotScript+ −
imports Plain ATP_Linkup Predicate+ −
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_reflp:+ −
shows "equivp E \<Longrightarrow> (\<And>x. E x x)"+ −
by (simp only: equivp_reflp_symp_transp reflp_def)+ −
+ −
lemma equivp_symp:+ −
shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"+ −
by (metis equivp_reflp_symp_transp symp_def)+ −
+ −
lemma equivp_transp:+ −
shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"+ −
by (metis equivp_reflp_symp_transp transp_def)+ −
+ −
lemma equivpI:+ −
assumes "reflp R" "symp R" "transp R"+ −
shows "equivp R"+ −
using assms by (simp add: equivp_reflp_symp_transp)+ −
+ −
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+ −
+ −
+ −
abbreviation + −
rel_conj (infixr "OOO" 75)+ −
where+ −
"r1 OOO r2 \<equiv> r1 OO r2 OO r1"+ −
+ −
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)))"+ −
+ −
(* TEST+ −
lemma + −
fixes Abs1::"'b \<Rightarrow> 'c"+ −
and Abs2::"'a \<Rightarrow> 'b"+ −
and Rep1::"'c \<Rightarrow> 'b"+ −
and Rep2::"'b \<Rightarrow> 'a"+ −
assumes "Quotient R1 Abs1 Rep1"+ −
and "Quotient R2 Abs2 Rep2"+ −
shows "Quotient (f R2 R1) (Abs1 \<circ> Abs2) (Rep2 \<circ> Rep1)"+ −
*)+ −
+ −
lemma Quotient_abs_rep:+ −
assumes a: "Quotient E Abs Rep"+ −
shows "Abs (Rep a) \<equiv> 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_rep:+ −
assumes a: "Quotient R Abs Rep"+ −
shows "R (Rep a) (Rep b) \<equiv> (a = b)"+ −
apply (rule eq_reflection)+ −
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 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 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+ −
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_id:+ −
shows "(id ---> id) = id"+ −
by (simp add: expand_fun_eq id_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 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+ −
+ −
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])+ −
+ −
lemma rep_abs_rsp_left:+ −
assumes q: "Quotient R Abs Rep"+ −
and a: "R x1 x2"+ −
shows "R (Rep (Abs x1)) x2"+ −
using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])+ −
+ −
(* 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 R1 that+ −
will be provable; which is why we need to use apply_rsp and+ −
not the primed version *)+ −
lemma apply_rsp:+ −
fixes f g::"'a \<Rightarrow> 'c"+ −
assumes q: "Quotient R1 Abs1 Rep1"+ −
and a: "(R1 ===> R2) f g" "R1 x y"+ −
shows "R2 (f x) (g y)"+ −
using a by simp+ −
+ −
lemma apply_rsp':+ −
assumes a: "(R1 ===> R2) f g" "R1 x y"+ −
shows "R2 (f x) (g y)"+ −
using a by simp+ −
+ −
(* 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: 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:+ −
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+ −
+ −
(* Bounded abstraction *)+ −
definition+ −
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"+ −
where+ −
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"+ −
+ −
(* 3 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)+ −
+ −
lemma babs_rsp:+ −
assumes q: "Quotient R1 Abs1 Rep1"+ −
and a: "(R1 ===> R2) f g"+ −
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"+ −
apply (auto simp add: Babs_def)+ −
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")+ −
using a apply (simp add: Babs_def)+ −
apply (simp add: in_respects)+ −
using Quotient_rel[OF q]+ −
by metis+ −
+ −
lemma babs_prs:+ −
assumes q1: "Quotient R1 Abs1 Rep1"+ −
and q2: "Quotient R2 Abs2 Rep2"+ −
shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f"+ −
apply(rule eq_reflection)+ −
apply(rule ext)+ −
apply simp+ −
apply (subgoal_tac "Rep1 x \<in> Respects R1")+ −
apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])+ −
apply (simp add: in_respects Quotient_rel_rep[OF q1])+ −
done+ −
+ −
lemma babs_simp:+ −
assumes q: "Quotient R1 Abs Rep"+ −
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"+ −
apply(rule iffI)+ −
apply(simp_all only: babs_rsp[OF q])+ −
apply(auto simp add: Babs_def)+ −
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")+ −
apply(metis Babs_def)+ −
apply (simp add: in_respects)+ −
using Quotient_rel[OF q]+ −
by metis+ −
+ −
(* If a user proves that a particular functional relation + −
is an equivalence this may be useful in regularising *)+ −
lemma babs_reg_eqv:+ −
shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"+ −
by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)+ −
+ −
(* 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)+ −
+ −
lemma fun_rel_id:+ −
assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"+ −
shows "(R1 ===> R2) f g"+ −
using a by simp+ −
+ −
lemma fun_rel_id_asm:+ −
assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"+ −
shows "A \<longrightarrow> (R1 ===> R2) f g"+ −
using a by auto+ −
+ −
lemma quot_rel_rsp:+ −
assumes a: "Quotient R Abs Rep"+ −
shows "(R ===> R ===> op =) R R"+ −
apply(rule fun_rel_id)++ −
apply(rule equals_rsp[OF a])+ −
apply(assumption)++ −
done+ −
+ −
lemma o_prs:+ −
assumes q1: "Quotient R1 Abs1 Rep1"+ −
and q2: "Quotient R2 Abs2 Rep2"+ −
and q3: "Quotient R3 Abs3 Rep3"+ −
shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o 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 "absf (if a then repf b else repf c) = (if a then b else c)"+ −
using a unfolding Quotient_def by auto+ −
+ −
lemma if_prs:+ −
assumes q: "Quotient R Abs Rep"+ −
shows "Abs (If a (Rep b) (Rep c)) = If a b c"+ −
using Quotient_abs_rep[OF q] by auto+ −
+ −
(* q not used *)+ −
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 "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"+ −
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto+ −
+ −
lemma let_rsp:+ −
assumes q1: "Quotient R1 Abs1 Rep1"+ −
and a1: "(R1 ===> R2) f g"+ −
and a2: "R1 x y"+ −
shows "R2 ((Let x f)::'c) ((Let y g)::'c)"+ −
using apply_rsp[OF q1 a1] a2 by auto+ −
+ −
+ −
+ −
+ −
(******************************************)+ −
(* REST OF THE FILE IS UNUSED (until now) *)+ −
(******************************************)+ −
+ −
lemma in_fun:+ −
shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"+ −
by (simp add: mem_def)+ −
+ −
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_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_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_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+ −
+ −
lemma abs_o_rep:+ −
assumes a: "Quotient r absf repf"+ −
shows "absf o repf = id"+ −
apply(rule ext)+ −
apply(simp add: Quotient_abs_rep[OF a])+ −
done+ −
+ −
lemma eq_comp_r: "op = OO R OO op = \<equiv> R"+ −
apply (rule eq_reflection)+ −
apply (rule ext)++ −
apply auto+ −
done+ −
+ −
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+ −
+ −
lemma let_babs:+ −
"v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"+ −
by (simp add: Babs_def)+ −
+ −
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 apply_rsp')+ −
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)+ −
+ −
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+ −
+ −
(* ask peter what are literal_case *)+ −
(* literal_case_PRS *)+ −
(* literal_case_RSP *)+ −
(* Cez: !f x. literal_case f x = f x *)+ −
+ −
(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)+ −
lemma id_prs:+ −
assumes q: "Quotient R Abs Rep"+ −
shows "Abs (id (Rep e)) = id e"+ −
using Quotient_abs_rep[OF q] by auto+ −
+ −
lemma id_rsp:+ −
assumes q: "Quotient R Abs Rep"+ −
and a: "R e1 e2"+ −
shows "R (id e1) (id e2)"+ −
using a by auto+ −
+ −
end+ −
+ −