# HG changeset patch # User Christian Urban # Date 1257150828 -3600 # Node ID 77ff9624cfd6494d5d2a4ce89cf57047faa8412b # Parent e30997c88050ac80541749627200332ce6414bc8 fixed the problem with types in map diff -r e30997c88050 -r 77ff9624cfd6 FSet.thy --- a/FSet.thy Fri Oct 30 19:03:53 2009 +0100 +++ b/FSet.thy Mon Nov 02 09:33:48 2009 +0100 @@ -44,7 +44,7 @@ thm EMPTY_def quotient_def (for "'a fset") - INSERT :: "'a \ 'a fset \ 'a fet" + INSERT :: "'a \ 'a fset \ 'a fset" where "INSERT \ op #" @@ -168,10 +168,10 @@ thm fold_def (* FIXME: does not work yet for all types*) -quotient_def (for "'a fset") - fmap::"('a \ 'a) \ 'a fset \ 'a fset" +quotient_def (for "'a fset" "'b fset") + fmap::"('a \ 'b) \ 'a fset \ 'b fset" where - "fmap \ (map::('a \ 'a) \ 'a list \ 'a list)" + "fmap \ map" term map term fmap @@ -296,6 +296,9 @@ by simp (rule list_eq_refl) +print_quotients + + ML {* val qty = @{typ "'a fset"} *} ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} diff -r e30997c88050 -r 77ff9624cfd6 QuotMain.thy --- a/QuotMain.thy Fri Oct 30 19:03:53 2009 +0100 +++ b/QuotMain.thy Mon Nov 02 09:33:48 2009 +0100 @@ -159,17 +159,13 @@ 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 + (case (AList.lookup (op =) qenv qty) of SOME rty => SOME (qty, rty) | NONE => NONE) *} @@ -225,7 +221,7 @@ fun mk_identity ty = Abs ("", ty, Bound 0) in - if (AList.defined matches qenv ty) + if (AList.defined (op =) qenv ty) then (get_const flag (the (lookup_qenv qenv ty))) else (case ty of TFree _ => (mk_identity ty, (ty, ty)) @@ -259,11 +255,10 @@ end *} -ML {* lookup_snd *} ML {* fun exchange_ty qenv ty = - case (lookup_snd matches qenv ty) of + case (lookup_snd (op =) qenv ty) of SOME qty => qty | NONE => (case ty of @@ -272,6 +267,18 @@ ) *} +ML {* +fun ppair lthy (ty1, ty2) = + "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")" +*} + +ML {* +fun print_env qenv lthy = + map (ppair lthy) qenv + |> commas + |> tracing +*} + ML {* fun make_const_def nconst_bname otrm mx qenv lthy = let @@ -279,6 +286,11 @@ 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 @@ -288,46 +300,37 @@ 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"]) + val tsig = Sign.tsig_of (ProofContext.theory_of lthy) + + fun find_assoc ((qty', rty')::rest) qty = + let + val inst = Type.typ_match tsig (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 qtys + map (find_assoc qenv) 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) ^ ")" + (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) *} ML {* -fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = +fun parse_qd_spec (qtystrs, ((bind, tystr, 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 qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy val (lhs, rhs) = Logic.dest_equals prop in @@ -340,6 +343,8 @@ OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) *} +(* ML {* show_all_types := true *} *) + section {* ATOMIZE *} text {* @@ -501,10 +506,6 @@ else Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t end - | Const (@{const_name "op ="}, ty) $ t => - if needs_lift rty (fastype_of t) then - (tyRel (fastype_of t) rty rel lthy) $ t - else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) | _ => trm *} @@ -517,31 +518,16 @@ (my_reg lthy rel rty (prop_of thm))) *} -lemma universal_twice: "(\x. (P x \ Q x)) \ ((\x. P x) \ (\x. Q x))" -apply (auto) -done - -lemma implication_twice: "(c \ a) \ (a \ b \ d) \ (a \ b) \ (c \ d)" -apply (auto) -done - ML {* -fun regularize thm rty rel rel_eqv rel_refl lthy = +fun regularize thm rty rel rel_eqv lthy = let val g = build_regularize_goal thm rty rel lthy; fun tac ctxt = - (ObjectLogic.full_atomize_tac) THEN' - REPEAT_ALL_NEW (FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - rtac @{thm implication_twice}, - (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])]) i)), - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]); + (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW + (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' + (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); in cthm OF [thm] @@ -565,10 +551,14 @@ ) *} +ML {* make_const_def *} + ML {* fun old_get_fun flag rty qty lthy ty = get_fun flag [(qty, rty)] lthy ty +*} +ML {* fun old_make_const_def nconst_bname otrm mx rty qty lthy = make_const_def nconst_bname otrm mx [(qty, rty)] lthy *} @@ -926,7 +916,7 @@ val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; val consts = lookup_quot_consts defs; val t_a = atomize_thm t; - val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; + val t_r = regularize t_a rty rel rel_eqv lthy; val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val abs = findabs rty (prop_of t_a); val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; diff -r e30997c88050 -r 77ff9624cfd6 QuotTest.thy --- a/QuotTest.thy Fri Oct 30 19:03:53 2009 +0100 +++ b/QuotTest.thy Mon Nov 02 09:33:48 2009 +0100 @@ -2,6 +2,7 @@ imports QuotMain begin + section {* various tests for quotient types*} datatype trm = var "nat" diff -r e30997c88050 -r 77ff9624cfd6 quotient.ML --- a/quotient.ML Fri Oct 30 19:03:53 2009 +0100 +++ b/quotient.ML Mon Nov 02 09:33:48 2009 +0100 @@ -6,7 +6,7 @@ val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory val note: binding * thm -> local_theory -> thm * local_theory - val maps_lookup: theory -> string -> maps_info option + val maps_lookup_thy: theory -> string -> maps_info option 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 @@ -32,7 +32,9 @@ val extend = I fun merge _ = Symtab.merge (K true)) -val maps_lookup = Symtab.lookup o MapsData.get +val maps_lookup_thy = Symtab.lookup o MapsData.get + + fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) @@ -242,7 +244,7 @@ val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name (* storing the quot-info *) - val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2 + val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))