# HG changeset patch # User Christian Urban # Date 1249986555 -7200 # Node ID ebe0ea8fe247f0bb5d5d9075849b6a126c14bbfa initial commit diff -r 000000000000 -r ebe0ea8fe247 QuotList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/QuotList.thy Tue Aug 11 12:29:15 2009 +0200 @@ -0,0 +1,255 @@ +theory QuotList +imports QuotScript +begin + + +lemma LIST_map_I: + shows "map (\x. x) = (\x. x)" + by simp + +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)" + +lemma LIST_REL_EQ: + 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) + +lemma LIST_EQUIV: + assumes a: "EQUIV R" + shows "EQUIV (LIST_REL R)" +unfolding EQUIV_def +apply(rule allI)+ +apply(induct_tac x y rule: list_induct2') +apply(simp) +apply(simp add: expand_fun_eq) +apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) +apply(simp add: expand_fun_eq) +apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) +apply(simp add: expand_fun_eq) +apply(rule iffI) +apply(rule allI) +apply(case_tac x) +apply(simp) +apply(simp) +using a +apply(unfold EQUIV_def) +apply(auto)[1] +apply(metis LIST_REL.simps(4)) +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: + assumes q: "QUOTIENT R Abs Rep" + shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)" +unfolding QUOTIENT_def +apply(rule conjI) +apply(rule allI) +apply(induct_tac a) +apply(simp) +apply(simp add: QUOTIENT_ABS_REP[OF q]) +apply(rule conjI) +apply(rule allI) +apply(induct_tac a) +apply(simp) +apply(simp) +apply(simp add: QUOTIENT_REP_REFL[OF q]) +apply(rule allI)+ +apply(rule LIST_REL_REL[OF q]) +done + +lemma CONS_PRS: + assumes q: "QUOTIENT R Abs Rep" + shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" +by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q]) + +lemma CONS_RSP: + assumes q: "QUOTIENT R Abs Rep" + and a: "R h1 h2" "LIST_REL R t1 t2" + shows "LIST_REL R (h1#t1) (h2#t2)" +using a by (auto) + +lemma NIL_PRS: + assumes q: "QUOTIENT R Abs Rep" + shows "[] = (map Abs [])" +by (simp) + +lemma NIL_RSP: + assumes q: "QUOTIENT R Abs Rep" + shows "LIST_REL R [] []" +by simp + +lemma MAP_PRS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))" +by (induct l) + (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]) + +lemma MAP_RSP: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and a: "(R1 ===> R2) f1 f2" + and b: "LIST_REL R1 l1 l2" + shows "LIST_REL R2 (map f1 l1) (map f2 l2)" +using b a +by (induct l1 l2 rule: list_induct2') + (simp_all) + + +end + +(* +val LENGTH_PRS = store_thm + ("LENGTH_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l. LENGTH l = LENGTH (MAP rep l)--), + +val LENGTH_RSP = store_thm + ("LENGTH_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2. + (LIST_REL R) l1 l2 ==> + (LENGTH l1 = LENGTH l2)--), +val APPEND_PRS = store_thm + ("APPEND_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))--), + +val APPEND_RSP = store_thm + ("APPEND_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2 m1 m2. + (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==> + (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)--), +val FLAT_PRS = store_thm + ("FLAT_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))--), + +val FLAT_RSP = store_thm + ("FLAT_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2. + LIST_REL (LIST_REL R) l1 l2 ==> + (LIST_REL R) (FLAT l1) (FLAT l2)--), + +val REVERSE_PRS = store_thm + ("REVERSE_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l. REVERSE l = MAP abs (REVERSE (MAP rep l))--), + +val REVERSE_RSP = store_thm + ("REVERSE_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2. + LIST_REL R l1 l2 ==> + (LIST_REL R) (REVERSE l1) (REVERSE l2)--), + +val FILTER_PRS = store_thm + ("FILTER_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l)) + --), + +val FILTER_RSP = store_thm + ("FILTER_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !P1 P2 l1 l2. + (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> + (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)--), + +val NULL_PRS = store_thm + ("NULL_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l. NULL l = NULL (MAP rep l)--), + +val NULL_RSP = store_thm + ("NULL_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2. + LIST_REL R l1 l2 ==> + (NULL l1 = NULL l2)--), + +val SOME_EL_PRS = store_thm + ("SOME_EL_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)--), + +val SOME_EL_RSP = store_thm + ("SOME_EL_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2 P1 P2. + (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> + (SOME_EL P1 l1 = SOME_EL P2 l2)--), + +val ALL_EL_PRS = store_thm + ("ALL_EL_PRS", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)--), + +val ALL_EL_RSP = store_thm + ("ALL_EL_RSP", + (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !l1 l2 P1 P2. + (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> + (ALL_EL P1 l1 = ALL_EL P2 l2)--), + +val FOLDL_PRS = store_thm + ("FOLDL_PRS", + (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> + !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> + !l f e. FOLDL f e l = + abs1 (FOLDL ((abs1 --> abs2 --> rep1) f) + (rep1 e) + (MAP rep2 l))--), + +val FOLDL_RSP = store_thm + ("FOLDL_RSP", + (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> + !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> + !l1 l2 f1 f2 e1 e2. + (R1 ===> R2 ===> R1) f1 f2 /\ + R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==> + R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)--), + +val FOLDR_PRS = store_thm + ("FOLDR_PRS", + (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> + !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> + !l f e. FOLDR f e l = + abs2 (FOLDR ((abs1 --> abs2 --> rep2) f) + (rep2 e) + (MAP rep1 l))--), + +val FOLDR_RSP = store_thm + ("FOLDR_RSP", + (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> + !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> + !l1 l2 f1 f2 e1 e2. + (R1 ===> R2 ===> R2) f1 f2 /\ + R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==> + R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)--), +*) + diff -r 000000000000 -r ebe0ea8fe247 QuotMain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/QuotMain.thy Tue Aug 11 12:29:15 2009 +0200 @@ -0,0 +1,559 @@ +theory QuotMain +imports QuotScript QuotList +begin + +locale QUOT_TYPE = + fixes R :: "'a \ 'a \ bool" + and Abs :: "('a \ bool) \ 'b" + and Rep :: "'b \ ('a \ bool)" + assumes equiv: "EQUIV 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 x \ Abs (R x)" + +definition + "REP a = Eps (Rep a)" + +lemma lem9: + shows "R (Eps (R x)) = R x" +proof - + have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) + then have "R x (Eps (R x))" by (rule someI) + then show "R (Eps (R x)) = R x" + using equiv unfolding EQUIV_def by simp +qed + +theorem 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 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 REP_refl: + shows "R (REP a) (REP a)" +unfolding REP_def +by (simp add: equiv[simplified EQUIV_def]) + +lemma lem7: + "(R x = R y) = (Abs (R x) = Abs (R y))" +apply(rule iffI) +apply(simp) +apply(drule rep_inject[THEN iffD2]) +apply(simp add: abs_inverse) +done + +theorem thm11: + shows "R r r' = (ABS r = ABS r')" +unfolding ABS_def +by (simp only: equiv[simplified EQUIV_def] lem7) + +lemma QUOTIENT: + "QUOTIENT R ABS REP" +apply(unfold QUOTIENT_def) +apply(simp add: thm10) +apply(simp add: REP_refl) +apply(subst thm11[symmetric]) +apply(simp add: equiv[simplified EQUIV_def]) +done + +end + +ML {* + Variable.variant_frees +*} + + +section {* type definition for the quotient type *} + +ML {* +(* constructs the term \(c::ty\bool). \x. c = rel x *) +fun typedef_term rel ty lthy = +let + val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] + |> Variable.variant_frees lthy [rel] + |> map Free +in + lambda c + ((HOLogic.exists_const ty) $ + (lambda x (HOLogic.mk_eq (c, (rel $ x))))) +end +*} + +ML {* +val typedef_tac = + EVERY1 [rewrite_goal_tac @{thms mem_def}, + rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}] +*} + +ML {* +(* makes the new type definitions *) +fun typedef_make (qty_name, rel, ty) lthy = + LocalTheory.theory_result + (TypedefPackage.add_typedef false NONE + (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) + (typedef_term rel ty lthy) + NONE typedef_tac) lthy +*} + +text {* proves the QUOTIENT theorem for the new type *} +ML {* +fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.info) = +let + val rep_thm = #Rep typedef_info + val rep_inv = #Rep_inverse typedef_info + val abs_inv = #Abs_inverse typedef_info + val rep_inj = #Rep_inject typedef_info + + val ss = HOL_basic_ss addsimps @{thms mem_def} + val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm + val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv +in + EVERY1 [rtac @{thm QUOT_TYPE.intro}, + rtac equiv_thm, + rtac rep_thm_simpd, + rtac rep_inv, + rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl}, + rtac rep_inj] +end +*} + +ML {* +fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = +let + val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) + val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) + |> Syntax.check_term lthy +in + Goal.prove lthy [] [] goal + (fn _ => typedef_quot_type_tac equiv_thm typedef_info) +end +*} + +ML {* +fun typedef_quotient_thm_tac defs quot_type_thm = + EVERY1 [K (rewrite_goals_tac defs), + rtac @{thm QUOT_TYPE.QUOTIENT}, + rtac quot_type_thm] +*} + +ML {* +fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = +let + val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) + val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) + |> Syntax.check_term lthy +in + Goal.prove lthy [] [] goal + (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm) +end +*} + +text {* two wrappers for define and note *} +ML {* +fun make_def (name, mx, trm) lthy = +let + val ((trm, (_ , thm)), lthy') = + LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy +in + ((trm, thm), lthy') +end +*} + +ML {* +fun reg_thm (name, thm) lthy = +let + val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy +in + (thm',lthy') +end +*} + +ML {* +fun typedef_main (qty_name, rel, ty, equiv_thm) lthy = +let + (* generates typedef *) + val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy + + (* abs and rep functions *) + val abs_ty = #abs_type typedef_info + val rep_ty = #rep_type typedef_info + val abs_name = #Abs_name typedef_info + val rep_name = #Rep_name typedef_info + val abs = Const (abs_name, rep_ty --> abs_ty) + val rep = Const (rep_name, abs_ty --> rep_ty) + + (* ABS and REP definitions *) + val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) + val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) + val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) + val REP_trm = Syntax.check_term lthy' (REP_const $ rep) + val ABS_name = Binding.prefix_name "ABS_" qty_name + val REP_name = Binding.prefix_name "REP_" qty_name + val (((ABS, ABS_def), (REP, REP_def)), lthy'') = + lthy' |> make_def (ABS_name, NoSyn, ABS_trm) + ||>> make_def (REP_name, NoSyn, REP_trm) + + (* quot_type theorem *) + val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy'' + val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name + + (* quotient theorem *) + val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy'' + val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name + +in + lthy'' + |> reg_thm (quot_thm_name, quot_thm) + ||>> reg_thm (quotient_thm_name, quotient_thm) +end +*} + +section {* various tests for quotient types*} +datatype trm = + var "nat" +| app "trm" "trm" +| lam "nat" "trm" + +consts R :: "trm \ trm \ bool" +axioms r_eq: "EQUIV R" + +local_setup {* + typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd +*} + +term Rep_qtrm +term Abs_qtrm +term ABS_qtrm +term REP_qtrm +thm QUOT_TYPE_qtrm +thm QUOTIENT_qtrm +thm Rep_qtrm + +text {* another test *} +datatype 'a my = foo +consts Rmy :: "'a my \ 'a my \ bool" +axioms rmy_eq: "EQUIV Rmy" + +term "\(c::'a my\bool). \x. c = Rmy x" + +datatype 'a trm' = + var' "'a" +| app' "'a trm'" "'a trm'" +| lam' "'a" "'a trm'" + +consts R' :: "'a trm' \ 'a trm' \ bool" +axioms r_eq': "EQUIV R'" + +local_setup {* + typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd +*} + +term ABS_qtrm' +term REP_qtrm' +thm QUOT_TYPE_qtrm' +thm QUOTIENT_qtrm' +thm Rep_qtrm' + +text {* a test with lists of terms *} +datatype t = + vr "string" +| ap "t list" +| lm "string" "t" + +consts Rt :: "t \ t \ bool" +axioms t_eq: "EQUIV Rt" + +local_setup {* + typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd +*} + +section {* lifting of constants *} + +text {* information about map-functions for type-constructor *} +ML {* +type typ_info = {mapfun: string} + +local + structure Data = GenericDataFun + (type T = typ_info Symtab.table + val empty = Symtab.empty + val extend = I + fun merge _ = Symtab.merge (K true)) +in + val lookup = Symtab.lookup o Data.get + fun update k v = Data.map (Symtab.update (k, v)) +end +*} + +(* mapfuns for some standard types *) +setup {* + Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}}) + #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}}) + #> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}}) +*} + +ML {* lookup (Context.Proof @{context}) @{type_name list} *} + +ML {* +datatype abs_or_rep = abs | rep + +fun get_fun abs_or_rep rty qty lthy ty = +let + val qty_name = Long_Name.base_name (fst (dest_Type qty)) + + fun get_fun_aux s fs_tys = + let + val (fs, tys) = split_list fs_tys + val (otys, ntys) = split_list tys + val oty = Type (s, otys) + val nty = Type (s, ntys) + val ftys = map (op -->) tys + in + (case (lookup (Context.Proof lthy) s) of + SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) + | NONE => raise ERROR ("no map association for type " ^ s)) + end + + fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) + | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) +in + if ty = qty + then (get_const abs_or_rep) + else (case ty of + TFree _ => (Abs ("x", ty, Bound 0), (ty, ty)) + | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty)) + | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys) + | _ => raise ERROR ("no variables") + ) +end +*} + +ML {* +fun get_const_def nconst oconst rty qty lthy = +let + val ty = fastype_of nconst + val (arg_tys, res_ty) = strip_type ty + + val fresh_args = arg_tys |> map (pair "x") + |> Variable.variant_frees lthy [nconst, oconst] + |> map Free + + val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys + val abs_fn = (fst o get_fun abs rty qty lthy) res_ty + +in + map (op $) (rep_fns ~~ fresh_args) + |> curry list_comb oconst + |> curry (op $) abs_fn + |> fold_rev lambda fresh_args +end +*} + +ML {* +fun exchange_ty rty qty ty = + if ty = rty then qty + else + (case ty of + Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) + | _ => ty) +*} + +ML {* +fun make_const_def nconst_name oconst mx rty qty lthy = +let + val oconst_ty = fastype_of oconst + val nconst_ty = exchange_ty rty qty oconst_ty + val nconst = Const (nconst_name, nconst_ty) + val def_trm = get_const_def nconst oconst rty qty lthy +in + make_def (Binding.name nconst_name, mx, def_trm) lthy +end +*} + +text {* a test with functions *} +datatype 'a t' = + vr' "string" +| ap' "('a t') * ('a t')" +| lm' "'a" "string \ ('a t')" + +consts Rt' :: "('a t') \ ('a t') \ bool" +axioms t_eq': "EQUIV Rt'" + +local_setup {* + typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd +*} + +local_setup {* + make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd +*} + +local_setup {* + make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd +*} + +local_setup {* + make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd +*} + +thm VR'_def +thm AP'_def +thm LM'_def +term LM' +term VR' +term AP' + +text {* finite set example *} + +inductive + list_eq ("_ \ _") +where + "a#b#xs \ b#a#xs" +| "[] \ []" +| "xs \ ys \ ys \ xs" +| "a#a#xs \ a#xs" +| "xs \ ys \ a#xs \ a#ys" +| "\xs1 \ xs2; xs2 \ xs3\ \ xs1 \ xs3" + +lemma list_eq_sym: + shows "xs \ xs" +apply(induct xs) +apply(auto intro: list_eq.intros) +done + +lemma equiv_list_eq: + shows "EQUIV list_eq" +unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def +apply(auto intro: list_eq.intros list_eq_sym) +done + +local_setup {* + typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd +*} + +typ "'a fset" +thm "Rep_fset" + +local_setup {* + make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term Nil +term EMPTY + +local_setup {* + make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term Cons +term INSERT + +local_setup {* + make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term append +term UNION +thm QUOTIENT_fset +thm Insert_def + +fun + membship :: "'a \ 'a list \ bool" ("_ memb _") +where + m1: "(x memb []) = False" +| m2: "(x memb (y#xs)) = ((x=y) \ (x memb xs))" + + +local_setup {* + make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term membship +term IN + +lemma + shows "IN x EMPTY = False" +unfolding IN_def EMPTY_def +apply(auto) +thm Rep_fset_inverse + + + + + + + + + + +text {* old stuff *} + + +lemma QUOT_TYPE_qtrm_old: + "QUOT_TYPE R Abs_qtrm Rep_qtrm" +apply(rule QUOT_TYPE.intro) +apply(rule r_eq) +apply(rule Rep_qtrm[simplified mem_def]) +apply(rule Rep_qtrm_inverse) +apply(rule Abs_qtrm_inverse[simplified mem_def]) +apply(rule exI) +apply(rule refl) +apply(rule Rep_qtrm_inject) +done + +definition + "ABS_qtrm_old \ QUOT_TYPE.ABS R Abs_qtrm" + +definition + "REP_qtrm_old \ QUOT_TYPE.REP Rep_qtrm" + +lemma + "QUOTIENT R (ABS_qtrm) (REP_qtrm)" +apply(simp add: ABS_qtrm_def REP_qtrm_def) +apply(rule QUOT_TYPE.QUOTIENT) +apply(rule QUOT_TYPE_qtrm) +done + +term "var" +term "app" +term "lam" + +definition + "VAR x \ ABS_qtrm (var x)" + +definition + "APP t1 t2 \ ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))" + +definition + "LAM x t \ ABS_qtrm (lam x (REP_qtrm t))" + + + + +definition + "VR x \ ABS_qt (vr x)" + +definition + "AP ts \ ABS_qt (ap (map REP_qt ts))" + +definition + "LM x t \ ABS_qt (lm x (REP_qt t))" + +(* for printing types *) +ML {* +fun setmp_show_all_types f = + setmp show_all_types + (! show_types orelse ! show_sorts orelse ! show_all_types) f +*} \ No newline at end of file diff -r 000000000000 -r ebe0ea8fe247 QuotScript.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/QuotScript.thy Tue Aug 11 12:29:15 2009 +0200 @@ -0,0 +1,401 @@ +theory QuotScript +imports Main +begin + +definition + "EQUIV E \ \x y. E x y = (E x = E y)" + +definition + "REFL E \ \x. E x x" + +definition + "SYM E \ \x y. E x y \ E y x" + +definition + "TRANS E \ \x y z. E x y \ E y z \ E x z" + +lemma EQUIV_REFL_SYM_TRANS: + shows "EQUIV E = (REFL E \ SYM E \ TRANS E)" +unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq +by (blast) + +definition + "PART_EQUIV E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" + +lemma EQUIV_IMP_PART_EQUIV: + assumes a: "EQUIV E" + shows "PART_EQUIV E" +using a unfolding EQUIV_def PART_EQUIV_def +by auto + +definition + "QUOTIENT E Abs Rep \ (\a. Abs (Rep a) = a) \ + (\a. E (Rep a) (Rep a)) \ + (\r s. E r s = (E r r \ E s s \ (Abs r = Abs s)))" + +lemma QUOTIENT_ABS_REP: + assumes a: "QUOTIENT E Abs Rep" + shows "Abs (Rep a) = a" +using a unfolding QUOTIENT_def +by simp + +lemma QUOTIENT_REP_REFL: + 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_ABS: + assumes a: "QUOTIENT E Abs Rep" + shows "E r s \ Abs r = Abs s" +using a unfolding QUOTIENT_def +by blast + +lemma QUOTIENT_REL_ABS_EQ: + assumes a: "QUOTIENT E Abs Rep" + shows "E r r \ E s s \ E r s = (Abs r = Abs s)" +using a unfolding QUOTIENT_def +by blast + +lemma QUOTIENT_REL_REP: + assumes a: "QUOTIENT E Abs Rep" + shows "E (Rep a) (Rep b) = (a = b)" +using a unfolding QUOTIENT_def +by metis + +lemma QUOTIENT_REP_ABS: + assumes a: "QUOTIENT E Abs Rep" + shows "E r r \ E (Rep (Abs r)) r" +using a unfolding QUOTIENT_def +by blast + +lemma IDENTITY_EQUIV: + shows "EQUIV (op =)" +unfolding EQUIV_def +by auto + +lemma IDENTITY_QUOTIENT: + shows "QUOTIENT (op =) (\x. x) (\x. x)" +unfolding QUOTIENT_def +by blast + +lemma QUOTIENT_SYM: + assumes a: "QUOTIENT E Abs Rep" + shows "SYM E" +using a unfolding QUOTIENT_def SYM_def +by metis + +lemma QUOTIENT_TRANS: + assumes a: "QUOTIENT E Abs Rep" + shows "TRANS E" +using a unfolding QUOTIENT_def TRANS_def +by metis + +fun + fun_map +where + "fun_map f g h x = g (h (f x))" + +abbreviation + fun_map_syn ("_ ---> _") +where + "f ---> g \ fun_map f g" + +lemma FUN_MAP_I: + shows "(\x. x ---> \x. x) = (\x. x)" +by (simp add: expand_fun_eq) + +lemma IN_FUN: + shows "x \ ((f ---> g) s) = g (f x \ s)" +by (simp add: mem_def) + +fun + FUN_REL +where + "FUN_REL E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" + +abbreviation + FUN_REL_syn ("_ ===> _") +where + "E1 ===> E2 \ FUN_REL E1 E2" + +lemma FUN_REL_EQ: + "(op =) ===> (op =) = (op =)" +by (simp add: expand_fun_eq) + +lemma FUN_QUOTIENT: + assumes q1: "QUOTIENT R1 abs1 rep1" + and q2: "QUOTIENT R2 abs2 rep2" + shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" +proof - + have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + apply(simp add: expand_fun_eq) + using q1 q2 + apply(simp add: QUOTIENT_def) + done + moreover + have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + apply(auto) + using q1 q2 unfolding QUOTIENT_def + apply(metis) + done + moreover + have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s)" + apply(auto simp add: expand_fun_eq) + using q1 q2 unfolding QUOTIENT_def + apply(metis) + using q1 q2 unfolding QUOTIENT_def + apply(metis) + using q1 q2 unfolding QUOTIENT_def + apply(metis) + using q1 q2 unfolding QUOTIENT_def + apply(metis) + done + ultimately + show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" + unfolding QUOTIENT_def by blast +qed + +definition + Respects +where + "Respects R x \ (R x x)" + +lemma IN_RESPECTS: + shows "(x \ Respects R) = R x x" +unfolding mem_def Respects_def by simp + +lemma RESPECTS_THM: + shows "Respects (R1 ===> R2) f = (\x y. R1 x y \ R2 (f x) (f y))" +unfolding Respects_def +by (simp add: expand_fun_eq) + +lemma RESPECTS_MP: + assumes a: "Respects (R1 ===> R2) f" + and b: "R1 x y" + shows "R2 (f x) (f y)" +using a b unfolding Respects_def +by simp + +lemma RESPECTS_REP_ABS: + assumes a: "QUOTIENT R1 Abs1 Rep1" + and b: "Respects (R1 ===> R2) f" + and c: "R1 x x" + shows "R2 (f (Rep1 (Abs1 x))) (f x)" +using a b[simplified RESPECTS_THM] c unfolding QUOTIENT_def +by blast + +lemma RESPECTS_o: + assumes a: "Respects (R2 ===> R3) f" + and b: "Respects (R1 ===> R2) g" + shows "Respects (R1 ===> R3) (f o g)" +using a b unfolding Respects_def +by simp + +(* +definition + "RES_EXISTS_EQUIV R P \ (\x \ Respects R. P x) \ + (\x\ Respects R. \y\ Respects R. P x \ P y \ R x y)" +*) + +lemma FUN_REL_EQ_REL: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \ (Respects (R1 ===> R2) g) + \ ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" +using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq +by blast + +(* q1 and q2 not used; see next lemma *) +lemma FUN_REL_MP: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "(R1 ===> R2) f g \ R1 x y \ R2 (f x) (g y)" +by simp + +lemma FUN_REL_IMP: + shows "(R1 ===> R2) f g \ R1 x y \ R2 (f x) (g y)" +by simp + +lemma FUN_REL_EQUALS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and r1: "Respects (R1 ===> R2) f" + and r2: "Respects (R1 ===> R2) g" + shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\x y. R1 x y \ R2 (f x) (g y))" +apply(rule_tac iffI) +using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def +apply(metis FUN_REL_IMP) +using r1 unfolding Respects_def expand_fun_eq +apply(simp (no_asm_use)) +apply(metis QUOTIENT_REL[OF q2] QUOTIENT_REL_REP[OF q1]) +done + +(* ask Peter: FUN_REL_IMP used twice *) +lemma FUN_REL_IMP2: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and r1: "Respects (R1 ===> R2) f" + and r2: "Respects (R1 ===> R2) g" + and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" + shows "R1 x y \ R2 (f x) (g y)" +using q1 q2 r1 r2 a +by (simp add: FUN_REL_EQUALS) + +lemma EQUALS_PRS: + assumes q: "QUOTIENT R Abs Rep" + shows "(x = y) = R (Rep x) (Rep y)" +by (simp add: QUOTIENT_REL_REP[OF q]) + +lemma EQUALS_RSP: + assumes q: "QUOTIENT R Abs Rep" + and a: "R x1 x2" "R y1 y2" + shows "R x1 y1 = R x2 y2" +using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def +using a by blast + +lemma LAMBDA_PRS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "(\x. f x) = (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 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 "(\x. f x) = (Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x)" +unfolding expand_fun_eq +by (subst LAMBDA_PRS[OF q1 q2]) (simp) + +(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) +lemma LAMBDA_RSP: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and a: "(R1 ===> R2) f1 f2" + shows "(R1 ===> R2) (\x. f1 x) (\y. f2 y)" +by (rule a) + +(* ASK Peter about next four lemmas in quotientScript +lemma ABSTRACT_PRS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "f = (Rep1 ---> Abs2) ???" +*) + +lemma LAMBDA_REP_ABS_RSP: + assumes r1: "\r r'. R1 r r' \R1 r (Rep1 (Abs1 r'))" + and r2: "\r r'. R2 r r' \R2 r (Rep2 (Abs2 r'))" + shows "(R1 ===> R2) f1 f2 \ (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" +using r1 r2 by auto + +lemma REP_ABS_RSP: + assumes q: "QUOTIENT R Abs Rep" + and a: "R x1 x2" + shows "R x1 (Rep (Abs x2))" +using a +by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) + +(* ----------------------------------------------------- *) +(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) +(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) +(* ----------------------------------------------------- *) + +(* what is RES_FORALL *) +(*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> + !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*) +(*as peter here *) + +(* bool theory: COND, LET *) + +lemma IF_PRS: + assumes q: "QUOTIENT R Abs Rep" + shows "If a b c = Abs (If a (Rep b) (Rep c))" +using QUOTIENT_ABS_REP[OF q] by auto + +(* ask peter: no use of q *) +lemma IF_RSP: + assumes q: "QUOTIENT R Abs Rep" + and a: "a1 = a2" "R b1 b2" "R c1 c2" + shows "R (If a1 b1 c1) (If a2 b2 c2)" +using a by auto + +lemma LET_PRS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))" +using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto + +lemma LET_RSP: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and a1: "(R1 ===> R2) f g" + and a2: "R1 x y" + shows "R2 (Let x f) (Let y g)" +using FUN_REL_MP[OF q1 q2 a1] a2 +by auto + + +(* ask peter what are literal_case *) +(* literal_case_PRS *) +(* literal_case_RSP *) + + +(* FUNCTION APPLICATION *) + +lemma APPLY_PRS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" +using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto + +(* ask peter: no use of q1 q2 *) +lemma APPLY_RSP: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" +using a by (rule FUN_REL_IMP) + + +(* combinators: I, K, o, C, W *) + +lemma I_PRS: + assumes q: "QUOTIENT R Abs Rep" + shows "(\x. x) e = Abs ((\ x. x) (Rep e))" +using QUOTIENT_ABS_REP[OF q] by auto + +lemma I_RSP: + assumes q: "QUOTIENT R Abs Rep" + and a: "R e1 e2" + shows "R ((\x. x) e1) ((\ x. x) e2)" +using a by auto + +lemma o_PRS: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and q3: "QUOTIENT R3 Abs3 Rep3" + shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))" +using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3] +unfolding o_def expand_fun_eq +by simp + +lemma o_RSP: + assumes q1: "QUOTIENT R1 Abs1 Rep1" + and q2: "QUOTIENT R2 Abs2 Rep2" + and q3: "QUOTIENT R3 Abs3 Rep3" + and a1: "(R2 ===> R3) f1 f2" + and a2: "(R1 ===> R2) g1 g2" + shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" +using a1 a2 unfolding o_def expand_fun_eq +by (auto) + +end \ No newline at end of file diff -r 000000000000 -r ebe0ea8fe247 Quotients.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quotients.thy Tue Aug 11 12:29:15 2009 +0200 @@ -0,0 +1,412 @@ +theory Quotients +imports Main +begin + +definition + "REFL E \ \x. E x x" + +definition + "SYM E \ \x y. E x y \ E y x" + +definition + "TRANS E \ \x y z. E x y \ E y z \ E x z" + +definition + "NONEMPTY E \ \x. E x x" + +definition + "EQUIV E \ REFL E \ SYM E \ TRANS E" + +definition + "EQUIV_PROP E \ (\x y. E x y = (E x = E y))" + +lemma EQUIV_PROP_EQUALITY: + shows "EQUIV_PROP (op =)" +unfolding EQUIV_PROP_def expand_fun_eq +by (blast) + +lemma EQUIV_implies_EQUIV_PROP: + assumes a: "REFL E" + and b: "SYM E" + and c: "TRANS E" + shows "EQUIV_PROP E" +using a b c +unfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eq +by (metis) + +lemma EQUIV_PROP_implies_REFL: + assumes a: "EQUIV_PROP E" + shows "REFL E" +using a +unfolding EQUIV_PROP_def REFL_def expand_fun_eq +by (metis) + +lemma EQUIV_PROP_implies_SYM: + assumes a: "EQUIV_PROP E" + shows "SYM E" +using a +unfolding EQUIV_PROP_def SYM_def expand_fun_eq +by (metis) + +lemma EQUIV_PROP_implies_TRANS: + assumes a: "EQUIV_PROP E" + shows "TRANS E" +using a +unfolding EQUIV_PROP_def TRANS_def expand_fun_eq +by (blast) + +ML {* +fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL} +fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM} +fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS} + +fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP} +*} + + +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)" + +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" + +fun + option_map +where + "option_map f None = None" +| "option_map f (Some x) = Some (f x)" + +fun + PROD_REL +where + "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \ R2 a2 b2)" + +fun + prod_map +where + "prod_map f1 f2 (a,b) = (f1 a, f2 b)" + +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)" + +fun + FUN_REL +where + "FUN_REL R1 R2 f g = (\x y. R1 x y \ R2 (f x) (g y))" + +fun + fun_map +where + "fun_map f g h x = g (h (f x))" + +definition + "QUOTIENT_ABS_REP Abs Rep \ (\a. Abs (Rep a) = a)" + + + +definition + "QUOTIENT R Abs Rep \ (\a. Abs (Rep a) = a) \ + (\a. R (Rep a) (Rep a)) \ + (\r s. R r s = (R r r \ R s s \ (Abs r = Abs s)))" + +lemma QUOTIENT_ID: + shows "QUOTIENT (op =) id id" +unfolding QUOTIENT_def id_def +by (blast) + +lemma QUOTIENT_PROD: + assumes a: "QUOTIENT E1 Abs1 Rep1" + and b: "QUOTIENT E2 Abs2 Rep2" + shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)" +using a b unfolding QUOTIENT_def +oops + +lemma QUOTIENT_ABS_REP_LIST: + assumes a: "QUOTIENT_ABS_REP Abs Rep" + shows "QUOTIENT_ABS_REP (map Abs) (map Rep)" +using a +unfolding QUOTIENT_ABS_REP_def +apply(rule_tac allI) +apply(induct_tac a rule: list.induct) +apply(auto) +done + +definition + eqclass ("[_]_") +where + "[x]E \ E x" + +definition + QUOTIENT_SET :: "'a set \ ('a \'a\bool) \ ('a set) set" ("_'/#'/_") +where + "S/#/E = {[x]E | x. x\S}" + +definition + QUOTIENT_UNIV +where + "QUOTIENT_UNIV TYPE('a) E \ (UNIV::'a set)/#/E" + +consts MY::"'a\'a\bool" +axioms my1: "REFL MY" +axioms my2: "SYM MY" +axioms my3: "TRANS MY" + +term "QUOTIENT_UNIV TYPE('a) MY" +term "\f. \x. f = [x]MY" + +typedef 'a quot = "\f::'a\bool. \x. f = [x]MY" +by (auto simp add: mem_def) + +thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot +thm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_induct + +lemma lem2: + shows "([x]MY = [y]MY) = MY x y" +apply(rule iffI) +apply(simp add: eqclass_def) +using my1 +apply(auto simp add: REFL_def)[1] +apply(simp add: eqclass_def expand_fun_eq) +apply(rule allI) +apply(rule iffI) +apply(subgoal_tac "MY y x") +using my3 +apply(simp add: TRANS_def)[1] +apply(drule_tac x="y" in spec) +apply(drule_tac x="x" in spec) +apply(drule_tac x="xa" in spec) +apply(simp) +using my2 +apply(simp add: SYM_def)[1] +oops + +lemma lem6: + "\a. \r. Rep_quot a = [r]MY" +apply(rule allI) +apply(subgoal_tac "Rep_quot a \ quot") +apply(simp add: quot_def mem_def) +apply(rule Rep_quot) +done + +lemma lem7: + "\x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)" +apply(subst Abs_quot_inject) +apply(unfold quot_def mem_def) +apply(auto) +done + +definition + "Abs x = Abs_quot ([x]MY)" + +definition + "Rep a = Eps (Rep_quot a)" + +lemma lem9: + "\r. [(Eps [r]MY)]MY = [r]MY" +apply(rule allI) +apply(subgoal_tac "MY r r \ MY r (Eps (MY r))") +apply(drule meta_mp) +apply(rule eq1[THEN spec]) + + +apply(rule_tac x="MY r" in someI) + +lemma + "(f \ UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)" +apply(simp add: QUOTIENT_SET_def) +apply(auto) +apply(subgoal_tac "[x]MY \ quot") +apply(simp add: Abs_quot_inverse) +apply(simp add: quot_def) +apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) +apply(auto)[1] +apply(subgoal_tac "[x]MY \ quot") +apply(simp add: Abs_quot_inverse) +apply(simp add: quot_def) +apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) +apply(auto)[1] +apply(subst expand_set_eq) +thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot + +lemma + "\a. \r. Rep_quot a = [r]MY" +apply(rule allI) +apply(subst Abs_quot_inject[symmetric]) +apply(rule Rep_quot) +apply(simp add: quot_def) +apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) +apply(auto)[1] +apply(simp add: Rep_quot_inverse) +thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot +apply(subst Abs_quot_inject[symmetric]) +proof - + have "[r]MY \ quot" + apply(simp add: quot_def) + apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) + apply(auto) + +thm Abs_quot_inverse + + +thm Abs_quot_inverse +apply(simp add: Rep_quot_inverse) + + +thm Rep_quot_inverse + +term "" + +lemma + assumes a: "EQUIV2 E" + shows "([x]E = [y]E) = E x y" +using a +by (simp add: eqclass_def EQUIV2_def) + + + + + +lemma + shows "QUOTIENT (op =) (\x. x) (\x. x)" +apply(unfold QUOTIENT_def) +apply(blast) +done + +definition + fun_app ("_ ---> _") +where + "f ---> g \ \h x. g (h (f x))" + +lemma helper: + assumes q: "QUOTIENT R ab re" + and a: "R z z" + shows "R (re (ab z)) z" +using q a +apply(unfold QUOTIENT_def)[1] +apply(blast) +done + + +lemma + assumes q1: "QUOTIENT R1 abs1 rep1" + and q2: "QUOTIENT R2 abs2 rep2" + shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" +proof - + have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + apply(simp add: expand_fun_eq) + apply(simp add: fun_app_def) + using q1 q2 + apply(simp add: QUOTIENT_def) + done + moreover + have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + apply(simp add: FUN_REL_def) + apply(auto) + apply(simp add: fun_app_def) + using q1 q2 + apply(unfold QUOTIENT_def) + apply(metis) + done + moreover + have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s)" + apply(simp add: expand_fun_eq) + apply(rule allI)+ + apply(rule iffI) + using q1 q2 + apply(unfold QUOTIENT_def)[1] + apply(unfold fun_app_def)[1] + apply(unfold FUN_REL_def)[1] + apply(rule conjI) + apply(metis) + apply(rule conjI) + apply(metis) + apply(metis) + apply(erule conjE) + apply(simp (no_asm) add: FUN_REL_def) + apply(rule allI impI)+ + apply(subgoal_tac "R1 x x \ R1 y y \ abs1 x = abs1 y")(*A*) + using q2 + apply(unfold QUOTIENT_def)[1] + apply(unfold fun_app_def)[1] + apply(unfold FUN_REL_def)[1] + apply(subgoal_tac "R2 (r x) (r x)")(*B*) + apply(subgoal_tac "R2 (s y) (s y)")(*C*) + apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*) + apply(blast) + (*D*) + apply(metis helper q1) + (*C*) + apply(blast) + (*B*) + apply(blast) + (*A*) + using q1 + apply(unfold QUOTIENT_def)[1] + apply(unfold fun_app_def)[1] + apply(unfold FUN_REL_def)[1] + apply(metis) + done + ultimately + show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" + apply(unfold QUOTIENT_def)[1] + apply(blast) + done +qed + + + + + + + +definition + "USER R \ NONEMPTY R \ + + + +typedecl tau +consts R::"tau \ tau \ bool" + + + +definition + FACTOR :: "'a set \ ('a \'a \ bool) \ ('a set) set" ("_ '/'/'/ _") +where + "A /// r \ \x\A. {r``{x}}" + +typedef qtau = "\c::tau\bool. (\x. R x x \ (c = R x))" +apply(rule exI) + +apply(rule_tac x="R x" in exI) +apply(auto) + +definition + "QUOT TYPE('a) R \ \c::'a\bool. (\x. R x x \ (c = R x))" + + + + + +