diff -r 6088fea1c8b1 -r 8a1c8dc72b5c QuotScript.thy --- a/QuotScript.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,569 +0,0 @@ -theory QuotScript -imports Plain ATP_Linkup -begin - -definition - "equivp E \ \x y. E x y = (E x = E y)" - -definition - "reflp E \ \x. E x x" - -definition - "symp E \ \x y. E x y \ E y x" - -definition - "transp E \ \x y z. E x y \ E y z \ E x z" - -lemma equivp_reflp_symp_transp: - shows "equivp E = (reflp E \ symp E \ transp E)" - unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq - by (blast) - -lemma equivp_reflp: - shows "equivp E \ (\x. E x x)" - by (simp only: equivp_reflp_symp_transp reflp_def) - -lemma equivp_symp: - shows "equivp E \ (\x y. E x y \ E y x)" - by (metis equivp_reflp_symp_transp symp_def) - -lemma equivp_transp: - shows "equivp E \ (\x y z. E x y \ E y z \ E x z)" -by (metis equivp_reflp_symp_transp transp_def) - -definition - "part_equivp E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (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 \ (\a. Abs (Rep a) = a) \ - (\a. E (Rep a) (Rep a)) \ - (\r s. E r s = (E r r \ E s s \ (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 \ E s s \ (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) \ (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 \ 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 - fun_map -where - "fun_map f g h x = g (h (f x))" - -abbreviation - fun_map_syn (infixr "--->" 55) -where - "f ---> g \ 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 = (\x y. E1 x y \ E2 (f x) (g y))" - -abbreviation - fun_rel_syn (infixr "===>" 55) -where - "E1 ===> E2 \ fun_rel E1 E2" - -lemma fun_rel_eq: - "(op =) ===> (op =) \ (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 "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" - apply(simp add: expand_fun_eq) - using q1 q2 - apply(simp add: Quotient_def) - done - moreover - have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" - apply(auto) - using q1 q2 unfolding Quotient_def - apply(metis) - done - moreover - have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ - (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 \ (R x x)" - -lemma in_respects: - shows "(x \ 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) (\x. Rep2 (f (Abs1 x))) = (\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) (\x. (Abs1 ---> Rep2) f x) = (\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]) - -(* 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: - assumes q: "Quotient R1 Abs1 Rep1" - and a: "(R1 ===> R2) f g" "R1 x y" - shows "R2 ((f::'a\'c) x) ((g::'a\'c) 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 \ 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 \ 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: "\x. R x \ P x \ Q x" - shows "All P \ Ball R Q" - by (metis COMBC_def Collect_def Collect_mem_eq a) - -lemma bex_reg_left: - assumes a: "\x. R x \ Q x \ P x" - shows "Bex R Q \ Ex P" - by (metis COMBC_def Collect_def Collect_mem_eq a) - -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) - -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) - -lemma ball_reg_eqv_range: - fixes P::"'a \ bool" - and x::"'a" - assumes a: "equivp R2" - shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" - apply(rule iffI) - apply(rule allI) - apply(drule_tac x="\y. f x" in bspec) - apply(simp add: Respects_def 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: - fixes P::"'a \ bool" - and x::"'a" - assumes a: "equivp R2" - shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" - apply(auto) - apply(rule_tac x="\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: - "(\y. (\x\P. A x y) \ (\x. B x y)) \ ((\x\P. \y. A x y) \ (\x. \y. B x y))" -by auto - -lemma bex_ex_comm: - "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" -by auto - -(* Bounded abstraction *) -definition - Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" -where - "(x \ p) \ (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 \ Respects R1 \ y \ Respects R1") - using a apply (simp add: Babs_def) - apply (simp add: in_respects) - using Quotient_rel[OF q] - by metis - -(* 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: "\x y. R1 x y \ R2 (f x) (g y)" - shows "(R1 ===> R2) f g" -using a by simp - -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 - - - - - - -(******************************************) -(* REST OF THE FILE IS UNUSED (until now) *) -(******************************************) -lemma Quotient_rel_abs: - assumes a: "Quotient E Abs Rep" - shows "E r s \ Abs r = Abs s" -using a unfolding Quotient_def -by blast - -lemma Quotient_rel_abs_eq: - assumes a: "Quotient E Abs Rep" - shows "E r r \ E s s \ E r s = (Abs r = Abs s)" -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 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 \ 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]) - - - -(* 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 -