# HG changeset patch # User Christian Urban # Date 1261808130 -3600 # Node ID 3a48ffcf0f9a0f5624c18ef5aea9bc55ad4df73a # Parent 8237786171f14faea179b0d66c91d6441d2422b8 generalised absrep function; needs consolidation diff -r 8237786171f1 -r 3a48ffcf0f9a Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Fri Dec 25 00:58:06 2009 +0100 +++ b/Quot/Examples/AbsRepTest.thy Sat Dec 26 07:15:30 2009 +0100 @@ -2,21 +2,87 @@ imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List begin +ML {* open Quotient_Term *} + print_maps + 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 - apply(auto) - done + by auto quotient_type 'a foo = "('a * 'a) list" / "\(xs::('a * 'a) list) ys. \e. e \ set xs \ e \ set ys" apply(rule equivpI) unfolding reflp_def symp_def transp_def - apply(auto) - done + by auto + +quotient_type + 'a bar = "('a * int) list" / "\(xs::('a * int) list) ys. \e. e \ set xs \ e \ set ys" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + by auto + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient_type int = "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 +*} + +(* PROBLEM +ML {* +absrep_fun_chk 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 +*} + + +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 @@ -24,12 +90,6 @@ Quotient_Info.quotient_rules_get @{context} *} -quotient_type int = "nat \ nat" / "\(x, y) (u, v). x + v = u + (y::nat)" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(auto) - done - print_quotients ML {* diff -r 8237786171f1 -r 3a48ffcf0f9a Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Fri Dec 25 00:58:06 2009 +0100 +++ b/Quot/Examples/IntEx2.thy Sat Dec 26 07:15:30 2009 +0100 @@ -1,5 +1,5 @@ theory IntEx2 -imports "../QuotMain" Nat +imports "../QuotMain" "../QuotProd" Nat (*uses ("Tools/numeral.ML") ("Tools/numeral_syntax.ML") @@ -196,7 +196,7 @@ lemma add: "(abs_int (x,y)) + (abs_int (u,v)) = (abs_int (x + u, y + v))" -apply(simp add: plus_int_def) +apply(simp add: plus_int_def id_simps) apply(fold plus_raw.simps) apply(rule Quotient_rel_abs[OF Quotient_int]) apply(rule plus_raw_rsp_aux) diff -r 8237786171f1 -r 3a48ffcf0f9a Quot/Examples/LarryInt.thy --- a/Quot/Examples/LarryInt.thy Fri Dec 25 00:58:06 2009 +0100 +++ b/Quot/Examples/LarryInt.thy Sat Dec 26 07:15:30 2009 +0100 @@ -2,7 +2,7 @@ header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} theory LarryInt -imports Nat "../QuotMain" +imports Nat "../QuotMain" "../QuotProd" begin fun @@ -361,22 +361,6 @@ apply(auto iff: nat_raw_def) done -ML {* - let - val parser = Args.context -- Scan.lift Args.name_source - fun term_pat (ctxt, str) = - str |> ProofContext.read_term_pattern ctxt - |> ML_Syntax.print_term - |> ML_Syntax.atomic -in - ML_Antiquote.inline "term_pat" (parser >> term_pat) -end - -*} - -consts test::"'b \ 'b \ 'b" - - lemma nat_le_eq_zle: "0 < w \ 0 \ z \ (nat2 w \ nat2 z) = (w\z)" unfolding less_int_def apply(lifting nat_le_eq_zle_raw) diff -r 8237786171f1 -r 3a48ffcf0f9a Quot/quotient_term.ML --- a/Quot/quotient_term.ML Fri Dec 25 00:58:06 2009 +0100 +++ b/Quot/quotient_term.ML Sat Dec 26 07:15:30 2009 +0100 @@ -34,27 +34,59 @@ fun negF absF = repF | negF repF = absF +val mk_id = Const (@{const_name "id"}, dummyT) fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) +fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) + fun mk_compose flag (trm1, trm2) = case flag of absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 -fun get_map ctxt ty_str = +fun get_mapfun ctxt s = let val thy = ProofContext.theory_of ctxt - val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."]) - val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc + val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.") + val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc in Const (mapfun, dummyT) end -fun get_absrep_const flag ctxt _ qty = -(* FIXME: check here that the type-constructors of _ and qty are related *) +fun mk_mapfun ctxt vs ty = +let + val vs' = map (mk_Free) vs + + fun mk_mapfun_aux ty = + case ty of + TVar _ => mk_Free ty + | Type (_, []) => mk_id + | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) + | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") +in + fold_rev Term.lambda vs' (mk_mapfun_aux ty) +end + +fun get_rty_qty ctxt s = let val thy = ProofContext.theory_of ctxt - val qty_name = Long_Name.base_name (fst (dest_Type qty)) + val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") + val qdata = (quotdata_lookup thy s) handle NotFound => raise exc +in + (#rtyp qdata, #qtyp qdata) +end + +fun double_lookup rtyenv qtyenv v = +let + val v' = fst (dest_TVar v) +in + (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) +end + +fun absrep_const flag ctxt qty_str = +let + val thy = ProofContext.theory_of ctxt + val qty_name = Long_Name.base_name qty_str in case flag of absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) @@ -62,39 +94,62 @@ end 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 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_absrep_const flag ctxt rty qty - | (Type (s, tys), Type (s', tys')) => - let - val args = map (absrep_fun flag ctxt) (tys ~~ tys') - val result = list_comb (get_map ctxt s, args) - in + if rty = qty + then mk_identity qty + else + case (rty, qty) of + (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => + let + val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') + val arg2 = absrep_fun flag ctxt (ty2, ty2') + in + list_comb (get_mapfun ctxt "fun", [arg1, arg2]) + end + | (Type (s, tys), Type (s', tys')) => if s = s' - 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)") - | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") - | _ => raise (LIFT_MATCH "absrep_fun (default)") + then + let + val args = map (absrep_fun flag ctxt) (tys ~~ tys') + in + list_comb (get_mapfun ctxt s, args) + end + else + let + val thy = ProofContext.theory_of ctxt + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty + val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty + 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) + in + mk_compose flag (absrep_const flag ctxt s', result) + end + | (TFree x, TFree x') => + if x = x' + then mk_identity qty + else raise (LIFT_MATCH "absrep_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") + | _ => + let + val rty_str = Syntax.string_of_typ ctxt rty + val qty_str = Syntax.string_of_typ ctxt qty + in + raise (LIFT_MATCH ("absrep_fun (default) " ^ rty_str ^ " " ^ qty_str)) + end fun absrep_fun_chk flag ctxt (rty, qty) = +let + val rty_str = Syntax.string_of_typ ctxt rty + val qty_str = Syntax.string_of_typ ctxt qty + val _ = tracing "rty / qty" + val _ = tracing rty_str + val _ = tracing qty_str +in absrep_fun flag ctxt (rty, qty) |> Syntax.check_term ctxt - +end (* Regularizing an rtrm means: diff -r 8237786171f1 -r 3a48ffcf0f9a Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Fri Dec 25 00:58:06 2009 +0100 +++ b/Quot/quotient_typ.ML Sat Dec 26 07:15:30 2009 +0100 @@ -39,6 +39,7 @@ end +(********************************) (* definition of quotient types *) (********************************) @@ -52,11 +53,11 @@ |> Variable.variant_frees lthy [rel] |> map Free in - lambda c - (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_eq (c, (rel $ x)))) + lambda c (HOLogic.exists_const rty $ + lambda x (HOLogic.mk_eq (c, (rel $ x)))) end + (* makes the new type definitions and proves non-emptyness *) fun typedef_make (vs, qty_name, mx, rel, rty) lthy = let @@ -69,10 +70,11 @@ Local_Theory.theory_result (Typedef.add_typedef false NONE (qty_name, vs, mx) - (typedef_term rel rty lthy) - NONE typedef_tac) lthy + (typedef_term rel rty lthy) + NONE typedef_tac) lthy end + (* tactic to prove the Quot_Type theorem for the new type *) fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let @@ -89,6 +91,7 @@ rtac rep_inj]) 1 end + (* proves the Quot_Type theorem *) fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let @@ -116,6 +119,7 @@ (K typedef_quotient_thm_tac) end + (* main function for constructing a quotient type *) fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = let @@ -164,6 +168,7 @@ ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) end + (* sanity checks of the quotient type specifications *) fun sanity_check ((vs, qty_name, _), (rty, rel)) = let @@ -203,7 +208,10 @@ if null errs then () else error (cat_lines errs) end + +(******************************) (* interface and syntax setup *) +(******************************) (* the ML-interface takes a list of 5-tuples consisting of *) (* *)