# HG changeset patch # User Cezary Kaliszyk # Date 1259944605 -3600 # Node ID d030c8e194658cb0a646afffba688774d6189344 # Parent fe468f8723fc08560e7c5953c21b6c43e25f001e Cleaning/review of QuotScript. diff -r fe468f8723fc -r d030c8e19465 QuotMain.thy --- a/QuotMain.thy Fri Dec 04 17:15:55 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 17:36:45 2009 +0100 @@ -260,7 +260,6 @@ let val qty_name = fst (dest_Type qty) val SOME quotdata = quotdata_lookup lthy qty_name - (* cu: Changed the lookup\not sure whether this works *) (* TODO: Should no longer be needed *) val rty = Logic.unvarifyT (#rtyp quotdata) val rel = #rel quotdata diff -r fe468f8723fc -r d030c8e19465 QuotScript.thy --- a/QuotScript.thy Fri Dec 04 17:15:55 2009 +0100 +++ b/QuotScript.thy Fri Dec 04 17:36:45 2009 +0100 @@ -2,13 +2,13 @@ imports Plain ATP_Linkup begin -definition - "equivp E \ \x y. E x y = (E x = E y)" +definition + "equivp E \ \x y. E x y = (E x = E y)" definition "reflp E \ \x. E x x" -definition +definition "symp E \ \x y. E x y \ E y x" definition @@ -16,8 +16,8 @@ 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) + unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq + by (blast) lemma equivp_refl: shows "equivp R \ (\x. R x x)" @@ -33,66 +33,66 @@ lemma equivp_IMP_part_equivp: assumes a: "equivp E" shows "part_equivp E" -using a unfolding equivp_def part_equivp_def -by auto + 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)) \ + "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 + 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 + 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 + 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 + 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 + using a unfolding Quotient_def + by blast lemma identity_equivp: shows "equivp (op =)" -unfolding equivp_def -by auto + unfolding equivp_def + by auto lemma identity_quotient: shows "Quotient (op =) id id" -unfolding Quotient_def id_def -by blast + 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 + 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 + using a unfolding Quotient_def transp_def + by metis fun prod_rel @@ -104,7 +104,6 @@ where "fun_map f g h x = g (h (f x))" - abbreviation fun_map_syn (infixr "--->" 55) where @@ -112,7 +111,7 @@ lemma fun_map_id: shows "(id ---> id) = id" -by (simp add: expand_fun_eq id_def) + by (simp add: expand_fun_eq id_def) fun fun_rel @@ -169,155 +168,55 @@ lemma in_respects: shows "(x \ 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 \ R1 x y \ R2 (f x) (g y)" -by simp - -lemma fun_rel_IMP: - shows "(R1 ===> R2) f g \ R1 x y \ R2 (f x) (g y)" -by simp - + 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 + 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 + 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 + 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 *) + 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 R2 that - will be provable; which is why we need to use APPLY_RSP *) + 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 (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) - - -(* 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 - - - - + 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" @@ -437,7 +336,13 @@ 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 \ Abs r = Abs s" @@ -522,7 +427,7 @@ 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) +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]) @@ -553,5 +458,83 @@ 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