# HG changeset patch # User Christian Urban # Date 1261560714 -3600 # Node ID 3b21b24a5fb617bb5e474f968361161d6cc533ed # Parent 54f186bb5e3e50d43528c15e36cf884c8a3f41bb corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/Examples/AbsRepTest.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Examples/AbsRepTest.thy Wed Dec 23 10:31:54 2009 +0100 @@ -0,0 +1,78 @@ +theory AbsRepTest +imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List +begin + + +(* +quotient_type + fset = "'a list" / "\(xs::'a list) ys. \e. e \ set xs \ e \ set ys" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(auto) + sorry + done +*) + +inductive + list_eq (infix "\" 50) +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" + +quotient_type + fset = "'a list" / "list_eq" + sorry + + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient_type int = "nat \ nat" / intrel + sorry + + +ML {* +open Quotient_Term; +*} + +ML {* +absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"}) +|> Syntax.string_of_term @{context} +|> writeln +*} + +term "option_map (prod_fun (abs_fset \ map abs_int) id)" +term "option_map (prod_fun (map rep_int \ rep_fset) id)" +term "option_map (map rep_int \ rep_fset)" +term "option_map (abs_fset o (map abs_int))" +term "abs_fset" + +ML {* +absrep_fun_chk absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"}) +|> Syntax.string_of_term @{context} +|> writeln +*} + +term "map abs_int" +term "abs_fset o map abs_int" + + +ML {* +absrep_fun_chk absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) +|> Syntax.string_of_term @{context} +|> writeln +*} + +ML {* +absrep_fun_chk absF @{context} (@{typ "('a list) list \ 'a"}, @{typ "('a fset) fset \ 'a"}) +|> Syntax.string_of_term @{context} +|> writeln +*} + +end \ No newline at end of file diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 22 22:10:48 2009 +0100 +++ b/Quot/Examples/FSet.thy Wed Dec 23 10:31:54 2009 +0100 @@ -26,61 +26,6 @@ fset = "'a list" / "list_eq" by (rule equivp_list_eq) - -fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" -where - "intrel (x, y) (u, v) = (x + v = u + y)" - -quotient_type int = "nat \ nat" / intrel - apply(unfold equivp_def) - apply(auto simp add: mem_def expand_fun_eq) - done - - -ML {* -open Quotient_Term; -*} - -ML {* -absrep_fun absF @{context} (@{typ "'a list"}, - @{typ "'a fset"}) -|> Syntax.check_term @{context} -|> Syntax.string_of_term @{context} -|> writeln -*} - -term "map id" -term "abs_fset o (map id)" - -ML {* -absrep_fun absF @{context} (@{typ "(nat * nat) list"}, - @{typ "int fset"}) -|> Syntax.check_term @{context} -|> Syntax.string_of_term @{context} -|> writeln -*} - -term "map abs_int" -term "abs_fset o map abs_int" - - -ML {* -absrep_fun absF @{context} (@{typ "('a list) list"}, - @{typ "('a fset) fset"}) -|> Syntax.check_term @{context} -|> Syntax.string_of_term @{context} -|> writeln -*} - -ML {* -absrep_fun absF @{context} (@{typ "('a list) list \ 'a"}, - @{typ "('a fset) fset \ 'a"}) -|> Syntax.check_term @{context} -|> Syntax.string_of_term @{context} -|> writeln -*} - quotient_definition "EMPTY :: 'a fset" as diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/QuotOption.thy --- a/Quot/QuotOption.thy Tue Dec 22 22:10:48 2009 +0100 +++ b/Quot/QuotOption.thy Wed Dec 23 10:31:54 2009 +0100 @@ -16,7 +16,8 @@ "option_map f None = None" | "option_map f (Some x) = Some (f x)" -declare [[map * = (option_map, option_rel)]] +declare [[map option = (option_map, option_rel)]] + lemma option_quotient[quot_thm]: assumes q: "Quotient R Abs Rep" diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/QuotSum.thy --- a/Quot/QuotSum.thy Tue Dec 22 22:10:48 2009 +0100 +++ b/Quot/QuotSum.thy Wed Dec 23 10:31:54 2009 +0100 @@ -16,7 +16,8 @@ "sum_map f1 f2 (Inl a) = Inl (f1 a)" | "sum_map f1 f2 (Inr a) = Inr (f2 a)" -declare [[map * = (sum_map, sum_rel)]] +declare [[map "+" = (sum_map, sum_rel)]] + lemma sum_equivp[quot_equiv]: assumes a: "equivp R1" diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/ROOT.ML --- a/Quot/ROOT.ML Tue Dec 22 22:10:48 2009 +0100 +++ b/Quot/ROOT.ML Wed Dec 23 10:31:54 2009 +0100 @@ -2,6 +2,7 @@ no_document use_thys ["QuotMain", + "Examples/AbsRepTest", "Examples/FSet", "Examples/FSet2", "Examples/FSet3", diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Tue Dec 22 22:10:48 2009 +0100 +++ b/Quot/quotient_term.ML Wed Dec 23 10:31:54 2009 +0100 @@ -21,10 +21,13 @@ exception LIFT_MATCH of string -(* Calculates the aggregate abs and rep functions for a given type; *) -(* repF is for constants' arguments; absF is for constants; *) -(* function types need to be treated specially, since repF and absF *) -(* change *) +(*******************************) +(* Aggregate Rep/Abs Functions *) +(*******************************) + +(* The flag repF is for types in negative position, while 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 @@ -38,19 +41,19 @@ absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 -fun absrep_fun_aux lthy s fs = +fun get_map ctxt ty_str = let - val thy = ProofContext.theory_of lthy - val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."]) - val info = maps_lookup thy s handle NotFound => raise exc + val thy = ProofContext.theory_of ctxt + val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."]) + val info = maps_lookup thy ty_str handle NotFound => raise exc in - list_comb (Const (#mapfun info, dummyT), fs) + Const (#mapfun info, dummyT) end -fun get_const flag lthy _ qty = +fun get_absrep_const flag ctxt _ qty = (* FIXME: check here that the type-constructors of _ and qty are related *) let - val thy = ProofContext.theory_of lthy + val thy = ProofContext.theory_of ctxt val qty_name = Long_Name.base_name (fst (dest_Type qty)) in case flag of @@ -58,41 +61,42 @@ | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) end -fun absrep_fun flag lthy (rty, qty) = +fun absrep_fun flag ctxt (rty, qty) = if rty = qty then mk_identity qty else case (rty, qty) of (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => - let - val fs_ty1 = absrep_fun (negF flag) lthy (ty1, ty1') - val fs_ty2 = absrep_fun flag lthy (ty2, ty2') - in - absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2] - end + let + val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') + val arg2 = absrep_fun flag ctxt (ty2, ty2') + in + list_comb (get_map ctxt "fun", [arg1, arg2]) + end | (Type (s, _), Type (s', [])) => - if s = s' - then mk_identity qty - else get_const flag lthy rty qty + if s = s' + then mk_identity qty + else get_absrep_const flag ctxt rty qty | (Type (s, tys), Type (s', tys')) => - let - val args = map (absrep_fun flag lthy) (tys ~~ tys') - in + let + val args = map (absrep_fun flag ctxt) (tys ~~ tys') + val result = list_comb (get_map ctxt s, args) + in if s = s' - then absrep_fun_aux lthy s args - else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args) - end + then result + else mk_compose flag (get_absrep_const flag ctxt rty qty, result) + end | (TFree x, TFree x') => - if x = x' - then mk_identity qty - else raise (LIFT_MATCH "absrep_fun (frees)") + if x = x' + then mk_identity qty + else raise (LIFT_MATCH "absrep_fun (frees)") | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") | _ => raise (LIFT_MATCH "absrep_fun (default)") -fun absrep_fun_chk flag lthy (rty, qty) = - absrep_fun flag lthy (rty, qty) - |> Syntax.check_term lthy +fun absrep_fun_chk flag ctxt (rty, qty) = + absrep_fun flag ctxt (rty, qty) + |> Syntax.check_term ctxt -(* -Regularizing an rtrm means: + +(* Regularizing an rtrm means: - Quantifiers over types that need lifting are replaced by bounded quantifiers, for example: @@ -120,9 +124,9 @@ (* builds the aggregate equivalence relation *) (* that will be the argument of Respects *) -fun mk_resp_arg lthy (rty, qty) = +fun mk_resp_arg ctxt (rty, qty) = let - val thy = ProofContext.theory_of lthy + val thy = ProofContext.theory_of ctxt in if rty = qty then HOLogic.eq_const rty @@ -134,7 +138,7 @@ let val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) val map_info = maps_lookup thy s handle NotFound => raise exc - val args = map (mk_resp_arg lthy) (tys ~~ tys') + val args = map (mk_resp_arg ctxt) (tys ~~ tys') in list_comb (Const (#relfun map_info, dummyT), args) end @@ -180,43 +184,43 @@ (* - for regularisation we do not need any *) (* special treatment of bound variables *) -fun regularize_trm lthy (rtrm, qtrm) = +fun regularize_trm ctxt (rtrm, qtrm) = case (rtrm, qtrm) of (Abs (x, ty, t), Abs (_, ty', t')) => let - val subtrm = Abs(x, ty, regularize_trm lthy (t, t')) + val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) in if ty = ty' then subtrm - else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm + else mk_babs $ (mk_resp $ mk_resp_arg ctxt (ty, ty')) $ subtrm end | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => let - val subtrm = apply_subt (regularize_trm lthy) (t, t') + val subtrm = apply_subt (regularize_trm ctxt) (t, t') in if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm - else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + else mk_ball $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => let - val subtrm = apply_subt (regularize_trm lthy) (t, t') + val subtrm = apply_subt (regularize_trm ctxt) (t, t') in if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm - else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + else mk_bex $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end | (* 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 mk_resp_arg lthy (domain_type ty, domain_type ty') + else mk_resp_arg ctxt (domain_type ty, domain_type ty') | (* in this case we just check whether the given equivalence relation is correct *) (rel, Const (@{const_name "op ="}, ty')) => let val exc = LIFT_MATCH "regularise (relation mismatch)" val rel_ty = (fastype_of rel) handle TERM _ => raise exc - val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') + val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') in if rel' aconv rel then rtrm else raise exc end @@ -241,8 +245,8 @@ if same_name rtrm qtrm then rtrm else let - val thy = ProofContext.theory_of lthy - val qtrm_str = Syntax.string_of_term lthy qtrm + val thy = ProofContext.theory_of ctxt + val qtrm_str = Syntax.string_of_term ctxt qtrm val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 @@ -253,7 +257,7 @@ end | (t1 $ t2, t1' $ t2') => - (regularize_trm lthy (t1, t1')) $ (regularize_trm lthy (t2, t2')) + (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2')) | (Bound i, Bound i') => if i = i' then rtrm @@ -261,15 +265,15 @@ | _ => let - val rtrm_str = Syntax.string_of_term lthy rtrm - val qtrm_str = Syntax.string_of_term lthy qtrm + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm in raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) end -fun regularize_trm_chk lthy (rtrm, qtrm) = - regularize_trm lthy (rtrm, qtrm) - |> Syntax.check_term lthy +fun regularize_trm_chk ctxt (rtrm, qtrm) = + regularize_trm ctxt (rtrm, qtrm) + |> Syntax.check_term ctxt (* Injection of Rep/Abs means: @@ -299,27 +303,27 @@ Vars case cannot occur. *) -fun mk_repabs lthy (T, T') trm = - absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (T, T') $ trm) +fun mk_repabs ctxt (T, T') trm = + absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm) (* bound variables need to be treated properly, *) (* as the type of subterms needs to be calculated *) -fun inj_repabs_trm lthy (rtrm, qtrm) = +fun inj_repabs_trm ctxt (rtrm, qtrm) = case (rtrm, qtrm) of (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => - Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => let val rty = fastype_of rtrm val qty = fastype_of qtrm in - mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))) + mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) end | (Abs (x, T, t), Abs (x', T', t')) => @@ -329,18 +333,18 @@ val (y, s) = Term.dest_abs (x, T, t) val (_, s') = Term.dest_abs (x', T', t') val yvar = Free (y, T) - val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) + val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s')) in if rty = qty then result - else mk_repabs lthy (rty, qty) result + else mk_repabs ctxt (rty, qty) result end | (t $ s, t' $ s') => - (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) + (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) | (Free (_, T), Free (_, T')) => if T = T' then rtrm - else mk_repabs lthy (T, T') rtrm + else mk_repabs ctxt (T, T') rtrm | (_, Const (@{const_name "op ="}, _)) => rtrm @@ -349,14 +353,14 @@ val rty = fastype_of rtrm in if rty = T' then rtrm - else mk_repabs lthy (rty, T') rtrm + else mk_repabs ctxt (rty, T') rtrm end | _ => raise (LIFT_MATCH "injection (default)") -fun inj_repabs_trm_chk lthy (rtrm, qtrm) = - inj_repabs_trm lthy (rtrm, qtrm) - |> Syntax.check_term lthy +fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = + inj_repabs_trm ctxt (rtrm, qtrm) + |> Syntax.check_term ctxt end; (* structure *)