# HG changeset patch # User Christian Urban # Date 1261859780 -3600 # Node ID a28f805df355f7dea48f2a468bfebc4306feccf0 # Parent f0a78fda343fe521a933898aa9feaad6c1d271ac renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy diff -r f0a78fda343f -r a28f805df355 Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Sat Dec 26 20:45:37 2009 +0100 +++ b/Quot/Examples/AbsRepTest.thy Sat Dec 26 21:36:20 2009 +0100 @@ -4,142 +4,101 @@ ML {* open Quotient_Term *} -print_maps - +ML {* +fun test_funs flag ctxt (rty, qty) = + (absrep_fun_chk flag ctxt (rty, qty) + |> Syntax.string_of_term ctxt + |> writeln; + equiv_relation_chk ctxt (rty, qty) + |> Syntax.string_of_term ctxt + |> writeln) +*} -quotient_type - 'a fset = "'a list" / "\xs ys. \e. e \ set xs \ e \ set ys" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - by auto +definition + erel1 (infixl "\1" 50) +where + "erel1 \ \xs ys. \e. e \ set xs \ e \ set ys" quotient_type - 'a foo = "('a * 'a) list" / "\(xs::('a * 'a) list) ys. \e. e \ set xs \ e \ set ys" + 'a fset = "'a list" / erel1 apply(rule equivpI) - unfolding reflp_def symp_def transp_def + unfolding erel1_def reflp_def symp_def transp_def by auto +definition + erel2 (infixl "\2" 50) +where + "erel2 \ \(xs::('a * 'a) list) ys. \e. e \ set xs \ e \ set ys" + quotient_type - 'a bar = "('a * int) list" / "\(xs::('a * int) list) ys. \e. e \ set xs \ e \ set ys" + 'a foo = "('a * 'a) list" / erel2 apply(rule equivpI) - unfolding reflp_def symp_def transp_def + unfolding erel2_def reflp_def symp_def transp_def + by auto + +definition + erel3 (infixl "\3" 50) +where + "erel3 \ \(xs::('a * int) list) ys. \e. e \ set xs \ e \ set ys" + +quotient_type + 'a bar = "('a * int) list" / "erel3" + apply(rule equivpI) + unfolding erel3_def reflp_def symp_def transp_def by auto fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infixl "\4" 50) where "intrel (x, y) (u, v) = (x + v = u + y)" -quotient_type int = "nat \ nat" / intrel +quotient_type myint = "nat \ nat" / intrel by (auto simp add: equivp_def expand_fun_eq) -print_quotients - ML {* -absrep_fun_chk absF @{context} - (@{typ "('a * 'a) list"}, - @{typ "'a foo"}) -|> Syntax.string_of_term @{context} -|> writeln +test_funs absF @{context} + (@{typ "nat \ nat"}, + @{typ "myint"}) *} -(* PROBLEM ML {* -absrep_fun_chk absF @{context} +test_funs absF @{context} + (@{typ "('a * 'a) list"}, + @{typ "'a foo"}) +*} + +ML {* +test_funs absF @{context} (@{typ "(('a list) * int) list"}, @{typ "('a fset) bar"}) -|> Syntax.string_of_term @{context} -|> writeln -*}*) - -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 "nat \ nat"}, - @{typ "int"}) -|> Syntax.string_of_term @{context} -|> writeln +test_funs absF @{context} + (@{typ "('a list) list"}, + @{typ "('a fset) fset"}) +*} + +ML {* +test_funs absF @{context} + (@{typ "(('a * 'a) list) list"}, + @{typ "(('a * 'a) fset) fset"}) +*} + +ML {* +test_funs absF @{context} + (@{typ "(nat * nat) list"}, + @{typ "myint fset"}) +*} + +ML {* +test_funs absF @{context} + (@{typ "('a list) list \ 'a"}, + @{typ "('a fset) fset \ 'a"}) *} -term abs_foo -term rep_foo -term "abs_foo o map (prod_fun id id)" -term "map (prod_fun id id) o rep_foo" - -ML {* -absrep_fun_chk absF @{context} - (@{typ "('a * 'a) list"}, - @{typ "'a foo"}) -|> Syntax.string_of_term @{context} -|> writeln -*} - -typ "('a fset) foo" - -print_quotients - -ML{* -Quotient_Info.quotient_rules_get @{context} -*} - -print_quotients - -ML {* -open Quotient_Term; -*} - -ML {* -absrep_fun_chk absF @{context} - (@{typ "(('a * 'a) list) list"}, - @{typ "(('a * 'a) fset) fset"}) -|> Syntax.string_of_term @{context} -|> writeln -*} - -(* -ML {* -absrep_fun_chk absF @{context} - (@{typ "('a * 'a) list"}, - @{typ "'a foo"}) -|> 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 f0a78fda343f -r a28f805df355 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Sat Dec 26 20:45:37 2009 +0100 +++ b/Quot/quotient_term.ML Sat Dec 26 21:36:20 2009 +0100 @@ -7,6 +7,9 @@ val absrep_fun: flag -> Proof.context -> (typ * typ) -> term val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term + val equiv_relation: Proof.context -> (typ * typ) -> term + val equiv_relation_chk: Proof.context -> (typ * typ) -> term + val regularize_trm: Proof.context -> (term * term) -> term val regularize_trm_chk: Proof.context -> (term * term) -> term @@ -57,7 +60,7 @@ (* 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 *) +(* correspond to the type variables in rty) *) fun mk_mapfun ctxt vs ty = let val vs' = map (mk_Free) vs @@ -83,8 +86,9 @@ (#rtyp qdata, #qtyp qdata) end -(* receives two type-environments and looks *) -(* up in both of them the variable v *) +(* 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 val v' = fst (dest_TVar v) @@ -103,7 +107,16 @@ | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) end -(* produces the aggregate absrep function *) +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 +in + raise LIFT_MATCH (space_implode " " + ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) +end + +(* produces an aggregate absrep function *) (* *) (* - In case of function types and TFrees, we recurse, taking in *) (* the first case the polarity change into account. *) @@ -157,12 +170,11 @@ else let val thy = ProofContext.theory_of ctxt - val exc = (LIFT_MATCH "absrep_fun (Types do not match.)") val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val (rtyenv, qtyenv) = - (Sign.typ_match thy (rty_pat, rty) Vartab.empty, - Sign.typ_match thy (qty_pat, qty) Vartab.empty) - handle MATCH_TYPE => raise exc + val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty + handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty + val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty + handle MATCH_TYPE => absrep_match_err ctxt 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 @@ -182,31 +194,9 @@ |> Syntax.check_term ctxt -(* Regularizing an rtrm means: - - - 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 - corresponding equivalence relations, for example: - - A = B ----> R A B - - or - - A = B ----> (R ===> R) A B - - for more complicated types of A and B -*) +(**********************************) +(* Aggregate Equivalence Relation *) +(**********************************) (* instantiates TVars so that the term is of type ty *) fun force_typ ctxt trm ty = @@ -239,7 +229,7 @@ (* that will be the argument of Respects *) (* FIXME: check that the types correspond to each other? *) -fun mk_resp_arg ctxt (rty, qty) = +fun equiv_relation ctxt (rty, qty) = if rty = qty then HOLogic.eq_const rty else @@ -248,7 +238,7 @@ if s = s' then let - val args = map (mk_resp_arg ctxt) (tys ~~ tys') + val args = map (equiv_relation ctxt) (tys ~~ tys') in list_comb (get_relmap ctxt s, args) end @@ -259,6 +249,42 @@ force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) end | _ => HOLogic.eq_const rty + +fun equiv_relation_chk ctxt (rty, qty) = + equiv_relation ctxt (rty, qty) + |> Syntax.check_term ctxt + + +(******************) +(* Regularization *) +(******************) + +(* Regularizing an rtrm means: + + - 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 + corresponding equivalence relations, for example: + + A = B ----> R A B + + or + + A = B ----> (R ===> R) A B + + for more complicated types of A and B +*) + val mk_babs = Const (@{const_name Babs}, dummyT) val mk_ball = Const (@{const_name Ball}, dummyT) @@ -292,7 +318,7 @@ val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) in if ty = ty' then subtrm - else mk_babs $ (mk_resp $ mk_resp_arg ctxt (ty, ty')) $ subtrm + else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm end | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => @@ -300,7 +326,7 @@ 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 ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => @@ -308,20 +334,20 @@ 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 ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + else mk_bex $ (mk_resp $ equiv_relation 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 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 *) (rel, Const (@{const_name "op ="}, ty')) => let val exc = LIFT_MATCH "regularise (relation mismatch)" val rel_ty = fastype_of rel - val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') + val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') in if rel' aconv rel then rtrm else raise exc end @@ -376,6 +402,10 @@ regularize_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt +(*********************) +(* Rep/Abs Injection *) +(*********************) + (* Injection of Rep/Abs means: