# HG changeset patch # User Christian Urban # Date 1261256674 -3600 # Node ID c1989de100b42a49d3abab6b1eeb01fee58fa366 # Parent 119f7d6a3556bc42ad9332cdd5e5c1471916e00e various tunings; map_lookup now raises an exception; addition to FIXME-TODO diff -r 119f7d6a3556 -r c1989de100b4 FIXME-TODO --- a/FIXME-TODO Thu Dec 17 17:59:12 2009 +0100 +++ b/FIXME-TODO Sat Dec 19 22:04:34 2009 +0100 @@ -14,14 +14,21 @@ - Handle theorems that include Ball/Bex -- quotient_respects and preserves in a natural form. +- user should be able to give quotient_respects and + preserves theorems in a more natural form. +- the test in the (_, Const _) needs to be fixed Lower Priority ============== - accept partial equvalence relations +- what happens if the original theorem contains bounded + quantifiers? can such theorems be lifted? If not, would + it help if we introduced separate Bex and Ball constants + for quotienting? + - inductions from the datatype package have a strange order of quantifiers in assumptions. diff -r 119f7d6a3556 -r c1989de100b4 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Thu Dec 17 17:59:12 2009 +0100 +++ b/Quot/quotient_def.ML Sat Dec 19 22:04:34 2009 +0100 @@ -3,6 +3,7 @@ sig datatype flag = absF | repF val get_fun: flag -> Proof.context -> typ * typ -> term + val quotient_def: mixfix -> Attrib.binding -> term -> term -> Proof.context -> (term * thm) * local_theory val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> @@ -29,10 +30,13 @@ fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) fun get_fun_aux lthy s fs = - case (maps_lookup (ProofContext.theory_of lthy) s) of - SOME info => list_comb (Const (#mapfun info, dummyT), fs) - | NONE => raise - (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) +let + val thy = ProofContext.theory_of lthy + val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) + val info = maps_lookup thy s handle NotFound => raise exc +in + list_comb (Const (#mapfun info, dummyT), fs) +end fun get_const flag lthy _ qty = (* FIXME: check here that _ and qty are related *) @@ -72,9 +76,9 @@ | (TFree x, TFree x') => if x = x' then mk_identity qty - else raise (LIFT_MATCH "get_fun") - | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") - | _ => raise (LIFT_MATCH "get_fun") + else raise (LIFT_MATCH "get_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") + | _ => raise (LIFT_MATCH "get_fun (default)") (* interface and syntax setup *) @@ -84,6 +88,7 @@ (* - name and attributes of the meta eq *) (* - the new constant including its type *) (* - the rhs of the definition *) + fun quotient_def mx attr lhs rhs lthy = let val Free (lhs_str, lhs_ty) = lhs; @@ -115,9 +120,9 @@ val quotdef_parser = (SpecParse.opt_thm_name ":" -- - OuterParse.term) -- - (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- - OuterParse.term) + OuterParse.term) -- + (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- + OuterParse.term) val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) diff -r 119f7d6a3556 -r c1989de100b4 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Thu Dec 17 17:59:12 2009 +0100 +++ b/Quot/quotient_info.ML Sat Dec 19 22:04:34 2009 +0100 @@ -3,7 +3,7 @@ exception NotFound type maps_info = {mapfun: string, relfun: string} - val maps_lookup: theory -> string -> maps_info option + val maps_lookup: theory -> string -> maps_info (* raises NotFound *) val maps_update_thy: string -> maps_info -> theory -> theory val maps_update: string -> maps_info -> Proof.context -> Proof.context val print_mapsinfo: Proof.context -> unit @@ -18,7 +18,7 @@ type qconsts_info = {qconst: term, rconst: term, def: thm} val qconsts_transfer: morphism -> qconsts_info -> qconsts_info - val qconsts_lookup: theory -> term -> qconsts_info + val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) val qconsts_update_thy: string -> qconsts_info -> theory -> theory val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic val qconsts_dest: theory -> qconsts_info list @@ -50,7 +50,10 @@ val extend = I val merge = Symtab.merge (K true)) -val maps_lookup = Symtab.lookup o MapsData.get +fun maps_lookup thy s = + case (Symtab.lookup (MapsData.get thy) s) of + SOME map_fun => map_fun + | NONE => raise NotFound fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) @@ -188,14 +191,15 @@ | _ => raise NotFound end -(* We omit printing the definition *) fun print_qconstinfo ctxt = let fun prt_qconst {qconst, rconst, def} = Pretty.block (separate (Pretty.brk 1) [Syntax.pretty_term ctxt qconst, Pretty.str ":=", - Syntax.pretty_term ctxt rconst]) + Syntax.pretty_term ctxt rconst, + Pretty.str "as", + Syntax.pretty_term ctxt (prop_of def)]) in QConstsData.get (ProofContext.theory_of ctxt) |> Symtab.dest diff -r 119f7d6a3556 -r c1989de100b4 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Thu Dec 17 17:59:12 2009 +0100 +++ b/Quot/quotient_term.ML Sat Dec 19 22:04:34 2009 +0100 @@ -10,31 +10,32 @@ (* Regularizing an rtrm means: - - Quantifiers over a type that need lifting are replaced + - Quantifiers over types that need lifting are replaced by bounded quantifiers, for example: - All P ===> All (Respects R) P + All P ----> All (Respects R) P - where the relation R is given by the rty and qty; + where the aggregate relation R is given by the rty and qty; - - Abstractions over a type that needs lifting are replaced - by bounded abstractions: + - Abstractions over types that need lifting are replaced + by bounded abstractions, for example: - %x. P ===> Ball (Respects R) %x. P + %x. P ----> Ball (Respects R) %x. P - - Equalities over the type being lifted are replaced by - corresponding equivalence relations: + - Equalities over types that need lifting are replaced by + corresponding equivalence relations, for example: - A = B ===> R A B + A = B ----> R A B or - A = B ===> (R ===> R) A B + A = B ----> (R ===> R) A B for more complicated types of A and B *) -(* builds the relation that is the argument of respects *) +(* builds the aggregate equivalence relation *) +(* that will be the argument of Respects *) fun mk_resp_arg lthy (rty, qty) = let val thy = ProofContext.theory_of lthy @@ -46,8 +47,9 @@ (Type (s, tys), Type (s', tys')) => if s = s' then let - val SOME map_info = maps_lookup thy s - (* FIXME dont return an option, raise an exception *) + val map_info = maps_lookup thy s + handle NotFound => + raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) val args = map (mk_resp_arg lthy) (tys ~~ tys') in list_comb (Const (#relfun map_info, dummyT), args) @@ -88,7 +90,7 @@ (* produces a regularized version of rtrm *) (* *) -(* - the result is still contains dummyT *) +(* - the result still contains dummyTs *) (* *) (* - for regularisation we do not need any *) (* special treatment of bound variables *) @@ -124,14 +126,14 @@ if ty = ty' then rtrm else mk_resp_arg lthy (domain_type ty, domain_type ty') - | (* in this case we check whether the given equivalence relation is correct *) + | (* 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) handle TERM _ => raise exc val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') in - if rel' = rel then rtrm else raise exc + if rel' aconv rel then rtrm else raise exc end | (_, Const _) => @@ -168,10 +170,6 @@ | (t1 $ t2, t1' $ t2') => (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') - | (Free (x, ty), Free (x', ty')) => - (* this case cannot arrise as we start with two fully atomized terms *) - raise (LIFT_MATCH "regularize (frees)") - | (Bound i, Bound i') => if i = i' then rtrm else raise (LIFT_MATCH "regularize (bounds mismatch)") @@ -187,32 +185,31 @@ (* -Injecting of Rep/Abs means: +Injection of Rep/Abs means: For abstractions : - * If the type of the abstraction doesn't need lifting we recurse. - - * If it needs lifting then we add Rep/Abs around the whole term and - check if the bound variable needs lifting. + * If the type of the abstraction needs lifting, then we add Rep/Abs + around the abstraction; otherwise we leave it unchanged. - * If it does we recurse and put Rep/Abs around all occurences - of the variable in the obtained subterm. This in combination - with the Rep/Abs from above will let us change the type of - the abstraction with rewriting. - For applications: - * If the term is Respects applied to anything we leave it unchanged + * If the application involves a bounded quantifier, we recurse on + the second argument. If the application is a bounded abstraction, + we always put an Re/Abs around it (since bounded abstractions + always need lifting). Otherwise we recurse on both arguments. - * If the term needs lifting and the head is a constant that we know - how to lift, we put a Rep/Abs and recurse + For constants: - * If the term needs lifting and the head is a Free applied to subterms - (if it is not applied we treated it in Abs branch) then we - put Rep/Abs and recurse + * If the constant is (op =), we leave it always unchanged. + Otherwise the type of the constant needs lifting, we put + and Rep/Abs around it. - * Otherwise just recurse. + For free variables: + + * We put aRep/Abs around it if the type needs lifting. + + Vars case cannot occur. *) fun mk_repabs lthy (T, T') trm = @@ -269,7 +266,7 @@ else mk_repabs lthy (rty, T') rtrm end - | _ => raise (LIFT_MATCH "injection") + | _ => raise (LIFT_MATCH "injection (default)") end; (* structure *) diff -r 119f7d6a3556 -r c1989de100b4 Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Thu Dec 17 17:59:12 2009 +0100 +++ b/Quot/quotient_typ.ML Sat Dec 19 22:04:34 2009 +0100 @@ -12,7 +12,7 @@ exception LIFT_MATCH of string -(* wrappers for define, note and theorem_i *) +(* wrappers for define, note, Attrib.internal and theorem_i *) fun define (name, mx, rhs) lthy = let val ((rhs, (_ , thm)), lthy') = @@ -28,7 +28,7 @@ (thm', lthy') end -fun internal_attr at = Attrib.internal (K at) +fun intern_attr at = Attrib.internal (K at) fun theorem after_qed goals ctxt = let @@ -117,13 +117,13 @@ (K typedef_quotient_thm_tac) end -(* main function for constructing the quotient type *) +(* main function for constructing a quotient type *) fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = let - (* generates typedef *) + (* generates the typedef *) val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy - (* abs and rep functions *) + (* abs and rep functions from the typedef *) val abs_ty = #abs_type typedef_info val rep_ty = #rep_type typedef_info val abs_name = #Abs_name typedef_info @@ -131,7 +131,7 @@ val abs = Const (abs_name, rep_ty --> abs_ty) val rep = Const (rep_name, abs_ty --> rep_ty) - (* ABS and REP definitions *) + (* more abstract ABS and REP definitions *) val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT ) val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT ) val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) @@ -155,14 +155,14 @@ val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 (* FIXME: varifyT should not be used *) - (* FIXME: the relation needs to be a string, since its type needs *) - (* FIXME: to recalculated in for example REGULARIZE *) + (* FIXME: the relation can be any term, that later maybe needs to be given *) + (* FIXME: a different type (in regularize_trm); how should tis be done? *) in lthy3 |> note (quot_thm_name, quot_thm, []) - ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) - ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add]) + ||>> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) + ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) end