diff -r 94deffed619d -r fe468f8723fc QuotScript.thy --- a/QuotScript.thy Fri Dec 04 16:53:11 2009 +0100 +++ b/QuotScript.thy Fri Dec 04 17:15:55 2009 +0100 @@ -72,12 +72,12 @@ using a unfolding Quotient_def by blast -lemma IDENTITY_equivp: +lemma identity_equivp: shows "equivp (op =)" unfolding equivp_def by auto -lemma IDENTITY_Quotient: +lemma identity_quotient: shows "Quotient (op =) id id" unfolding Quotient_def id_def by blast @@ -114,11 +114,6 @@ shows "(id ---> id) = id" by (simp add: expand_fun_eq id_def) -(* Not used *) -lemma in_fun: - shows "x \ ((f ---> g) s) = g (f x \ s)" -by (simp add: mem_def) - fun fun_rel where @@ -172,51 +167,10 @@ where "Respects R x \ (R x x)" -lemma IN_RESPECTS: +lemma in_respects: shows "(x \ Respects R) = R x x" unfolding mem_def Respects_def by simp -lemma RESPECTS_THM: - shows "Respects (R1 ===> R2) f = (\x y. R1 x y \ R2 (f x) (f y))" -unfolding Respects_def -by (simp add: expand_fun_eq) - -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_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_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 - -(* -definition - "RES_EXISTS_EQUIV R P \ (\x \ Respects R. P x) \ - (\x\ Respects R. \y\ Respects R. P x \ P y \ R x y)" -*) - -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) \ (Respects (R1 ===> R2) g) - \ ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" -using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq -by blast - (* TODO: it is the same as APPLY_RSP *) (* q1 and q2 not used; see next lemma *) lemma fun_rel_MP: @@ -229,30 +183,6 @@ shows "(R1 ===> R2) f g \ R1 x y \ R2 (f x) (g y)" by simp -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) = (\x y. R1 x y \ 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) -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 \ R2 (f x) (g y)" -using q1 q2 r1 r2 a -by (simp add: fun_rel_EQUALS) lemma equals_rsp: assumes q: "Quotient R Abs Rep" @@ -277,44 +207,7 @@ using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by simp -(* Not used since applic_prs proves a version for an arbitrary number of arguments *) -lemma APP_PRS: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" - shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" -unfolding expand_fun_eq -using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] -by simp - -(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) -lemma LAMBDA_RSP: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and a: "(R1 ===> R2) f1 f2" - shows "(R1 ===> R2) (\x. f1 x) (\y. f2 y)" -by (rule a) - -(* ASK Peter about next four lemmas in quotientScript -lemma ABSTRACT_PRS: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "f = (Rep1 ---> Abs2) ???" -*) - -lemma LAMBDA_REP_ABS_RSP: - assumes r1: "\r r'. R1 r r' \R1 r (Rep1 (Abs1 r'))" - and r2: "\r r'. R2 r r' \R2 r (Rep2 (Abs2 r'))" - shows "(R1 ===> R2) f1 f2 \ (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" -using r1 r2 by auto - -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]) - -(* Not used *) -lemma REP_ABS_RSP_LEFT: +lemma rep_abs_rsp: assumes q: "Quotient R Abs Rep" and a: "R x1 x2" shows "R x1 (Rep (Abs x2))" @@ -362,13 +255,6 @@ (* FUNCTION APPLICATION *) -(* Not used *) -lemma APPLY_PRS: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" -using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto - (* 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 @@ -436,13 +322,13 @@ fixes P :: "'a \ bool" assumes a: "equivp R" shows "Ball (Respects R) P = (All P)" - by (metis equivp_def IN_RESPECTS a) + by (metis equivp_def in_respects a) lemma bex_reg_eqv: fixes P :: "'a \ bool" assumes a: "equivp R" shows "Bex (Respects R) P = (Ex P)" - by (metis equivp_def IN_RESPECTS a) + by (metis equivp_def in_respects a) lemma ball_reg_right: assumes a: "\x. R x \ P x \ Q x" @@ -457,12 +343,12 @@ lemma ball_reg_left: assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" - by (metis equivp_reflp IN_RESPECTS a) + by (metis equivp_reflp in_respects a) lemma bex_reg_right: assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" - by (metis equivp_reflp IN_RESPECTS a) + by (metis equivp_reflp in_respects a) lemma ball_reg_eqv_range: fixes P::"'a \ bool" @@ -472,7 +358,7 @@ apply(rule iffI) apply(rule allI) apply(drule_tac x="\y. f x" in bspec) - apply(simp add: Respects_def IN_RESPECTS) + apply(simp add: Respects_def in_respects) apply(rule impI) using a equivp_reflp_symp_transp[of "R2"] apply(simp add: reflp_def) @@ -488,7 +374,7 @@ apply(auto) apply(rule_tac x="\y. f x" in bexI) apply(simp) - apply(simp add: Respects_def IN_RESPECTS) + apply(simp add: Respects_def in_respects) apply(rule impI) using a equivp_reflp_symp_transp[of "R2"] apply(simp add: reflp_def) @@ -530,25 +416,25 @@ 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) + 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) + using a by (simp add: Bex_def in_respects) (* 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) + 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) + by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) (* UNUSED *) @@ -564,6 +450,107 @@ using a unfolding Quotient_def by blast +lemma in_fun: + shows "x \ ((f ---> g) s) = g (f x \ s)" +by (simp add: mem_def) + +lemma RESPECTS_THM: + shows "Respects (R1 ===> R2) f = (\x y. R1 x y \ 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 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) \ (Respects (R1 ===> R2) g) + \ ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" +using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq +by blast + +(* Not used since in the end we just unfold fun_map *) +lemma APP_PRS: + assumes q1: "Quotient R1 abs1 rep1" + and q2: "Quotient R2 abs2 rep2" + shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" +unfolding expand_fun_eq +using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] +by simp + +(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) +lemma LAMBDA_RSP: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and a: "(R1 ===> R2) f1 f2" + shows "(R1 ===> R2) (\x. f1 x) (\y. f2 y)" +by (rule a) + +(* ASK Peter about next four lemmas in quotientScript +lemma ABSTRACT_PRS: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "f = (Rep1 ---> Abs2) ???" +*) + + +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) = (\x y. R1 x y \ 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) +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 \ R2 (f x) (g y)" +using q1 q2 r1 r2 a +by (simp add: fun_rel_EQUALS) + +lemma LAMBDA_REP_ABS_RSP: + assumes r1: "\r r'. R1 r r' \R1 r (Rep1 (Abs1 r'))" + and r2: "\r r'. R2 r r' \R2 r (Rep2 (Abs2 r'))" + shows "(R1 ===> R2) f1 f2 \ (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" +using r1 r2 by auto + +(* Not used *) +lemma rep_abs_rsp_left: + 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]) end