nominal2: comparison QuotScript.thy

equal deleted inserted replaced

-:fe468f8723fc
+:d030c8e19465
 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)
 "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_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 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_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))"
 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
-(* 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 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])
-(* ----------------------------------------------------- *)
-(* 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 *)
 (* 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
+so by solving Quotient assumptions we can get a unique R1 that
-will be provable; which is why we need to use APPLY_RSP *)
+will be provable; which is why we need to use apply_rsp and
+not the primed version *)
 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)
+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 (rule fun_rel_IMP)
+using a by simp
-(* 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)
 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)
-(* UNUSED *)
+(******************************************)
+(* REST OF THE FILE IS UNUSED (until now) *)
+(******************************************)
 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
 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)
+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
 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])
+(* 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     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
+(* ask peter what are literal_case *)
+(* literal_case_PRS *)
+(* literal_case_RSP *)
+(* 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
 end

changeset 543	d030c8e19465
parent 542	fe468f8723fc
child 546	8a1f4227dff9