# HG changeset patch # User Christian Urban # Date 1256739911 -3600 # Node ID df05cd030d2f90f4cc0d64e220625fe07b1428be # Parent 89a2ff3f82c779f0e4ca2ca7fd94dfbcded7b5ab added infrastructure for defining lifted constants diff -r 89a2ff3f82c7 -r df05cd030d2f FSet.thy --- a/FSet.thy Wed Oct 28 10:29:00 2009 +0100 +++ b/FSet.thy Wed Oct 28 15:25:11 2009 +0100 @@ -36,7 +36,7 @@ ML {* @{term "Abs_fset"} *} local_setup {* - make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} term Nil @@ -45,7 +45,7 @@ local_setup {* - make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} term Cons @@ -53,7 +53,7 @@ thm INSERT_def local_setup {* - make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} term append @@ -78,7 +78,7 @@ | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" local_setup {* - make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} term card1 @@ -143,7 +143,7 @@ done local_setup {* - make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} term membship @@ -151,7 +151,7 @@ thm IN_def local_setup {* - make_const_def @{binding fold} @{term "fold1::('b \ 'b \ 'b) \ ('a \ 'b) \ 'b \ 'a list \ 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + old_make_const_def @{binding fold} @{term "fold1::('b \ 'b \ 'b) \ ('a \ 'b) \ 'b \ 'a list \ 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} term fold1 @@ -159,7 +159,7 @@ thm fold_def local_setup {* - make_const_def @{binding fmap} @{term "map::('a \ 'a) \ 'a list \ 'a list"} NoSyn + old_make_const_def @{binding fmap} @{term "map::('a \ 'a) \ 'a list \ 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} diff -r 89a2ff3f82c7 -r df05cd030d2f IntEx.thy --- a/IntEx.thy Wed Oct 28 10:29:00 2009 +0100 +++ b/IntEx.thy Wed Oct 28 15:25:11 2009 +0100 @@ -12,27 +12,17 @@ apply(auto simp add: mem_def expand_fun_eq) done -print_quotients - -typ my_int +quotient_def (for my_int) + ZERO::"my_int" +where + "ZERO \ (0::nat, 0::nat)" -local_setup {* - make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd -*} - -term ZERO thm ZERO_def -(* -quotient_def (with my_int) - ZERO :: "my_int" +quotient_def (for my_int) + ONE::"my_int" where - "ZERO \ (0::nat, 0::nat)" -*) - -local_setup {* - make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd -*} + "ONE \ (1::nat, 0::nat)" term ONE thm ONE_def @@ -42,9 +32,10 @@ where "my_plus (x, y) (u, v) = (x + u, y + v)" -local_setup {* - make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd -*} +quotient_def (for my_int) + PLUS::"my_int \ my_int \ my_int" +where + "PLUS \ my_plus" term PLUS thm PLUS_def @@ -55,7 +46,7 @@ "my_neg (x, y) = (y, x)" local_setup {* - make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd + old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd *} term NEG @@ -72,7 +63,7 @@ "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" local_setup {* - make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd + old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd *} term MULT @@ -85,7 +76,7 @@ "my_le (x, y) (u, v) = (x+v \ u+y)" local_setup {* - make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd + old_make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd *} term LE diff -r 89a2ff3f82c7 -r df05cd030d2f LamEx.thy --- a/LamEx.thy Wed Oct 28 10:29:00 2009 +0100 +++ b/LamEx.thy Wed Oct 28 15:25:11 2009 +0100 @@ -23,11 +23,15 @@ print_quotients local_setup {* - make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> - make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> - make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd + old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> + old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> + old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd *} +thm Var_def +thm App_def +thm Lam_def + lemma real_alpha: assumes "t = ([(a,b)]\s)" "a\s" shows "Lam a t = Lam b s" diff -r 89a2ff3f82c7 -r df05cd030d2f QuotMain.thy --- a/QuotMain.thy Wed Oct 28 10:29:00 2009 +0100 +++ b/QuotMain.thy Wed Oct 28 15:25:11 2009 +0100 @@ -147,32 +147,7 @@ ML {* maps_lookup @{theory} "*" *} ML {* maps_lookup @{theory} "fun" *} -ML {* -fun matches ty1 ty2 = - Type.raw_instance (ty1, Logic.varifyT ty2) -*} - - - -ML {* -val quot_def_parser = - (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- - ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- - (OuterParse.binding -- - Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- - OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) -*} - -ML {* -fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy -*} - -ML {* -val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" - OuterKeyword.thy_decl (quot_def_parser >> test) -*} - -(* FIXME: auxiliary function *) +text {* FIXME: auxiliary function *} ML {* val no_vars = Thm.rule_attribute (fn context => fn th => let @@ -184,7 +159,19 @@ section {* lifting of constants *} ML {* +(* whether ty1 is an instance of ty2 *) +fun matches (ty1, ty2) = + Type.raw_instance (ty1, Logic.varifyT ty2) +fun lookup_snd _ [] _ = NONE + | lookup_snd eq ((value, key)::xs) key' = + if eq (key', key) then SOME value + else lookup_snd eq xs key'; + +fun lookup_qenv qenv qty = + (case (AList.lookup matches qenv qty) of + SOME rty => SOME (qty, rty) + | NONE => NONE) *} ML {* @@ -198,10 +185,9 @@ fun negF absF = repF | negF repF = absF -fun get_fun flag rty qty lthy ty = +fun get_fun flag qenv 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 @@ -226,22 +212,27 @@ (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) end - val thy = ProofContext.theory_of lthy - - fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) - | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) + fun get_const flag (qty, rty) = + let + val thy = ProofContext.theory_of lthy + val qty_name = Long_Name.base_name (fst (dest_Type qty)) + in + case flag of + absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) + | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) + end fun mk_identity ty = Abs ("", ty, Bound 0) in - if ty = qty - then (get_const flag) + if (AList.defined matches qenv ty) + then (get_const flag (the (lookup_qenv qenv ty))) else (case ty of TFree _ => (mk_identity ty, (ty, ty)) | Type (_, []) => (mk_identity ty, (ty, ty)) | Type ("fun" , [ty1, ty2]) => - get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] - | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) + get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] + | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) | _ => raise ERROR ("no type variables") ) end @@ -251,50 +242,104 @@ text {* produces the definition for a lifted constant *} ML {* -fun get_const_def nconst oconst rty qty lthy = +fun get_const_def nconst otrm qenv 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 repF rty qty lthy) arg_tys - val abs_fn = (fst o get_fun absF rty qty lthy) res_ty + val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys + val abs_fn = (fst o get_fun absF qenv lthy) res_ty fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2 - val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn) + val fns = Library.foldr mk_fun_map (rep_fns, abs_fn) |> Syntax.check_term lthy in - fns $ oconst + fns $ otrm end *} +ML {* lookup_snd *} + ML {* -fun exchange_ty rty qty ty = - if ty = rty - then qty - else +fun exchange_ty qenv ty = + case (lookup_snd matches qenv ty) of + SOME qty => qty + | NONE => (case ty of - Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) + Type (s, tys) => Type (s, map (exchange_ty qenv) tys) | _ => ty ) *} ML {* -fun make_const_def nconst_bname oconst mx rty qty lthy = +fun make_const_def nconst_bname otrm mx qenv lthy = let - val oconst_ty = fastype_of oconst - val nconst_ty = exchange_ty rty qty oconst_ty + val otrm_ty = fastype_of otrm + val nconst_ty = exchange_ty qenv otrm_ty val nconst = Const (Binding.name_of nconst_bname, nconst_ty) - val def_trm = get_const_def nconst oconst rty qty lthy + val def_trm = get_const_def nconst otrm qenv lthy in define (nconst_bname, mx, def_trm) lthy end *} +ML {* +fun build_qenv lthy qtys = +let + val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) + + fun find_assoc qty = + case (AList.lookup matches qenv qty) of + SOME rty => (qty, rty) + | NONE => error (implode + ["Quotient type ", + quote (Syntax.string_of_typ lthy qty), + " does not exists"]) +in + map find_assoc qtys +end +*} + +ML {* +(* taken from isar_syn.ML *) +val constdecl = + OuterParse.binding -- + (OuterParse.where_ >> K (NONE, NoSyn) || + OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- + OuterParse.opt_mixfix' --| OuterParse.where_) || + Scan.ahead (OuterParse.$$$ "(") |-- + OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE)) +*} + +ML {* +val qd_parser = + (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- + (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) +*} + +ML {* +fun pair lthy (ty1, ty2) = + "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")" +*} + +ML {* +fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = +let + val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs + val qenv = build_qenv lthy qtys + val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy + val (lhs, rhs) = Logic.dest_equals prop +in + make_const_def bind rhs mx qenv lthy |> snd +end +*} + +ML {* +val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" + OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) +*} + section {* ATOMIZE *} text {* @@ -587,17 +632,36 @@ by (simp add: id_def) ML {* +fun old_exchange_ty rty qty ty = + if ty = rty + then qty + else + (case ty of + Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) + | _ => ty + ) +*} + +ML {* +fun old_get_fun flag rty qty lthy ty = + get_fun flag [(qty, rty)] lthy ty + +fun old_make_const_def nconst_bname otrm mx rty qty lthy = + make_const_def nconst_bname otrm mx [(qty, rty)] lthy +*} + +ML {* fun build_repabs_term lthy thm constructors rty qty = let fun mk_rep tm = let - val ty = exchange_ty rty qty (fastype_of tm) - in fst (get_fun repF rty qty lthy ty) $ tm end + val ty = old_exchange_ty rty qty (fastype_of tm) + in fst (old_get_fun repF rty qty lthy ty) $ tm end fun mk_abs tm = let - val ty = exchange_ty rty qty (fastype_of tm) in - fst (get_fun absF rty qty lthy ty) $ tm end + val ty = old_exchange_ty rty qty (fastype_of tm) in + fst (old_get_fun absF rty qty lthy ty) $ tm end fun is_constructor (Const (x, _)) = member (op =) constructors x | is_constructor _ = false; diff -r 89a2ff3f82c7 -r df05cd030d2f quotient.ML --- a/quotient.ML Wed Oct 28 10:29:00 2009 +0100 +++ b/quotient.ML Wed Oct 28 15:25:11 2009 +0100 @@ -10,7 +10,8 @@ val maps_update_thy: string -> maps_info -> theory -> theory val maps_update: string -> maps_info -> Proof.context -> Proof.context val print_quotdata: Proof.context -> unit - val quotdata_lookup: theory -> quotient_info list + val quotdata_lookup_thy: theory -> quotient_info list + val quotdata_lookup: Proof.context -> quotient_info list val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context end; @@ -70,7 +71,8 @@ val extend = I fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) -val quotdata_lookup = QuotData.get +val quotdata_lookup_thy = QuotData.get +val quotdata_lookup = QuotData.get o ProofContext.theory_of fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy