# HG changeset patch # User Cezary Kaliszyk # Date 1257265843 -3600 # Node ID c55883442514ace654b47f5910149200d27d95c6 # Parent fe6eb116b341099298d4553ac10bfbb307d5a16a# Parent 4d58c02289caa91dc10b0e97a80ee7c7b3a8200d merge diff -r fe6eb116b341 -r c55883442514 FSet.thy --- a/FSet.thy Tue Nov 03 17:30:27 2009 +0100 +++ b/FSet.thy Tue Nov 03 17:30:43 2009 +0100 @@ -34,7 +34,7 @@ thm "Rep_fset" thm "ABS_fset_def" -quotient_def (for "'a fset") +quotient_def EMPTY :: "'a fset" where "EMPTY \ ([]::'a list)" @@ -43,7 +43,7 @@ term EMPTY thm EMPTY_def -quotient_def (for "'a fset") +quotient_def INSERT :: "'a \ 'a fset \ 'a fset" where "INSERT \ op #" @@ -52,7 +52,7 @@ term INSERT thm INSERT_def -quotient_def (for "'a fset") +quotient_def FUNION :: "'a fset \ 'a fset \ 'a fset" where "FUNION \ (op @)" @@ -78,7 +78,7 @@ card1_nil: "(card1 []) = 0" | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" -quotient_def (for "'a fset") +quotient_def CARD :: "'a fset \ nat" where "CARD \ card1" @@ -144,7 +144,7 @@ apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) done -quotient_def (for "'a fset") +quotient_def IN :: "'a \ 'a fset \ bool" where "IN \ membship" @@ -168,7 +168,7 @@ thm fold_def (* FIXME: does not work yet for all types*) -quotient_def (for "'a fset" "'b fset") +quotient_def fmap::"('a \ 'b) \ 'a fset \ 'b fset" where "fmap \ map" diff -r fe6eb116b341 -r c55883442514 IntEx.thy --- a/IntEx.thy Tue Nov 03 17:30:27 2009 +0100 +++ b/IntEx.thy Tue Nov 03 17:30:43 2009 +0100 @@ -14,13 +14,15 @@ print_theorems -quotient_def (for my_int) +quotient_def ZERO::"my_int" where "ZERO \ (0::nat, 0::nat)" +term ZERO +thm ZERO_def -quotient_def (for my_int) +quotient_def ONE::"my_int" where "ONE \ (1::nat, 0::nat)" @@ -33,7 +35,7 @@ where "my_plus (x, y) (u, v) = (x + u, y + v)" -quotient_def (for my_int) +quotient_def PLUS::"my_int \ my_int \ my_int" where "PLUS \ my_plus" @@ -48,13 +50,12 @@ thm MPLUS_def thm MPLUS_def_raw - fun my_neg :: "(nat \ nat) \ (nat \ nat)" where "my_neg (x, y) = (y, x)" -quotient_def (for my_int) +quotient_def NEG::"my_int \ my_int" where "NEG \ my_neg" @@ -72,7 +73,7 @@ where "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" -quotient_def (for my_int) +quotient_def MULT::"my_int \ my_int \ my_int" where "MULT \ my_mult" @@ -86,7 +87,7 @@ where "my_le (x, y) (u, v) = (x+v \ u+y)" -quotient_def (for my_int) +quotient_def LE :: "my_int \ my_int \ bool" where "LE \ my_le" diff -r fe6eb116b341 -r c55883442514 LamEx.thy --- a/LamEx.thy Tue Nov 03 17:30:27 2009 +0100 +++ b/LamEx.thy Tue Nov 03 17:30:43 2009 +0100 @@ -37,17 +37,17 @@ print_quotients -quotient_def (for lam) +quotient_def Var :: "name \ lam" where "Var \ rVar" -quotient_def (for lam) +quotient_def App :: "lam \ lam \ lam" where "App \ rApp" -quotient_def (for lam) +quotient_def Lam :: "name \ lam \ lam" where "Lam \ rLam" @@ -56,7 +56,7 @@ thm App_def thm Lam_def -quotient_def (for lam) +quotient_def fv :: "lam \ name set" where "fv \ rfv" @@ -66,10 +66,10 @@ (* definition of overloaded permutation function *) (* for the lifted type lam *) overloading - perm_lam \ "perm :: 'x prm \ lam \ lam" (unchecked) + perm_lam \ "perm :: 'x prm \ lam \ lam" (unchecked) begin -quotient_def (for lam) +quotient_def perm_lam :: "'x prm \ lam \ lam" where "perm_lam \ (perm::'x prm \ rlam \ rlam)" @@ -308,14 +308,11 @@ thm alpha.induct lemma rvar_inject: "rVar a \ rVar b \ (a = b)" -apply (rule alpha.cases) -apply (assumption) -apply (assumption) -apply (simp_all) -apply (cases "a = b") -apply (simp_all) -apply (cases "ba = b") -apply (simp_all) +apply (erule alpha.cases) +apply (simp add: rlam.inject) +apply (simp) +apply (simp) +done lemma var_inject_test: diff -r fe6eb116b341 -r c55883442514 QuotMain.thy --- a/QuotMain.thy Tue Nov 03 17:30:27 2009 +0100 +++ b/QuotMain.thy Tue Nov 03 17:30:43 2009 +0100 @@ -140,8 +140,15 @@ section {* type definition for the quotient type *} +(* the auxiliary data for the quotient types *) use "quotient_info.ML" -use "quotient.ML" + +ML {* +fun error_msg pre post msg = + msg |> quote + |> enclose (pre ^ " ") (" " ^ post) + |> error +*} declare [[map list = (map, LIST_REL)]] declare [[map * = (prod_fun, prod_rel)]] @@ -151,6 +158,11 @@ ML {* maps_lookup @{theory} "*" *} ML {* maps_lookup @{theory} "fun" *} + +(* definition of the quotient types *) +use "quotient.ML" + + text {* FIXME: auxiliary function *} ML {* val no_vars = Thm.rule_attribute (fn context => fn th => @@ -238,7 +250,6 @@ end *} - text {* produces the definition for a lifted constant *} ML {* @@ -290,65 +301,56 @@ 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 otrm qenv lthy - - val _ = print_env qenv lthy - val _ = Syntax.string_of_typ lthy otrm_ty |> tracing - val _ = Syntax.string_of_typ lthy nconst_ty |> tracing - val _ = Syntax.string_of_term lthy def_trm |> tracing 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) - val thy = ProofContext.theory_of lthy - - fun find_assoc ((qty', rty')::rest) qty = - let - val inst = Sign.typ_match thy (qty', qty) Vartab.empty - in - (Envir.norm_type inst qty, Envir.norm_type inst rty') - end - | find_assoc [] qty = - let - val qtystr = quote (Syntax.string_of_typ lthy qty) - in - error (implode ["Quotient type ", qtystr, " does not exists"]) - end -in - map (find_assoc qenv) qtys -end +(* difference of two types *) +fun diff (T, S) Ds = + case (T, S) of + (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds + | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds + | (Type (a, Ts), Type (b, Us)) => + if a = b then diffs (Ts, Us) Ds else (T, S)::Ds + | _ => (T, S)::Ds +and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) + | diffs ([], []) Ds = Ds + | diffs _ _ = error "Unequal length of type arguments" *} - ML {* -fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy = +fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy = let - val (lhs_, rhs) = Logic.dest_equals prop + val (_, rhs) = Logic.dest_equals prop + val rty = fastype_of rhs + val qenv = distinct (op=) (diff (qty, rty) []) in make_const_def bind rhs mx qenv lthy end *} ML {* -val quotdef_parser = - Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- - (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- - OuterParse.prop)) >> OuterParse.triple2 +val constdecl = + OuterParse.binding -- + (OuterParse.$$$ "::" |-- OuterParse.!!! + (OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_)) + >> OuterParse.triple2; *} ML {* -fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = +val quotdef_parser = + (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) +*} + +ML {* +fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy = let - val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs) - val qenv = build_qenv lthy qtys - val qty = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr - val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy + val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr + val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr in - quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd + quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy |> snd end *} diff -r fe6eb116b341 -r c55883442514 quotient_info.ML --- a/quotient_info.ML Tue Nov 03 17:30:27 2009 +0100 +++ b/quotient_info.ML Tue Nov 03 17:30:43 2009 +0100 @@ -11,11 +11,16 @@ 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 + + type qenv = (typ * typ) list + val mk_qenv: Proof.context -> qenv + val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option end; structure Quotient_Info: QUOTIENT_INFO = struct + (* data containers *) (*******************) @@ -102,6 +107,22 @@ OuterSyntax.improper_command "print_quotients" "print out all quotients" OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) + +(* environments of quotient and raw types *) +type qenv = (typ * typ) list + +fun mk_qenv ctxt = +let + val qinfo = quotdata_lookup ctxt +in + map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo +end + +fun lookup_qenv _ [] _ = NONE + | lookup_qenv eq ((qty, rty)::xs) qty' = + if eq (qty', qty) then SOME (qty, rty) + else lookup_qenv eq xs qty' + end; (* structure *) open Quotient_Info \ No newline at end of file