# HG changeset patch # User Cezary Kaliszyk # Date 1265879162 -3600 # Node ID 17ca92ab4660e4ba1e5191ae890b7cbe11c94c40 # Parent 243a5ceaa08875a79698a9fa6bd48fecf636c4fe Main renaming + fixes for new Isabelle in IntEx2. diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory AbsRepTest -imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List +imports "../Quotient" "../Quotient_List" "../Quotient_Option" "../Quotient_Sum" "../Quotient_Product" List begin diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/FSet.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory FSet -imports "../QuotMain" "../QuotList" "../QuotProd" List +imports "../Quotient" "../Quotient_List" "../Quotient_Product" List begin inductive diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/FSet2.thy --- a/Quot/Examples/FSet2.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/FSet2.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory FSet2 -imports "../QuotMain" "../QuotList" List +imports "../Quotient" "../Quotient_List" List begin inductive diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/FSet3.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory FSet3 -imports "../QuotMain" "../QuotList" List +imports "../Quotient" "../Quotient_List" List begin ML {* diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/IntEx.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory IntEx -imports "../QuotProd" "../QuotList" +imports "../Quotient_Product" "../Quotient_List" begin fun diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/IntEx2.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory IntEx2 -imports "../QuotMain" "../QuotProd" Nat +imports "../Quotient" "../Quotient_Product" Nat (*uses ("Tools/numeral.ML") ("Tools/numeral_syntax.ML") @@ -271,7 +271,7 @@ by (cases i, cases j, cases k) (simp) -instance int :: pordered_cancel_ab_semigroup_add +instance int :: ordered_cancel_ab_semigroup_add proof fix i j k :: int show "i \ j \ k + i \ k + j" @@ -318,7 +318,7 @@ done text{*The integers form an ordered integral domain*} -instance int :: ordered_idom +instance int :: linordered_idom proof fix i j k :: int show "i < j \ 0 < k \ k * i < k * j" @@ -329,11 +329,11 @@ by (simp only: zsgn_def) qed -instance int :: lordered_ring +instance int :: linordered_ring proof - fix k :: int +(* fix k :: int show "abs k = sup k (- k)" - by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric]) + by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])*) qed lemmas int_distrib = diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/LFex.thy --- a/Quot/Examples/LFex.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/LFex.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory LFex -imports Nominal "../QuotList" +imports Nominal "../Quotient_List" begin atom_decl name ident diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/LamEx.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory LamEx -imports Nominal "../QuotMain" "../QuotList" +imports Nominal "../Quotient" "../Quotient_List" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/LarryDatatype.thy --- a/Quot/Examples/LarryDatatype.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/LarryDatatype.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory LarryDatatype -imports Main "../QuotMain" +imports Main "../Quotient" begin subsection{*Defining the Free Algebra*} diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/LarryInt.thy --- a/Quot/Examples/LarryInt.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/LarryInt.thy Thu Feb 11 10:06:02 2010 +0100 @@ -2,7 +2,7 @@ header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} theory LarryInt -imports Nat "../QuotMain" "../QuotProd" +imports Nat "../Quotient" "../Quotient_Product" begin fun diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/SigmaEx.thy --- a/Quot/Examples/SigmaEx.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/SigmaEx.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory SigmaEx -imports Nominal "../QuotMain" "../QuotList" "../QuotProd" +imports Nominal "../Quotient" "../Quotient_List" "../Quotient_Product" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/Terms.thy --- a/Quot/Examples/Terms.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Examples/Terms.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory Terms -imports Nominal "../QuotMain" "../QuotList" +imports Nominal "../Quotient" "../Quotient_List" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Nominal/Abs.thy --- a/Quot/Nominal/Abs.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Nominal/Abs.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory Abs -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" begin (* the next three lemmas that should be in Nominal \\must be cleaned *) diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Nominal/LFex.thy --- a/Quot/Nominal/LFex.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Nominal/LFex.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory LFex -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Nominal/LamEx.thy --- a/Quot/Nominal/LamEx.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Nominal/LamEx.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory LamEx -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Nominal/LamEx2.thy --- a/Quot/Nominal/LamEx2.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Nominal/LamEx2.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory LamEx -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs" "../Quotient_Product" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/Nominal/Terms.thy Thu Feb 11 10:06:02 2010 +0100 @@ -1,5 +1,5 @@ theory Terms -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs" begin atom_decl name diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/QuotList.thy --- a/Quot/QuotList.thy Thu Feb 11 09:23:59 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,232 +0,0 @@ -(* Title: QuotList.thy - Author: Cezary Kaliszyk and Christian Urban -*) -theory QuotList -imports QuotMain List -begin - -section {* Quotient infrastructure for the list type. *} - -fun - list_rel -where - "list_rel R [] [] = True" -| "list_rel R (x#xs) [] = False" -| "list_rel R [] (x#xs) = False" -| "list_rel R (x#xs) (y#ys) = (R x y \ list_rel R xs ys)" - -declare [[map list = (map, list_rel)]] - -lemma split_list_all: - shows "(\x. P x) \ P [] \ (\x xs. P (x#xs))" - apply(auto) - apply(case_tac x) - apply(simp_all) - done - -lemma map_id[id_simps]: - shows "map id = id" - apply(simp add: expand_fun_eq) - apply(rule allI) - apply(induct_tac x) - apply(simp_all) - done - - -lemma list_rel_reflp: - shows "equivp R \ list_rel R xs xs" - apply(induct xs) - apply(simp_all add: equivp_reflp) - done - -lemma list_rel_symp: - assumes a: "equivp R" - shows "list_rel R xs ys \ list_rel R ys xs" - apply(induct xs ys rule: list_induct2') - apply(simp_all) - apply(rule equivp_symp[OF a]) - apply(simp) - done - -lemma list_rel_transp: - assumes a: "equivp R" - shows "list_rel R xs1 xs2 \ list_rel R xs2 xs3 \ list_rel R xs1 xs3" - apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2') - apply(simp_all) - apply(case_tac xs3) - apply(simp_all) - apply(rule equivp_transp[OF a]) - apply(auto) - done - -lemma list_equivp[quot_equiv]: - assumes a: "equivp R" - shows "equivp (list_rel R)" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(subst split_list_all) - apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a]) - apply(blast intro: list_rel_symp[OF a]) - apply(blast intro: list_rel_transp[OF a]) - done - -lemma list_rel_rel: - assumes q: "Quotient R Abs Rep" - shows "list_rel R r s = (list_rel R r r \ list_rel R s s \ (map Abs r = map Abs s))" - apply(induct r s rule: list_induct2') - apply(simp_all) - using Quotient_rel[OF q] - apply(metis) - done - -lemma list_quotient[quot_thm]: - assumes q: "Quotient R Abs Rep" - shows "Quotient (list_rel R) (map Abs) (map Rep)" - unfolding Quotient_def - apply(subst split_list_all) - apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id) - apply(rule conjI) - apply(rule allI) - apply(induct_tac a) - apply(simp) - apply(simp) - apply(simp add: Quotient_rep_reflp[OF q]) - apply(rule allI)+ - apply(rule list_rel_rel[OF q]) - done - - -lemma cons_prs_aux: - assumes q: "Quotient R Abs Rep" - shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" - by (induct t) (simp_all add: Quotient_abs_rep[OF q]) - -lemma cons_prs[quot_preserve]: - assumes q: "Quotient R Abs Rep" - shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" - by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) - (simp) - -lemma cons_rsp[quot_respect]: - assumes q: "Quotient R Abs Rep" - shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)" - by (auto) - -lemma nil_prs[quot_preserve]: - assumes q: "Quotient R Abs Rep" - shows "map Abs [] = []" - by simp - -lemma nil_rsp[quot_respect]: - assumes q: "Quotient R Abs Rep" - shows "list_rel R [] []" - by simp - -lemma map_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" - by (induct l) - (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) - - -lemma map_prs[quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" - by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) - (simp) - - -lemma map_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" - apply(simp) - apply(rule allI)+ - apply(rule impI) - apply(rule allI)+ - apply (induct_tac xa ya rule: list_induct2') - apply simp_all - done - -lemma foldr_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" - by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) - -lemma foldr_prs[quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" - by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) - (simp) - -lemma foldl_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" - by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) - - -lemma foldl_prs[quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" - by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) - (simp) - -lemma list_rel_empty: - shows "list_rel R [] b \ length b = 0" - by (induct b) (simp_all) - -lemma list_rel_len: - shows "list_rel R a b \ length a = length b" - apply (induct a arbitrary: b) - apply (simp add: list_rel_empty) - apply (case_tac b) - apply simp_all - done - -(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) -lemma foldl_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" - apply(auto) - apply (subgoal_tac "R1 xa ya \ list_rel R2 xb yb \ R1 (foldl x xa xb) (foldl y ya yb)") - apply simp - apply (rule_tac x="xa" in spec) - apply (rule_tac x="ya" in spec) - apply (rule_tac xs="xb" and ys="yb" in list_induct2) - apply (rule list_rel_len) - apply (simp_all) - done - -lemma foldr_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" - apply auto - apply(subgoal_tac "R2 xb yb \ list_rel R1 xa ya \ R2 (foldr x xa xb) (foldr y ya yb)") - apply simp - apply (rule_tac xs="xa" and ys="ya" in list_induct2) - apply (rule list_rel_len) - apply (simp_all) - done - -lemma list_rel_eq[id_simps]: - shows "(list_rel (op =)) = (op =)" - unfolding expand_fun_eq - apply(rule allI)+ - apply(induct_tac x xa rule: list_induct2') - apply(simp_all) - done - -lemma list_rel_refl: - assumes a: "\x y. R x y = (R x = R y)" - shows "list_rel R x x" - by (induct x) (auto simp add: a) - -end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Thu Feb 11 09:23:59 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,802 +0,0 @@ -(* Title: QuotMain.thy - Author: Cezary Kaliszyk and Christian Urban -*) - -theory QuotMain -imports Plain ATP_Linkup -uses - ("quotient_info.ML") - ("quotient_typ.ML") - ("quotient_def.ML") - ("quotient_term.ML") - ("quotient_tacs.ML") -begin - -text {* - Basic definition for equivalence relations - that are represented by predicates. -*} - -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 \ E x x" - by (simp only: equivp_reflp_symp_transp reflp_def) - -lemma equivp_symp: - shows "equivp E \ E x y \ E y x" - by (metis equivp_reflp_symp_transp symp_def) - -lemma equivp_transp: - shows "equivp E \ E x y \ E y z \ 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) - -lemma eq_imp_rel: - shows "equivp R \ a = b \ R a b" - by (simp add: equivp_reflp) - -lemma identity_equivp: - shows "equivp (op =)" - unfolding equivp_def - by auto - - -text {* Partial equivalences: not yet used anywhere *} -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_implies_part_equivp: - assumes a: "equivp E" - shows "part_equivp E" - using a - unfolding equivp_def part_equivp_def - by auto - -text {* Composition of Relations *} - -abbreviation - rel_conj (infixr "OOO" 75) -where - "r1 OOO r2 \ r1 OO r2 OO r1" - -lemma eq_comp_r: - shows "((op =) OOO R) = R" - by (auto simp add: expand_fun_eq) - -section {* Respects predicate *} - -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 - -section {* Function map and function relation *} - -definition - fun_map (infixr "--->" 55) -where -[simp]: "fun_map f g h x = g (h (f x))" - -definition - fun_rel (infixr "===>" 55) -where -[simp]: "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" - - -lemma fun_map_id: - shows "(id ---> id) = id" - by (simp add: expand_fun_eq id_def) - -lemma fun_rel_eq: - shows "((op =) ===> (op =)) = (op =)" - by (simp add: expand_fun_eq) - -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 fun_rel_id_asm: - assumes a: "\x y. R1 x y \ (A \ R2 (f x) (g y))" - shows "A \ (R1 ===> R2) f g" - using a by auto - - -section {* Quotient Predicate *} - -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)" - 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 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_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 - -lemma identity_quotient: - shows "Quotient (op =) id id" - unfolding Quotient_def id_def - by blast - -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" - using q1 q2 - unfolding Quotient_def - unfolding expand_fun_eq - by simp - moreover - have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" - using q1 q2 - unfolding Quotient_def - by (simp (no_asm)) (metis) - moreover - have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ - (rep1 ---> abs2) r = (rep1 ---> abs2) s)" - unfolding expand_fun_eq - apply(auto) - 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 - -lemma abs_o_rep: - assumes a: "Quotient R Abs Rep" - shows "Abs o Rep = id" - unfolding expand_fun_eq - by (simp add: Quotient_abs_rep[OF a]) - -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 a Quotient_symp[OF q] Quotient_transp[OF q] - unfolding symp_def transp_def - 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 a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] - by metis - -lemma rep_abs_rsp_left: - assumes q: "Quotient R Abs Rep" - and a: "R x1 x2" - shows "R (Rep (Abs x1)) x2" - using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] - by metis - -text{* - 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 \ '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 - -section {* 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)" - using a - unfolding equivp_def - by (auto simp add: in_respects) - -lemma bex_reg_eqv: - fixes P :: "'a \ bool" - assumes a: "equivp R" - shows "Bex (Respects R) P = (Ex P)" - using a - unfolding equivp_def - by (auto simp add: in_respects) - -lemma ball_reg_right: - assumes a: "\x. R x \ P x \ Q x" - shows "All P \ Ball R Q" - using a by (metis COMBC_def Collect_def Collect_mem_eq) - -lemma bex_reg_left: - assumes a: "\x. R x \ Q x \ P x" - shows "Bex R Q \ Ex P" - using a by (metis COMBC_def Collect_def Collect_mem_eq) - -lemma ball_reg_left: - assumes a: "equivp R" - shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" - using a by (metis equivp_reflp in_respects) - -lemma bex_reg_right: - assumes a: "equivp R" - shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" - using a by (metis equivp_reflp in_respects) - -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: 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)) (\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: - assumes "\y. (\x\P. A x y) \ (\x. B x y)" - shows "(\x\P. \y. A x y) \ (\x. \y. B x y)" - using assms by auto - -lemma bex_ex_comm: - assumes "(\y. \x. A x y) \ (\y. \x\P. B x y)" - shows "(\x. \y. A x y) \ (\x\P. \y. B x y)" - using assms by auto - -section {* Bounded abstraction *} - -definition - Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" -where - "x \ p \ Babs p m x = m x" - -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 in_respects) - 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 - -lemma babs_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" - apply (rule ext) - apply (simp) - apply (subgoal_tac "Rep1 x \ 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 \ Respects R1 \ y \ 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 \ Babs (Respects R) P = P" - by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) - - -(* 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 bex1_rsp: - assumes a: "(R ===> (op =)) f g" - shows "Ex1 (\x. x \ Respects R \ f x) = Ex1 (\x. x \ Respects R \ g x)" - using a - by (simp add: Ex1_def in_respects) auto - -(* 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 Ball_def in_respects fun_map_def id_apply - by metis - -lemma ex_prs: - assumes a: "Quotient R absf repf" - shows "Bex (Respects R) ((absf ---> id) f) = Ex f" - using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply - by metis - -section {* Bex1_rel quantifier *} - -definition - Bex1_rel :: "('a \ 'a \ bool) \ ('a \ bool) \ bool" -where - "Bex1_rel R P \ (\x \ Respects R. P x) \ (\x \ Respects R. \y \ Respects R. ((P x \ P y) \ (R x y)))" - -lemma bex1_rel_aux: - "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R x\ \ Bex1_rel R y" - unfolding Bex1_rel_def - apply (erule conjE)+ - apply (erule bexE) - apply rule - apply (rule_tac x="xa" in bexI) - apply metis - apply metis - apply rule+ - apply (erule_tac x="xaa" in ballE) - prefer 2 - apply (metis) - apply (erule_tac x="ya" in ballE) - prefer 2 - apply (metis) - apply (metis in_respects) - done - -lemma bex1_rel_aux2: - "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R y\ \ Bex1_rel R x" - unfolding Bex1_rel_def - apply (erule conjE)+ - apply (erule bexE) - apply rule - apply (rule_tac x="xa" in bexI) - apply metis - apply metis - apply rule+ - apply (erule_tac x="xaa" in ballE) - prefer 2 - apply (metis) - apply (erule_tac x="ya" in ballE) - prefer 2 - apply (metis) - apply (metis in_respects) - done - -lemma bex1_rel_rsp: - assumes a: "Quotient R absf repf" - shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" - apply simp - apply clarify - apply rule - apply (simp_all add: bex1_rel_aux bex1_rel_aux2) - apply (erule bex1_rel_aux2) - apply assumption - done - - -lemma ex1_prs: - assumes a: "Quotient R absf repf" - shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" -apply simp -apply (subst Bex1_rel_def) -apply (subst Bex_def) -apply (subst Ex1_def) -apply simp -apply rule - apply (erule conjE)+ - apply (erule_tac exE) - apply (erule conjE) - apply (subgoal_tac "\y. R y y \ f (absf y) \ R x y") - apply (rule_tac x="absf x" in exI) - apply (simp) - apply rule+ - using a unfolding Quotient_def - apply metis - apply rule+ - apply (erule_tac x="x" in ballE) - apply (erule_tac x="y" in ballE) - apply simp - apply (simp add: in_respects) - apply (simp add: in_respects) -apply (erule_tac exE) - apply rule - apply (rule_tac x="repf x" in exI) - apply (simp only: in_respects) - apply rule - apply (metis Quotient_rel_rep[OF a]) -using a unfolding Quotient_def apply (simp) -apply rule+ -using a unfolding Quotient_def in_respects -apply metis -done - -lemma bex1_bexeq_reg: "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" - apply (simp add: Ex1_def Bex1_rel_def in_respects) - apply clarify - apply auto - apply (rule bexI) - apply assumption - apply (simp add: in_respects) - apply (simp add: in_respects) - apply auto - done - -section {* Various respects and preserve lemmas *} - -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 - -locale quot_type = - fixes R :: "'a \ 'a \ bool" - and Abs :: "('a \ bool) \ 'b" - and Rep :: "'b \ ('a \ bool)" - assumes equivp: "equivp R" - and rep_prop: "\y. \x. Rep y = R x" - and rep_inverse: "\x. Abs (Rep x) = x" - and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" - and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" -begin - -definition - abs::"'a \ 'b" -where - "abs x \ Abs (R x)" - -definition - rep::"'b \ 'a" -where - "rep a = Eps (Rep a)" - -lemma homeier_lem9: - shows "R (Eps (R x)) = R x" -proof - - have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) - then have "R x (Eps (R x))" by (rule someI) - then show "R (Eps (R x)) = R x" - using equivp unfolding equivp_def by simp -qed - -theorem homeier_thm10: - shows "abs (rep a) = a" - unfolding abs_def rep_def -proof - - from rep_prop - obtain x where eq: "Rep a = R x" by auto - have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp - also have "\ = Abs (R x)" using homeier_lem9 by simp - also have "\ = Abs (Rep a)" using eq by simp - also have "\ = a" using rep_inverse by simp - finally - show "Abs (R (Eps (Rep a))) = a" by simp -qed - -lemma homeier_lem7: - shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") -proof - - have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) - also have "\ = ?LHS" by (simp add: abs_inverse) - finally show "?LHS = ?RHS" by simp -qed - -theorem homeier_thm11: - shows "R r r' = (abs r = abs r')" - unfolding abs_def - by (simp only: equivp[simplified equivp_def] homeier_lem7) - -lemma rep_refl: - shows "R (rep a) (rep a)" - unfolding rep_def - by (simp add: equivp[simplified equivp_def]) - - -lemma rep_abs_rsp: - shows "R f (rep (abs g)) = R f g" - and "R (rep (abs g)) f = R g f" - by (simp_all add: homeier_thm10 homeier_thm11) - -lemma Quotient: - shows "Quotient R abs rep" - unfolding Quotient_def - apply(simp add: homeier_thm10) - apply(simp add: rep_refl) - apply(subst homeier_thm11[symmetric]) - apply(simp add: equivp[simplified equivp_def]) - done - -end - -section {* ML setup *} - -text {* Auxiliary data for the quotient package *} - -use "quotient_info.ML" - -declare [[map "fun" = (fun_map, fun_rel)]] - -lemmas [quot_thm] = fun_quotient -lemmas [quot_respect] = quot_rel_rsp -lemmas [quot_equiv] = identity_equivp - - -text {* Lemmas about simplifying id's. *} -lemmas [id_simps] = - id_def[symmetric] - fun_map_id - id_apply - id_o - o_id - eq_comp_r - -text {* Translation functions for the lifting process. *} -use "quotient_term.ML" - - -text {* Definitions of the quotient types. *} -use "quotient_typ.ML" - - -text {* Definitions for quotient constants. *} -use "quotient_def.ML" - - -text {* - An auxiliary constant for recording some information - about the lifted theorem in a tactic. -*} -definition - "Quot_True x \ True" - -lemma - shows QT_all: "Quot_True (All P) \ Quot_True P" - and QT_ex: "Quot_True (Ex P) \ Quot_True P" - and QT_ex1: "Quot_True (Ex1 P) \ Quot_True P" - and QT_lam: "Quot_True (\x. P x) \ (\x. Quot_True (P x))" - and QT_ext: "(\x. Quot_True (a x) \ f x = g x) \ (Quot_True a \ f = g)" - by (simp_all add: Quot_True_def ext) - -lemma QT_imp: "Quot_True a \ Quot_True b" - by (simp add: Quot_True_def) - - -text {* Tactics for proving the lifted theorems *} -use "quotient_tacs.ML" - -section {* Methods / Interface *} - -(* TODO inline *) -ML {* -fun mk_method1 tac thms ctxt = - SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) - -fun mk_method2 tac ctxt = - SIMPLE_METHOD (HEADGOAL (tac ctxt)) -*} - -method_setup lifting = - {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} - {* lifts theorems to quotient types *} - -method_setup lifting_setup = - {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} - {* sets up the three goals for the quotient lifting procedure *} - -method_setup regularize = - {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} - {* proves the regularization goals from the quotient lifting procedure *} - -method_setup injection = - {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *} - {* proves the rep/abs injection goals from the quotient lifting procedure *} - -method_setup cleaning = - {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} - {* proves the cleaning goals from the quotient lifting procedure *} - -attribute_setup quot_lifted = - {* Scan.succeed Quotient_Tacs.lifted_attrib *} - {* lifts theorems to quotient types *} - -end - diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/QuotOption.thy --- a/Quot/QuotOption.thy Thu Feb 11 09:23:59 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -(* Title: QuotOption.thy - Author: Cezary Kaliszyk and Christian Urban -*) -theory QuotOption -imports QuotMain -begin - -section {* Quotient infrastructure for the option type. *} - -fun - option_rel -where - "option_rel R None None = True" -| "option_rel R (Some x) None = False" -| "option_rel R None (Some x) = False" -| "option_rel R (Some x) (Some y) = R x y" - -declare [[map option = (Option.map, option_rel)]] - -text {* should probably be in Option.thy *} -lemma split_option_all: - shows "(\x. P x) \ P None \ (\a. P (Some a))" - apply(auto) - apply(case_tac x) - apply(simp_all) - done - -lemma option_quotient[quot_thm]: - assumes q: "Quotient R Abs Rep" - shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" - unfolding Quotient_def - apply(simp add: split_option_all) - apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) - using q - unfolding Quotient_def - apply(blast) - done - -lemma option_equivp[quot_equiv]: - assumes a: "equivp R" - shows "equivp (option_rel R)" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(simp_all add: split_option_all) - apply(blast intro: equivp_reflp[OF a]) - apply(blast intro: equivp_symp[OF a]) - apply(blast intro: equivp_transp[OF a]) - done - -lemma option_None_rsp[quot_respect]: - assumes q: "Quotient R Abs Rep" - shows "option_rel R None None" - by simp - -lemma option_Some_rsp[quot_respect]: - assumes q: "Quotient R Abs Rep" - shows "(R ===> option_rel R) Some Some" - by simp - -lemma option_None_prs[quot_preserve]: - assumes q: "Quotient R Abs Rep" - shows "Option.map Abs None = None" - by simp - -lemma option_Some_prs[quot_preserve]: - assumes q: "Quotient R Abs Rep" - shows "(Rep ---> Option.map Abs) Some = Some" - apply(simp add: expand_fun_eq) - apply(simp add: Quotient_abs_rep[OF q]) - done - -lemma option_map_id[id_simps]: - shows "Option.map id = id" - by (simp add: expand_fun_eq split_option_all) - -lemma option_rel_eq[id_simps]: - shows "option_rel (op =) = (op =)" - by (simp add: expand_fun_eq split_option_all) - -end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/QuotProd.thy --- a/Quot/QuotProd.thy Thu Feb 11 09:23:59 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -(* Title: QuotProd.thy - Author: Cezary Kaliszyk and Christian Urban -*) -theory QuotProd -imports QuotMain -begin - -section {* Quotient infrastructure for the product type. *} - -fun - prod_rel -where - "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" - -declare [[map * = (prod_fun, prod_rel)]] - - -lemma prod_equivp[quot_equiv]: - assumes a: "equivp R1" - assumes b: "equivp R2" - shows "equivp (prod_rel R1 R2)" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(simp_all add: split_paired_all) - apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) - apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) - apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) - done - -lemma prod_quotient[quot_thm]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" - unfolding Quotient_def - apply(simp add: split_paired_all) - apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) - apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) - using q1 q2 - unfolding Quotient_def - apply(blast) - done - -lemma Pair_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" - by simp - -lemma Pair_prs[quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" - apply(simp add: expand_fun_eq) - apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) - done - -lemma fst_rsp[quot_respect]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" - shows "(prod_rel R1 R2 ===> R1) fst fst" - by simp - -lemma fst_prs[quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" - apply(simp add: expand_fun_eq) - apply(simp add: Quotient_abs_rep[OF q1]) - done - -lemma snd_rsp[quot_respect]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" - shows "(prod_rel R1 R2 ===> R2) snd snd" - by simp - -lemma snd_prs[quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" - apply(simp add: expand_fun_eq) - apply(simp add: Quotient_abs_rep[OF q2]) - done - -lemma split_rsp[quot_respect]: - shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" - by auto - -lemma split_prs[quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" - by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) - -lemma prod_fun_id[id_simps]: - shows "prod_fun id id = id" - by (simp add: prod_fun_def) - -lemma prod_rel_eq[id_simps]: - shows "prod_rel (op =) (op =) = (op =)" - by (simp add: expand_fun_eq) - - -end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/QuotSum.thy --- a/Quot/QuotSum.thy Thu Feb 11 09:23:59 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Title: QuotSum.thy - Author: Cezary Kaliszyk and Christian Urban -*) -theory QuotSum -imports QuotMain -begin - -section {* Quotient infrastructure for the sum type. *} - -fun - sum_rel -where - "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" - -fun - sum_map -where - "sum_map f1 f2 (Inl a) = Inl (f1 a)" -| "sum_map f1 f2 (Inr a) = Inr (f2 a)" - -declare [[map "+" = (sum_map, sum_rel)]] - - -text {* should probably be in Sum_Type.thy *} -lemma split_sum_all: - shows "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" - apply(auto) - apply(case_tac x) - apply(simp_all) - done - -lemma sum_equivp[quot_equiv]: - assumes a: "equivp R1" - assumes b: "equivp R2" - shows "equivp (sum_rel R1 R2)" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(simp_all add: split_sum_all) - apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) - apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) - apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) - done - -lemma sum_quotient[quot_thm]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" - unfolding Quotient_def - apply(simp add: split_sum_all) - apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) - apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) - using q1 q2 - unfolding Quotient_def - apply(blast)+ - done - -lemma sum_Inl_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(R1 ===> sum_rel R1 R2) Inl Inl" - by simp - -lemma sum_Inr_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(R2 ===> sum_rel R1 R2) Inr Inr" - by simp - -lemma sum_Inl_prs[quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" - apply(simp add: expand_fun_eq) - apply(simp add: Quotient_abs_rep[OF q1]) - done - -lemma sum_Inr_prs[quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" - apply(simp add: expand_fun_eq) - apply(simp add: Quotient_abs_rep[OF q2]) - done - -lemma sum_map_id[id_simps]: - shows "sum_map id id = id" - by (simp add: expand_fun_eq split_sum_all) - -lemma sum_rel_eq[id_simps]: - shows "sum_rel (op =) (op =) = (op =)" - by (simp add: expand_fun_eq split_sum_all) - -end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Quotient.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Quotient.thy Thu Feb 11 10:06:02 2010 +0100 @@ -0,0 +1,802 @@ +(* Title: QuotMain.thy + Author: Cezary Kaliszyk and Christian Urban +*) + +theory Quotient +imports Plain ATP_Linkup +uses + ("quotient_info.ML") + ("quotient_typ.ML") + ("quotient_def.ML") + ("quotient_term.ML") + ("quotient_tacs.ML") +begin + +text {* + Basic definition for equivalence relations + that are represented by predicates. +*} + +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 \ E x x" + by (simp only: equivp_reflp_symp_transp reflp_def) + +lemma equivp_symp: + shows "equivp E \ E x y \ E y x" + by (metis equivp_reflp_symp_transp symp_def) + +lemma equivp_transp: + shows "equivp E \ E x y \ E y z \ 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) + +lemma eq_imp_rel: + shows "equivp R \ a = b \ R a b" + by (simp add: equivp_reflp) + +lemma identity_equivp: + shows "equivp (op =)" + unfolding equivp_def + by auto + + +text {* Partial equivalences: not yet used anywhere *} +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_implies_part_equivp: + assumes a: "equivp E" + shows "part_equivp E" + using a + unfolding equivp_def part_equivp_def + by auto + +text {* Composition of Relations *} + +abbreviation + rel_conj (infixr "OOO" 75) +where + "r1 OOO r2 \ r1 OO r2 OO r1" + +lemma eq_comp_r: + shows "((op =) OOO R) = R" + by (auto simp add: expand_fun_eq) + +section {* Respects predicate *} + +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 + +section {* Function map and function relation *} + +definition + fun_map (infixr "--->" 55) +where +[simp]: "fun_map f g h x = g (h (f x))" + +definition + fun_rel (infixr "===>" 55) +where +[simp]: "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" + + +lemma fun_map_id: + shows "(id ---> id) = id" + by (simp add: expand_fun_eq id_def) + +lemma fun_rel_eq: + shows "((op =) ===> (op =)) = (op =)" + by (simp add: expand_fun_eq) + +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 fun_rel_id_asm: + assumes a: "\x y. R1 x y \ (A \ R2 (f x) (g y))" + shows "A \ (R1 ===> R2) f g" + using a by auto + + +section {* Quotient Predicate *} + +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)" + 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 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_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 + +lemma identity_quotient: + shows "Quotient (op =) id id" + unfolding Quotient_def id_def + by blast + +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" + using q1 q2 + unfolding Quotient_def + unfolding expand_fun_eq + by simp + moreover + have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + using q1 q2 + unfolding Quotient_def + by (simp (no_asm)) (metis) + moreover + have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s)" + unfolding expand_fun_eq + apply(auto) + 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 + +lemma abs_o_rep: + assumes a: "Quotient R Abs Rep" + shows "Abs o Rep = id" + unfolding expand_fun_eq + by (simp add: Quotient_abs_rep[OF a]) + +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 a Quotient_symp[OF q] Quotient_transp[OF q] + unfolding symp_def transp_def + 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 a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] + by metis + +lemma rep_abs_rsp_left: + assumes q: "Quotient R Abs Rep" + and a: "R x1 x2" + shows "R (Rep (Abs x1)) x2" + using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] + by metis + +text{* + 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 \ '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 + +section {* 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)" + using a + unfolding equivp_def + by (auto simp add: in_respects) + +lemma bex_reg_eqv: + fixes P :: "'a \ bool" + assumes a: "equivp R" + shows "Bex (Respects R) P = (Ex P)" + using a + unfolding equivp_def + by (auto simp add: in_respects) + +lemma ball_reg_right: + assumes a: "\x. R x \ P x \ Q x" + shows "All P \ Ball R Q" + using a by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma bex_reg_left: + assumes a: "\x. R x \ Q x \ P x" + shows "Bex R Q \ Ex P" + using a by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma ball_reg_left: + assumes a: "equivp R" + shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" + using a by (metis equivp_reflp in_respects) + +lemma bex_reg_right: + assumes a: "equivp R" + shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" + using a by (metis equivp_reflp in_respects) + +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: 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)) (\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: + assumes "\y. (\x\P. A x y) \ (\x. B x y)" + shows "(\x\P. \y. A x y) \ (\x. \y. B x y)" + using assms by auto + +lemma bex_ex_comm: + assumes "(\y. \x. A x y) \ (\y. \x\P. B x y)" + shows "(\x. \y. A x y) \ (\x\P. \y. B x y)" + using assms by auto + +section {* Bounded abstraction *} + +definition + Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" +where + "x \ p \ Babs p m x = m x" + +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 in_respects) + 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 + +lemma babs_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" + apply (rule ext) + apply (simp) + apply (subgoal_tac "Rep1 x \ 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 \ Respects R1 \ y \ 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 \ Babs (Respects R) P = P" + by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) + + +(* 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 bex1_rsp: + assumes a: "(R ===> (op =)) f g" + shows "Ex1 (\x. x \ Respects R \ f x) = Ex1 (\x. x \ Respects R \ g x)" + using a + by (simp add: Ex1_def in_respects) auto + +(* 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 Ball_def in_respects fun_map_def id_apply + by metis + +lemma ex_prs: + assumes a: "Quotient R absf repf" + shows "Bex (Respects R) ((absf ---> id) f) = Ex f" + using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply + by metis + +section {* Bex1_rel quantifier *} + +definition + Bex1_rel :: "('a \ 'a \ bool) \ ('a \ bool) \ bool" +where + "Bex1_rel R P \ (\x \ Respects R. P x) \ (\x \ Respects R. \y \ Respects R. ((P x \ P y) \ (R x y)))" + +lemma bex1_rel_aux: + "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R x\ \ Bex1_rel R y" + unfolding Bex1_rel_def + apply (erule conjE)+ + apply (erule bexE) + apply rule + apply (rule_tac x="xa" in bexI) + apply metis + apply metis + apply rule+ + apply (erule_tac x="xaa" in ballE) + prefer 2 + apply (metis) + apply (erule_tac x="ya" in ballE) + prefer 2 + apply (metis) + apply (metis in_respects) + done + +lemma bex1_rel_aux2: + "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R y\ \ Bex1_rel R x" + unfolding Bex1_rel_def + apply (erule conjE)+ + apply (erule bexE) + apply rule + apply (rule_tac x="xa" in bexI) + apply metis + apply metis + apply rule+ + apply (erule_tac x="xaa" in ballE) + prefer 2 + apply (metis) + apply (erule_tac x="ya" in ballE) + prefer 2 + apply (metis) + apply (metis in_respects) + done + +lemma bex1_rel_rsp: + assumes a: "Quotient R absf repf" + shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" + apply simp + apply clarify + apply rule + apply (simp_all add: bex1_rel_aux bex1_rel_aux2) + apply (erule bex1_rel_aux2) + apply assumption + done + + +lemma ex1_prs: + assumes a: "Quotient R absf repf" + shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" +apply simp +apply (subst Bex1_rel_def) +apply (subst Bex_def) +apply (subst Ex1_def) +apply simp +apply rule + apply (erule conjE)+ + apply (erule_tac exE) + apply (erule conjE) + apply (subgoal_tac "\y. R y y \ f (absf y) \ R x y") + apply (rule_tac x="absf x" in exI) + apply (simp) + apply rule+ + using a unfolding Quotient_def + apply metis + apply rule+ + apply (erule_tac x="x" in ballE) + apply (erule_tac x="y" in ballE) + apply simp + apply (simp add: in_respects) + apply (simp add: in_respects) +apply (erule_tac exE) + apply rule + apply (rule_tac x="repf x" in exI) + apply (simp only: in_respects) + apply rule + apply (metis Quotient_rel_rep[OF a]) +using a unfolding Quotient_def apply (simp) +apply rule+ +using a unfolding Quotient_def in_respects +apply metis +done + +lemma bex1_bexeq_reg: "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" + apply (simp add: Ex1_def Bex1_rel_def in_respects) + apply clarify + apply auto + apply (rule bexI) + apply assumption + apply (simp add: in_respects) + apply (simp add: in_respects) + apply auto + done + +section {* Various respects and preserve lemmas *} + +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 + +locale quot_type = + fixes R :: "'a \ 'a \ bool" + and Abs :: "('a \ bool) \ 'b" + and Rep :: "'b \ ('a \ bool)" + assumes equivp: "equivp R" + and rep_prop: "\y. \x. Rep y = R x" + and rep_inverse: "\x. Abs (Rep x) = x" + and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" + and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" +begin + +definition + abs::"'a \ 'b" +where + "abs x \ Abs (R x)" + +definition + rep::"'b \ 'a" +where + "rep a = Eps (Rep a)" + +lemma homeier_lem9: + shows "R (Eps (R x)) = R x" +proof - + have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) + then have "R x (Eps (R x))" by (rule someI) + then show "R (Eps (R x)) = R x" + using equivp unfolding equivp_def by simp +qed + +theorem homeier_thm10: + shows "abs (rep a) = a" + unfolding abs_def rep_def +proof - + from rep_prop + obtain x where eq: "Rep a = R x" by auto + have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp + also have "\ = Abs (R x)" using homeier_lem9 by simp + also have "\ = Abs (Rep a)" using eq by simp + also have "\ = a" using rep_inverse by simp + finally + show "Abs (R (Eps (Rep a))) = a" by simp +qed + +lemma homeier_lem7: + shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") +proof - + have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) + also have "\ = ?LHS" by (simp add: abs_inverse) + finally show "?LHS = ?RHS" by simp +qed + +theorem homeier_thm11: + shows "R r r' = (abs r = abs r')" + unfolding abs_def + by (simp only: equivp[simplified equivp_def] homeier_lem7) + +lemma rep_refl: + shows "R (rep a) (rep a)" + unfolding rep_def + by (simp add: equivp[simplified equivp_def]) + + +lemma rep_abs_rsp: + shows "R f (rep (abs g)) = R f g" + and "R (rep (abs g)) f = R g f" + by (simp_all add: homeier_thm10 homeier_thm11) + +lemma Quotient: + shows "Quotient R abs rep" + unfolding Quotient_def + apply(simp add: homeier_thm10) + apply(simp add: rep_refl) + apply(subst homeier_thm11[symmetric]) + apply(simp add: equivp[simplified equivp_def]) + done + +end + +section {* ML setup *} + +text {* Auxiliary data for the quotient package *} + +use "quotient_info.ML" + +declare [[map "fun" = (fun_map, fun_rel)]] + +lemmas [quot_thm] = fun_quotient +lemmas [quot_respect] = quot_rel_rsp +lemmas [quot_equiv] = identity_equivp + + +text {* Lemmas about simplifying id's. *} +lemmas [id_simps] = + id_def[symmetric] + fun_map_id + id_apply + id_o + o_id + eq_comp_r + +text {* Translation functions for the lifting process. *} +use "quotient_term.ML" + + +text {* Definitions of the quotient types. *} +use "quotient_typ.ML" + + +text {* Definitions for quotient constants. *} +use "quotient_def.ML" + + +text {* + An auxiliary constant for recording some information + about the lifted theorem in a tactic. +*} +definition + "Quot_True x \ True" + +lemma + shows QT_all: "Quot_True (All P) \ Quot_True P" + and QT_ex: "Quot_True (Ex P) \ Quot_True P" + and QT_ex1: "Quot_True (Ex1 P) \ Quot_True P" + and QT_lam: "Quot_True (\x. P x) \ (\x. Quot_True (P x))" + and QT_ext: "(\x. Quot_True (a x) \ f x = g x) \ (Quot_True a \ f = g)" + by (simp_all add: Quot_True_def ext) + +lemma QT_imp: "Quot_True a \ Quot_True b" + by (simp add: Quot_True_def) + + +text {* Tactics for proving the lifted theorems *} +use "quotient_tacs.ML" + +section {* Methods / Interface *} + +(* TODO inline *) +ML {* +fun mk_method1 tac thms ctxt = + SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) + +fun mk_method2 tac ctxt = + SIMPLE_METHOD (HEADGOAL (tac ctxt)) +*} + +method_setup lifting = + {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} + {* lifts theorems to quotient types *} + +method_setup lifting_setup = + {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} + {* sets up the three goals for the quotient lifting procedure *} + +method_setup regularize = + {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} + {* proves the regularization goals from the quotient lifting procedure *} + +method_setup injection = + {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *} + {* proves the rep/abs injection goals from the quotient lifting procedure *} + +method_setup cleaning = + {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} + {* proves the cleaning goals from the quotient lifting procedure *} + +attribute_setup quot_lifted = + {* Scan.succeed Quotient_Tacs.lifted_attrib *} + {* lifts theorems to quotient types *} + +end + diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Quotient_List.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Quotient_List.thy Thu Feb 11 10:06:02 2010 +0100 @@ -0,0 +1,232 @@ +(* Title: Quotient_List.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_List +imports Quotient List +begin + +section {* Quotient infrastructure for the list type. *} + +fun + list_rel +where + "list_rel R [] [] = True" +| "list_rel R (x#xs) [] = False" +| "list_rel R [] (x#xs) = False" +| "list_rel R (x#xs) (y#ys) = (R x y \ list_rel R xs ys)" + +declare [[map list = (map, list_rel)]] + +lemma split_list_all: + shows "(\x. P x) \ P [] \ (\x xs. P (x#xs))" + apply(auto) + apply(case_tac x) + apply(simp_all) + done + +lemma map_id[id_simps]: + shows "map id = id" + apply(simp add: expand_fun_eq) + apply(rule allI) + apply(induct_tac x) + apply(simp_all) + done + + +lemma list_rel_reflp: + shows "equivp R \ list_rel R xs xs" + apply(induct xs) + apply(simp_all add: equivp_reflp) + done + +lemma list_rel_symp: + assumes a: "equivp R" + shows "list_rel R xs ys \ list_rel R ys xs" + apply(induct xs ys rule: list_induct2') + apply(simp_all) + apply(rule equivp_symp[OF a]) + apply(simp) + done + +lemma list_rel_transp: + assumes a: "equivp R" + shows "list_rel R xs1 xs2 \ list_rel R xs2 xs3 \ list_rel R xs1 xs3" + apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2') + apply(simp_all) + apply(case_tac xs3) + apply(simp_all) + apply(rule equivp_transp[OF a]) + apply(auto) + done + +lemma list_equivp[quot_equiv]: + assumes a: "equivp R" + shows "equivp (list_rel R)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(subst split_list_all) + apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a]) + apply(blast intro: list_rel_symp[OF a]) + apply(blast intro: list_rel_transp[OF a]) + done + +lemma list_rel_rel: + assumes q: "Quotient R Abs Rep" + shows "list_rel R r s = (list_rel R r r \ list_rel R s s \ (map Abs r = map Abs s))" + apply(induct r s rule: list_induct2') + apply(simp_all) + using Quotient_rel[OF q] + apply(metis) + done + +lemma list_quotient[quot_thm]: + assumes q: "Quotient R Abs Rep" + shows "Quotient (list_rel R) (map Abs) (map Rep)" + unfolding Quotient_def + apply(subst split_list_all) + apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id) + apply(rule conjI) + apply(rule allI) + apply(induct_tac a) + apply(simp) + apply(simp) + apply(simp add: Quotient_rep_reflp[OF q]) + apply(rule allI)+ + apply(rule list_rel_rel[OF q]) + done + + +lemma cons_prs_aux: + assumes q: "Quotient R Abs Rep" + shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" + by (induct t) (simp_all add: Quotient_abs_rep[OF q]) + +lemma cons_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" + by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) + (simp) + +lemma cons_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)" + by (auto) + +lemma nil_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "map Abs [] = []" + by simp + +lemma nil_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "list_rel R [] []" + by simp + +lemma map_prs_aux: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" + by (induct l) + (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + + +lemma map_prs[quot_preserve]: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" + by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) + (simp) + + +lemma map_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(rule allI)+ + apply (induct_tac xa ya rule: list_induct2') + apply simp_all + done + +lemma foldr_prs_aux: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" + by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + +lemma foldr_prs[quot_preserve]: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" + by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) + (simp) + +lemma foldl_prs_aux: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" + by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + + +lemma foldl_prs[quot_preserve]: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" + by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) + (simp) + +lemma list_rel_empty: + shows "list_rel R [] b \ length b = 0" + by (induct b) (simp_all) + +lemma list_rel_len: + shows "list_rel R a b \ length a = length b" + apply (induct a arbitrary: b) + apply (simp add: list_rel_empty) + apply (case_tac b) + apply simp_all + done + +(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) +lemma foldl_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" + apply(auto) + apply (subgoal_tac "R1 xa ya \ list_rel R2 xb yb \ R1 (foldl x xa xb) (foldl y ya yb)") + apply simp + apply (rule_tac x="xa" in spec) + apply (rule_tac x="ya" in spec) + apply (rule_tac xs="xb" and ys="yb" in list_induct2) + apply (rule list_rel_len) + apply (simp_all) + done + +lemma foldr_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" + apply auto + apply(subgoal_tac "R2 xb yb \ list_rel R1 xa ya \ R2 (foldr x xa xb) (foldr y ya yb)") + apply simp + apply (rule_tac xs="xa" and ys="ya" in list_induct2) + apply (rule list_rel_len) + apply (simp_all) + done + +lemma list_rel_eq[id_simps]: + shows "(list_rel (op =)) = (op =)" + unfolding expand_fun_eq + apply(rule allI)+ + apply(induct_tac x xa rule: list_induct2') + apply(simp_all) + done + +lemma list_rel_refl: + assumes a: "\x y. R x y = (R x = R y)" + shows "list_rel R x x" + by (induct x) (auto simp add: a) + +end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Quotient_Option.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Quotient_Option.thy Thu Feb 11 10:06:02 2010 +0100 @@ -0,0 +1,80 @@ +(* Title: Quotient_Option.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_Option +imports Quotient +begin + +section {* Quotient infrastructure for the option type. *} + +fun + option_rel +where + "option_rel R None None = True" +| "option_rel R (Some x) None = False" +| "option_rel R None (Some x) = False" +| "option_rel R (Some x) (Some y) = R x y" + +declare [[map option = (Option.map, option_rel)]] + +text {* should probably be in Option.thy *} +lemma split_option_all: + shows "(\x. P x) \ P None \ (\a. P (Some a))" + apply(auto) + apply(case_tac x) + apply(simp_all) + done + +lemma option_quotient[quot_thm]: + assumes q: "Quotient R Abs Rep" + shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" + unfolding Quotient_def + apply(simp add: split_option_all) + apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) + using q + unfolding Quotient_def + apply(blast) + done + +lemma option_equivp[quot_equiv]: + assumes a: "equivp R" + shows "equivp (option_rel R)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(simp_all add: split_option_all) + apply(blast intro: equivp_reflp[OF a]) + apply(blast intro: equivp_symp[OF a]) + apply(blast intro: equivp_transp[OF a]) + done + +lemma option_None_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "option_rel R None None" + by simp + +lemma option_Some_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "(R ===> option_rel R) Some Some" + by simp + +lemma option_None_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "Option.map Abs None = None" + by simp + +lemma option_Some_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "(Rep ---> Option.map Abs) Some = Some" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q]) + done + +lemma option_map_id[id_simps]: + shows "Option.map id = id" + by (simp add: expand_fun_eq split_option_all) + +lemma option_rel_eq[id_simps]: + shows "option_rel (op =) = (op =)" + by (simp add: expand_fun_eq split_option_all) + +end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Quotient_Product.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Quotient_Product.thy Thu Feb 11 10:06:02 2010 +0100 @@ -0,0 +1,104 @@ +(* Title: Quotient_Product.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_Product +imports Quotient +begin + +section {* Quotient infrastructure for the product type. *} + +fun + prod_rel +where + "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" + +declare [[map * = (prod_fun, prod_rel)]] + + +lemma prod_equivp[quot_equiv]: + assumes a: "equivp R1" + assumes b: "equivp R2" + shows "equivp (prod_rel R1 R2)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(simp_all add: split_paired_all) + apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) + apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) + apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) + done + +lemma prod_quotient[quot_thm]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" + unfolding Quotient_def + apply(simp add: split_paired_all) + apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) + apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) + using q1 q2 + unfolding Quotient_def + apply(blast) + done + +lemma Pair_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" + by simp + +lemma Pair_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + done + +lemma fst_rsp[quot_respect]: + assumes "Quotient R1 Abs1 Rep1" + assumes "Quotient R2 Abs2 Rep2" + shows "(prod_rel R1 R2 ===> R1) fst fst" + by simp + +lemma fst_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q1]) + done + +lemma snd_rsp[quot_respect]: + assumes "Quotient R1 Abs1 Rep1" + assumes "Quotient R2 Abs2 Rep2" + shows "(prod_rel R1 R2 ===> R2) snd snd" + by simp + +lemma snd_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q2]) + done + +lemma split_rsp[quot_respect]: + shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" + by auto + +lemma split_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" + by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + +lemma prod_fun_id[id_simps]: + shows "prod_fun id id = id" + by (simp add: prod_fun_def) + +lemma prod_rel_eq[id_simps]: + shows "prod_rel (op =) (op =) = (op =)" + by (simp add: expand_fun_eq) + + +end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Quotient_Sum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Quotient_Sum.thy Thu Feb 11 10:06:02 2010 +0100 @@ -0,0 +1,96 @@ +(* Title: Quotient_Sum.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_Sum +imports Quotient +begin + +section {* Quotient infrastructure for the sum type. *} + +fun + sum_rel +where + "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" + +fun + sum_map +where + "sum_map f1 f2 (Inl a) = Inl (f1 a)" +| "sum_map f1 f2 (Inr a) = Inr (f2 a)" + +declare [[map "+" = (sum_map, sum_rel)]] + + +text {* should probably be in Sum_Type.thy *} +lemma split_sum_all: + shows "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" + apply(auto) + apply(case_tac x) + apply(simp_all) + done + +lemma sum_equivp[quot_equiv]: + assumes a: "equivp R1" + assumes b: "equivp R2" + shows "equivp (sum_rel R1 R2)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(simp_all add: split_sum_all) + apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) + apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) + apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) + done + +lemma sum_quotient[quot_thm]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" + unfolding Quotient_def + apply(simp add: split_sum_all) + apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) + apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) + using q1 q2 + unfolding Quotient_def + apply(blast)+ + done + +lemma sum_Inl_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R1 ===> sum_rel R1 R2) Inl Inl" + by simp + +lemma sum_Inr_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R2 ===> sum_rel R1 R2) Inr Inr" + by simp + +lemma sum_Inl_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q1]) + done + +lemma sum_Inr_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q2]) + done + +lemma sum_map_id[id_simps]: + shows "sum_map id id = id" + by (simp add: expand_fun_eq split_sum_all) + +lemma sum_rel_eq[id_simps]: + shows "sum_rel (op =) (op =) = (op =)" + by (simp add: expand_fun_eq split_sum_all) + +end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/ROOT.ML --- a/Quot/ROOT.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/ROOT.ML Thu Feb 11 10:06:02 2010 +0100 @@ -1,7 +1,7 @@ quick_and_dirty := true; no_document use_thys - ["QuotMain", + ["Quotient", "Examples/AbsRepTest", "Examples/FSet", "Examples/FSet2", diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/quotient_def.ML Thu Feb 11 10:06:02 2010 +0100 @@ -6,7 +6,7 @@ *) signature QUOTIENT_DEF = -sig +sig val quotient_def: mixfix -> Attrib.binding -> term -> term -> local_theory -> (term * thm) * local_theory @@ -32,7 +32,7 @@ (** Interface and Syntax Setup **) -(* The ML-interface for a quotient definition takes +(* The ML-interface for a quotient definition takes as argument: - the mixfix annotation @@ -41,11 +41,11 @@ - the rhs of the definition as term It returns the defined constant and its definition - theorem; stores the data in the qconsts data slot. + theorem; stores the data in the qconsts data slot. Restriction: At the moment the right-hand side must - be a terms composed of constant. Similarly the - left-hand side must be a single constant. + be a terms composed of constant. Similarly the + left-hand side must be a single constant. *) fun quotient_def mx attr lhs rhs lthy = let @@ -87,7 +87,7 @@ (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- OuterParse.term) -val _ = OuterSyntax.local_theory "quotient_definition" +val _ = OuterSyntax.local_theory "quotient_definition" "definition for constants over the quotient type" OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/quotient_info.ML Thu Feb 11 10:06:02 2010 +0100 @@ -13,8 +13,8 @@ type maps_info = {mapfun: string, relmap: string} val maps_defined: theory -> string -> bool val maps_lookup: theory -> string -> maps_info (* raises NotFound *) - val maps_update_thy: string -> maps_info -> theory -> theory - val maps_update: string -> maps_info -> Proof.context -> Proof.context + val maps_update_thy: string -> maps_info -> theory -> theory + val maps_update: string -> maps_info -> Proof.context -> Proof.context val print_mapsinfo: Proof.context -> unit type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} @@ -36,8 +36,8 @@ val equiv_rules_get: Proof.context -> thm list val equiv_rules_add: attribute - val rsp_rules_get: Proof.context -> thm list - val prs_rules_get: Proof.context -> thm list + val rsp_rules_get: Proof.context -> thm list + val prs_rules_get: Proof.context -> thm list val id_simps_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute @@ -61,10 +61,10 @@ val extend = I val merge = Symtab.merge (K true)) -fun maps_defined thy s = +fun maps_defined thy s = Symtab.defined (MapsData.get thy) s -fun maps_lookup thy s = +fun maps_lookup thy s = case (Symtab.lookup (MapsData.get thy) s) of SOME map_fun => map_fun | NONE => raise NotFound @@ -72,12 +72,12 @@ fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) -fun maps_attribute_aux s minfo = Thm.declaration_attribute +fun maps_attribute_aux s minfo = Thm.declaration_attribute (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) (* attribute to be used in declare statements *) -fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = -let +fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = +let val thy = ProofContext.theory_of ctxt val tyname = Sign.intern_type thy tystr val mapname = Sign.intern_const thy mapstr @@ -89,21 +89,21 @@ maps_attribute_aux tyname {mapfun = mapname, relmap = relname} end -val maps_attr_parser = +val maps_attr_parser = Args.context -- Scan.lift - ((Args.name --| OuterParse.$$$ "=") -- - (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- + ((Args.name --| OuterParse.$$$ "=") -- + (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- Args.name --| OuterParse.$$$ ")")) val _ = Context.>> (Context.map_theory - (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) + (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) "declaration of map information")) fun print_mapsinfo ctxt = let - fun prt_map (ty_name, {mapfun, relmap}) = + fun prt_map (ty_name, {mapfun, relmap}) = Pretty.block (Library.separate (Pretty.brk 2) - (map Pretty.str + (map Pretty.str ["type:", ty_name, "map:", mapfun, "relation map:", relmap])) @@ -111,11 +111,11 @@ MapsData.get (ProofContext.theory_of ctxt) |> Symtab.dest |> map (prt_map) - |> Pretty.big_list "maps for type constructors:" + |> Pretty.big_list "maps for type constructors:" |> Pretty.writeln end - + (* info about quotient types *) type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} @@ -123,7 +123,7 @@ (type T = quotdata_info Symtab.table val empty = Symtab.empty val extend = I - val merge = Symtab.merge (K true)) + val merge = Symtab.merge (K true)) fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = {qtyp = Morphism.typ phi qtyp, @@ -160,7 +160,7 @@ QuotData.get (ProofContext.theory_of ctxt) |> Symtab.dest |> map (prt_quot o snd) - |> Pretty.big_list "quotients:" + |> Pretty.big_list "quotients:" |> Pretty.writeln end @@ -223,7 +223,7 @@ |> map snd |> flat |> map prt_qconst - |> Pretty.big_list "quotient constants:" + |> Pretty.big_list "quotient constants:" |> Pretty.writeln end @@ -266,7 +266,7 @@ (* setup of the theorem lists *) -val _ = Context.>> (Context.map_theory +val _ = Context.>> (Context.map_theory (EquivRules.setup #> RspRules.setup #> PrsRules.setup #> diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/quotient_tacs.ML Thu Feb 11 10:06:02 2010 +0100 @@ -102,7 +102,7 @@ Since the left-hand-side contains a non-pattern '?P (f ?x)' we rely on unification/instantiation to check whether the - theorem applies and return NONE if it doesn't. + theorem applies and return NONE if it doesn't. *) fun calculate_inst ctxt ball_bex_thm redex R1 R2 = let @@ -122,14 +122,14 @@ fun ball_bex_range_simproc ss redex = let val ctxt = Simplifier.the_context ss -in +in case redex of - (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 - | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 | _ => NONE @@ -151,7 +151,7 @@ 5. then simplification like 0 - finally jump back to 1 + finally jump back to 1 *) fun regularize_tac ctxt = let @@ -159,18 +159,18 @@ val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) - val simpset = (mk_minimal_ss ctxt) + val simpset = (mk_minimal_ss ctxt) addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [simproc] + addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) in simp_tac simpset THEN' - REPEAT_ALL_NEW (CHANGED o FIRST' + REPEAT_ALL_NEW (CHANGED o FIRST' [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, resolve_tac (Inductive.get_monos ctxt), resolve_tac @{thms ball_all_comm bex_ex_comm}, - resolve_tac eq_eqvs, + resolve_tac eq_eqvs, simp_tac simpset]) end @@ -179,7 +179,7 @@ (*** Injection Tactic ***) (* Looks for Quot_True assumptions, and in case its parameter - is an application, it returns the function and the argument. + is an application, it returns the function and the argument. *) fun find_qt_asm asms = let @@ -216,13 +216,13 @@ | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm | _ => Conv.all_conv ctrm -fun quot_true_tac ctxt fnctn = +fun quot_true_tac ctxt fnctn = CONVERSION ((Conv.params_conv ~1 (fn ctxt => (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) -fun dest_comb (f $ a) = (f, a) -fun dest_bcomb ((_ $ l) $ r) = (l, r) +fun dest_comb (f $ a) = (f, a) +fun dest_bcomb ((_ $ l) $ r) = (l, r) fun unlam t = case t of @@ -236,7 +236,7 @@ (* We apply apply_rsp only in case if the type needs lifting. This is the case if the type of the data in the Quot_True - assumption is different from the corresponding type in the goal. + assumption is different from the corresponding type in the goal. *) val apply_rsp_tac = Subgoal.FOCUS (fn {concl, asms, context,...} => @@ -265,7 +265,7 @@ end) (* Instantiates and applies 'equals_rsp'. Since the theorem is - complex we rely on instantiation to tell us if it applies + complex we rely on instantiation to tell us if it applies *) fun equals_rsp_tac R ctxt = let @@ -304,7 +304,7 @@ -(* Injection means to prove that the regularised theorem implies +(* Injection means to prove that the regularised theorem implies the abs/rep injected one. The deterministic part: @@ -317,7 +317,7 @@ - solve 'relation of relations' goals using quot_rel_rsp - remove rep_abs from the right side (Lambdas under respects may have left us some assumptions) - + Then in order: - split applications of lifted type (apply_rsp) - split applications of non-lifted type (cong_tac) @@ -364,7 +364,7 @@ (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] -| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => +| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE' (equals_rsp_tac R ctxt THEN' RANGE [ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) @@ -379,7 +379,7 @@ (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) (* observe fun_map *) | _ $ _ $ _ - => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) + => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt | _ => K no_tac @@ -428,7 +428,7 @@ ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => if member (op=) xs h then Conv.all_conv ctrm - else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm + else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm | _ => Conv.all_conv ctrm fun fun_map_conv xs ctxt ctrm = @@ -470,7 +470,7 @@ Then solves the quotient assumptions to get Rep2 and Abs1 Finally instantiates the function f using make_inst If Rep2 is an identity then the pattern is simpler and - make_inst_id is used + make_inst_id is used *) fun lambda_prs_simple_conv ctxt ctrm = case (term_of ctrm) of @@ -501,20 +501,20 @@ (* Cleaning consists of: 1. unfolding of ---> in front of everything, except - bound variables (this prevents lambda_prs from + bound variables (this prevents lambda_prs from becoming stuck) 2. simplification with lambda_prs - 3. simplification with: + 3. simplification with: - - Quotient_abs_rep Quotient_rel_rep + - Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs - - id_simps and preservation lemmas and + - id_simps and preservation lemmas and - - symmetric versions of the definitions - (that is definitions of quotient constants + - symmetric versions of the definitions + (that is definitions of quotient constants are folded) 4. test for refl @@ -545,10 +545,10 @@ fun inst_spec_tac ctrms = EVERY' (map (dtac o inst_spec) ctrms) -fun all_list xs trm = +fun all_list xs trm = fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm -fun apply_under_Trueprop f = +fun apply_under_Trueprop f = HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop fun gen_frees_tac ctxt = @@ -577,7 +577,7 @@ - 2nd prem is the rep/abs injection step - 3rd prem is the cleaning part - the Quot_True premise in 2nd records the lifted theorem + the Quot_True premise in 2nd records the lifted theorem *) val lifting_procedure_thm = @{lemma "[|A; @@ -590,7 +590,7 @@ let val rtrm_str = Syntax.string_of_term ctxt rtrm val qtrm_str = Syntax.string_of_term ctxt qtrm - val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, + val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, "", "does not match with original theorem", rtrm_str] in error msg @@ -629,22 +629,22 @@ (* Automatic Proofs *) val msg1 = "The regularize proof failed." -val msg2 = cat_lines ["The injection proof failed.", +val msg2 = cat_lines ["The injection proof failed.", "This is probably due to missing respects lemmas.", - "Try invoking the injection method manually to see", + "Try invoking the injection method manually to see", "which lemmas are missing."] val msg3 = "The cleaning proof failed." fun lift_tac ctxt rthms = let - fun mk_tac rthm = + fun mk_tac rthm = procedure_tac ctxt rthm - THEN' RANGE_WARN + THEN' RANGE_WARN [(regularize_tac ctxt, msg1), (all_injection_tac ctxt, msg2), (clean_tac ctxt, msg3)] in - simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) + simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) THEN' RANGE (map mk_tac rthms) end diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/quotient_term.ML Thu Feb 11 10:06:02 2010 +0100 @@ -41,9 +41,9 @@ (*** Aggregate Rep/Abs Function ***) -(* The flag RepF is for types in negative position; AbsF is for types - in positive position. Because of this, function types need to be - treated specially, since there the polarity changes. +(* The flag RepF is for types in negative position; AbsF is for types + in positive position. Because of this, function types need to be + treated specially, since there the polarity changes. *) datatype flag = AbsF | RepF @@ -56,7 +56,7 @@ fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) -fun mk_fun_compose flag (trm1, trm2) = +fun mk_fun_compose flag (trm1, trm2) = case flag of AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 @@ -73,13 +73,13 @@ (* makes a Free out of a TVar *) fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) -(* produces an aggregate map function for the - rty-part of a quotient definition; abstracts - over all variables listed in vs (these variables - correspond to the type variables in rty) - - for example for: (?'a list * ?'b) - it produces: %a b. prod_map (map a) b +(* produces an aggregate map function for the + rty-part of a quotient definition; abstracts + over all variables listed in vs (these variables + correspond to the type variables in rty) + + for example for: (?'a list * ?'b) + it produces: %a b. prod_map (map a) b *) fun mk_mapfun ctxt vs rty = let @@ -95,8 +95,8 @@ fold_rev Term.lambda vs' (mk_mapfun_aux rty) end -(* looks up the (varified) rty and qty for - a quotient definition +(* looks up the (varified) rty and qty for + a quotient definition *) fun get_rty_qty ctxt s = let @@ -107,9 +107,9 @@ (#rtyp qdata, #qtyp qdata) end -(* takes two type-environments and looks - up in both of them the variable v, which - must be listed in the environment +(* takes two type-environments and looks + up in both of them the variable v, which + must be listed in the environment *) fun double_lookup rtyenv qtyenv v = let @@ -145,58 +145,58 @@ fun absrep_match_err ctxt ty_pat ty = let val ty_pat_str = Syntax.string_of_typ ctxt ty_pat - val ty_str = Syntax.string_of_typ ctxt ty + val ty_str = Syntax.string_of_typ ctxt ty in - raise LIFT_MATCH (space_implode " " + raise LIFT_MATCH (space_implode " " ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) end (** generation of an aggregate absrep function **) -(* - In case of equal types we just return the identity. - +(* - In case of equal types we just return the identity. + - In case of TFrees we also return the identity. - - - In case of function types we recurse taking - the polarity change into account. - - - If the type constructors are equal, we recurse for the - arguments and build the appropriate map function. - - - If the type constructors are unequal, there must be an - instance of quotient types: - - - we first look up the corresponding rty_pat and qty_pat - from the quotient definition; the arguments of qty_pat - must be some distinct TVars - - we then match the rty_pat with rty and qty_pat with qty; - if matching fails the types do not correspond -> error - - the matching produces two environments; we look up the - assignments for the qty_pat variables and recurse on the - assignments - - we prefix the aggregate map function for the rty_pat, - which is an abstraction over all type variables - - finally we compose the result with the appropriate + + - In case of function types we recurse taking + the polarity change into account. + + - If the type constructors are equal, we recurse for the + arguments and build the appropriate map function. + + - If the type constructors are unequal, there must be an + instance of quotient types: + + - we first look up the corresponding rty_pat and qty_pat + from the quotient definition; the arguments of qty_pat + must be some distinct TVars + - we then match the rty_pat with rty and qty_pat with qty; + if matching fails the types do not correspond -> error + - the matching produces two environments; we look up the + assignments for the qty_pat variables and recurse on the + assignments + - we prefix the aggregate map function for the rty_pat, + which is an abstraction over all type variables + - finally we compose the result with the appropriate absrep function in case at least one argument produced a non-identity function / otherwise we just return the appropriate absrep - function - - The composition is necessary for types like - - ('a list) list / ('a foo) foo - - The matching is necessary for types like - - ('a * 'a) list / 'a bar + function + + The composition is necessary for types like + + ('a list) list / ('a foo) foo + + The matching is necessary for types like + + ('a * 'a) list / 'a bar The test is necessary in order to eliminate superfluous - identity maps. -*) + identity maps. +*) fun absrep_fun flag ctxt (rty, qty) = - if rty = qty + if rty = qty then mk_identity rty else case (rty, qty) of @@ -209,12 +209,12 @@ end | (Type (s, tys), Type (s', tys')) => if s = s' - then + then let val args = map (absrep_fun flag ctxt) (tys ~~ tys') in list_comb (get_mapfun ctxt s, args) - end + end else let val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' @@ -222,8 +222,8 @@ val qtyenv = match ctxt absrep_match_err qty_pat qty val args_aux = map (double_lookup rtyenv qtyenv) vs val args = map (absrep_fun flag ctxt) args_aux - val map_fun = mk_mapfun ctxt vs rty_pat - val result = list_comb (map_fun, args) + val map_fun = mk_mapfun ctxt vs rty_pat + val result = list_comb (map_fun, args) in if forall is_identity args then absrep_const flag ctxt s' @@ -253,7 +253,7 @@ (* instantiates TVars so that the term is of type ty *) fun force_typ ctxt trm ty = let - val thy = ProofContext.theory_of ctxt + val thy = ProofContext.theory_of ctxt val trm_ty = fastype_of trm val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty in @@ -269,7 +269,7 @@ fun get_relmap ctxt s = let val thy = ProofContext.theory_of ctxt - val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") + val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn in Const (relmap, dummyT) @@ -292,7 +292,7 @@ fun get_equiv_rel ctxt s = let val thy = ProofContext.theory_of ctxt - val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") + val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") in #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn end @@ -300,14 +300,14 @@ fun equiv_match_err ctxt ty_pat ty = let val ty_pat_str = Syntax.string_of_typ ctxt ty_pat - val ty_str = Syntax.string_of_typ ctxt ty + val ty_str = Syntax.string_of_typ ctxt ty in - raise LIFT_MATCH (space_implode " " + raise LIFT_MATCH (space_implode " " ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) end -(* builds the aggregate equivalence relation - that will be the argument of Respects +(* builds the aggregate equivalence relation + that will be the argument of Respects *) fun equiv_relation ctxt (rty, qty) = if rty = qty @@ -315,26 +315,26 @@ else case (rty, qty) of (Type (s, tys), Type (s', tys')) => - if s = s' - then + if s = s' + then let val args = map (equiv_relation ctxt) (tys ~~ tys') in - list_comb (get_relmap ctxt s, args) - end - else + list_comb (get_relmap ctxt s, args) + end + else let val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' val rtyenv = match ctxt equiv_match_err rty_pat rty val qtyenv = match ctxt equiv_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs + val args_aux = map (double_lookup rtyenv qtyenv) vs val args = map (equiv_relation ctxt) args_aux - val rel_map = mk_relmap ctxt vs rty_pat + val rel_map = mk_relmap ctxt vs rty_pat val result = list_comb (rel_map, args) val eqv_rel = get_equiv_rel ctxt s' val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) in - if forall is_eq args + if forall is_eq args then eqv_rel' else mk_rel_compose (result, eqv_rel') end @@ -349,17 +349,17 @@ (*** Regularization ***) (* Regularizing an rtrm means: - - - Quantifiers over types that need lifting are replaced + + - Quantifiers over types that need lifting are replaced by bounded quantifiers, for example: All P ----> All (Respects R) P where the aggregate relation R is given by the rty and qty; - + - Abstractions over types that need lifting are replaced by bounded abstractions, for example: - + %x. P ----> Ball (Respects R) %x. P - Equalities over types that need lifting are replaced by @@ -392,10 +392,10 @@ val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) val mk_resp = Const (@{const_name Respects}, dummyT) -(* - applies f to the subterm of an abstraction, - otherwise to the given term, - - used by regularize, therefore abstracted - variables do not have to be treated specially +(* - applies f to the subterm of an abstraction, + otherwise to the given term, + - used by regularize, therefore abstracted + variables do not have to be treated specially *) fun apply_subt f (trm1, trm2) = case (trm1, trm2) of @@ -433,10 +433,10 @@ (* produces a regularized version of rtrm - - the result might contain dummyTs + - the result might contain dummyTs - - for regularisation we do not need any - special treatment of bound variables + - for regularisation we do not need any + special treatment of bound variables *) fun regularize_trm ctxt (rtrm, qtrm) = case (rtrm, qtrm) of @@ -474,8 +474,8 @@ end | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _, - (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ - (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), + (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ + (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), Const (@{const_name "Ex1"}, ty') $ t') => let val t_ = incr_boundvars (~1) t @@ -495,7 +495,7 @@ else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end - | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, + | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') @@ -506,7 +506,7 @@ else mk_ball $ (mk_resp $ resrel) $ subtrm end - | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, + | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') @@ -527,18 +527,18 @@ else mk_bex1_rel $ resrel $ subtrm end - | (* equalities need to be replaced by appropriate equivalence relations *) + | (* equalities need to be replaced by appropriate equivalence relations *) (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => if ty = ty' then rtrm - else equiv_relation ctxt (domain_type ty, domain_type ty') + else equiv_relation ctxt (domain_type ty, domain_type ty') - | (* in this case we just check whether the given equivalence relation is correct *) + | (* in this case we just check whether the given equivalence relation is correct *) (rel, Const (@{const_name "op ="}, ty')) => let val rel_ty = fastype_of rel - val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') + val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') in - if rel' aconv rel then rtrm + if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel' end @@ -557,7 +557,7 @@ if Pattern.matches thy (rtrm', rtrm) then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm end - end + end | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => @@ -571,11 +571,11 @@ regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') | (Bound i, Bound i') => - if i = i' then rtrm + if i = i' then rtrm else raise (LIFT_MATCH "regularize (bounds mismatch)") | _ => - let + let val rtrm_str = Syntax.string_of_term ctxt rtrm val qtrm_str = Syntax.string_of_term ctxt qtrm in @@ -583,7 +583,7 @@ end fun regularize_trm_chk ctxt (rtrm, qtrm) = - regularize_trm ctxt (rtrm, qtrm) + regularize_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt @@ -595,22 +595,22 @@ For abstractions: - * If the type of the abstraction needs lifting, then we add Rep/Abs + * If the type of the abstraction needs lifting, then we add Rep/Abs around the abstraction; otherwise we leave it unchanged. - + For applications: - - * If the application involves a bounded quantifier, we recurse on + + * If the application involves a bounded quantifier, we recurse on the second argument. If the application is a bounded abstraction, we always put an Rep/Abs around it (since bounded abstractions - are assumed to always need lifting). Otherwise we recurse on both + are assumed to always need lifting). Otherwise we recurse on both arguments. For constants: - * If the constant is (op =), we leave it always unchanged. + * If the constant is (op =), we leave it always unchanged. Otherwise the type of the constant needs lifting, we put - and Rep/Abs around it. + and Rep/Abs around it. For free variables: @@ -619,13 +619,13 @@ Vars case cannot occur. *) -fun mk_repabs ctxt (T, T') trm = +fun mk_repabs ctxt (T, T') trm = absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) fun inj_repabs_err ctxt msg rtrm qtrm = let val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm in raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) end @@ -662,11 +662,11 @@ else mk_repabs ctxt (rty, qty) result end - | (t $ s, t' $ s') => + | (t $ s, t' $ s') => (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) - | (Free (_, T), Free (_, T')) => - if T = T' then rtrm + | (Free (_, T), Free (_, T')) => + if T = T' then rtrm else mk_repabs ctxt (T, T') rtrm | (_, Const (@{const_name "op ="}, _)) => rtrm @@ -674,15 +674,15 @@ | (_, Const (_, T')) => let val rty = fastype_of rtrm - in + in if rty = T' then rtrm else mk_repabs ctxt (rty, T') rtrm - end - + end + | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = - inj_repabs_trm ctxt (rtrm, qtrm) + inj_repabs_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/quotient_typ.ML Thu Feb 11 10:06:02 2010 +0100 @@ -7,10 +7,10 @@ signature QUOTIENT_TYPE = sig - val quotient_type: ((string list * binding * mixfix) * (typ * term)) list + val quotient_type: ((string list * binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state - val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list + val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list -> Proof.context -> Proof.state end; @@ -41,7 +41,7 @@ let val goals' = map (rpair []) goals fun after_qed' thms = after_qed (the_single thms) -in +in Proof.theorem_i NONE after_qed' [goals'] ctxt end @@ -155,7 +155,7 @@ (* quot_type theorem *) val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 - (* quotient theorem *) + (* quotient theorem *) val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name @@ -189,22 +189,22 @@ else [qty_str ^ "illegal schematic variable(s) in the relation."] val dup_vs = - (case duplicates (op =) vs of + (case duplicates (op =) vs of [] => [] | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups]) val extra_rty_tfrees = - (case subtract (op =) vs rty_tfreesT of + (case subtract (op =) vs rty_tfreesT of [] => [] | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras]) val extra_rel_tfrees = - (case subtract (op =) vs rel_tfrees of + (case subtract (op =) vs rel_tfrees of [] => [] | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras]) - + val illegal_rel_frees = - (case rel_frees of + (case rel_frees of [] => [] | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) @@ -248,28 +248,28 @@ relations are equivalence relations *) -fun quotient_type quot_list lthy = +fun quotient_type quot_list lthy = let - (* sanity check *) - val _ = List.app sanity_check quot_list + (* sanity check *) + val _ = List.app sanity_check quot_list val _ = List.app (map_check lthy) quot_list fun mk_goal (rty, rel) = let val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} - in + in HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) end val goals = map (mk_goal o snd) quot_list - + fun after_qed thms lthy = fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd in theorem after_qed goals lthy end - -fun quotient_type_cmd specs lthy = + +fun quotient_type_cmd specs lthy = let fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = let @@ -278,12 +278,12 @@ val lthy1 = Variable.declare_typ rty lthy val pre_rel = Syntax.parse_term lthy1 rel_str val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel - val rel = Syntax.check_term lthy1 pre_rel' + val rel = Syntax.check_term lthy1 pre_rel' val lthy2 = Variable.declare_term rel lthy1 - + (* old parsing *) (* val rty = Syntax.read_typ lthy rty_str - val rel = Syntax.read_term lthy rel_str *) + val rel = Syntax.read_term lthy rel_str *) in (((vs, qty_name, mx), (rty, rel)), lthy2) end @@ -293,16 +293,16 @@ quotient_type spec' lthy' end -val quotspec_parser = +val quotspec_parser = OuterParse.and_list1 - ((OuterParse.type_args -- OuterParse.binding) -- - OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- + ((OuterParse.type_args -- OuterParse.binding) -- + OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) val _ = OuterKeyword.keyword "/" -val _ = - OuterSyntax.local_theory_to_proof "quotient_type" +val _ = + OuterSyntax.local_theory_to_proof "quotient_type" "quotient type definitions (require equivalence proofs)" OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)