# HG changeset patch # User Cezary Kaliszyk # Date 1265725695 -3600 # Node ID 551eacf071d731700a0e6e8f90ec5487769c7deb # Parent 139b257e10d2bf5f637eff3bbc3a256f2691c339 More indentation, names and todo cleaning in the quotient package diff -r 139b257e10d2 -r 551eacf071d7 FIXME-TODO --- a/FIXME-TODO Tue Feb 09 14:32:37 2010 +0100 +++ b/FIXME-TODO Tue Feb 09 15:28:15 2010 +0100 @@ -11,9 +11,6 @@ - Ask Markus how the files Quot* should be named. (There is a HOL/Library/Quotient.thy --- seems to be an example. *) -- Is Bexeq the right name? - - - If the constant definition gives the wrong definition term, one gets a cryptic message about absrep_fun @@ -37,8 +34,6 @@ - inductions from the datatype package have a strange order of quantifiers in assumptions. -- wrapper for lifting ... to be used as an attribute - - find clean ways how to write down the "mathematical" procedure for a possible submission (Peter submitted his work only to TPHOLs 2005...we would have to go @@ -65,5 +60,3 @@ That means "qconst :: qty" is not read as a term, but as two entities. - -- Add syntax for Bexeq, for example "\!!" diff -r 139b257e10d2 -r 551eacf071d7 Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Tue Feb 09 14:32:37 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Tue Feb 09 15:28:15 2010 +0100 @@ -105,62 +105,62 @@ by (auto simp add: equivp_def expand_fun_eq) ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "nat \ nat"}, @{typ "myint"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a * 'a) list"}, @{typ "'a foo"}) *} ML {* -test_funs repF @{context} +test_funs RepF @{context} (@{typ "(('a * 'a) list * 'b)"}, @{typ "('a foo * 'b)"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "(('a list) * int) list"}, @{typ "('a fset) bar"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a list)"}, @{typ "('a fset)"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "((nat * nat) list) list"}, @{typ "((myint) fset) fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "(('a * 'a) list) list"}, @{typ "(('a * 'a) fset) fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "(nat * nat) list"}, @{typ "myint fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a list) list \ 'a list"}, @{typ "('a fset) fset \ 'a fset"}) *} diff -r 139b257e10d2 -r 551eacf071d7 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Tue Feb 09 14:32:37 2010 +0100 +++ b/Quot/quotient_def.ML Tue Feb 09 15:28:15 2010 +0100 @@ -53,7 +53,7 @@ val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" val qconst_bname = Binding.name lhs_str - val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs + val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) val (_, prop') = LocalDefs.cert_def lthy prop val (_, newrhs) = Primitive_Defs.abs_def prop' diff -r 139b257e10d2 -r 551eacf071d7 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Tue Feb 09 14:32:37 2010 +0100 +++ b/Quot/quotient_info.ML Tue Feb 09 15:28:15 2010 +0100 @@ -116,23 +116,23 @@ end val maps_attr_parser = - Args.context -- Scan.lift - ((Args.name --| OuterParse.$$$ "=") -- - (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- - Args.name --| OuterParse.$$$ ")")) + Args.context -- Scan.lift + ((Args.name --| OuterParse.$$$ "=") -- + (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- + Args.name --| OuterParse.$$$ ")")) val _ = Context.>> (Context.map_theory - (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) - "declaration of map information")) + (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) + "declaration of map information")) fun print_mapsinfo ctxt = let fun prt_map (ty_name, {mapfun, relmap}) = - Pretty.block (Library.separate (Pretty.brk 2) - (map Pretty.str - ["type:", ty_name, - "map:", mapfun, - "relation map:", relmap])) + Pretty.block (Library.separate (Pretty.brk 2) + (map Pretty.str + ["type:", ty_name, + "map:", mapfun, + "relation map:", relmap])) in MapsData.get (ProofContext.theory_of ctxt) |> Symtab.dest @@ -152,10 +152,10 @@ val merge = Symtab.merge (K true)) fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = - {qtyp = Morphism.typ phi qtyp, - rtyp = Morphism.typ phi rtyp, - equiv_rel = Morphism.term phi equiv_rel, - equiv_thm = Morphism.thm phi equiv_thm} + {qtyp = Morphism.typ phi qtyp, + rtyp = Morphism.typ phi rtyp, + equiv_rel = Morphism.term phi equiv_rel, + equiv_thm = Morphism.thm phi equiv_thm} fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str @@ -172,16 +172,16 @@ fun print_quotinfo ctxt = let - fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = - Pretty.block (Library.separate (Pretty.brk 2) - [Pretty.str "quotient type:", - Syntax.pretty_typ ctxt qtyp, - Pretty.str "raw type:", - Syntax.pretty_typ ctxt rtyp, - Pretty.str "relation:", - Syntax.pretty_term ctxt equiv_rel, - Pretty.str "equiv. thm:", - Syntax.pretty_term ctxt (prop_of equiv_thm)]) + fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = + Pretty.block (Library.separate (Pretty.brk 2) + [Pretty.str "quotient type:", + Syntax.pretty_typ ctxt qtyp, + Pretty.str "raw type:", + Syntax.pretty_typ ctxt rtyp, + Pretty.str "relation:", + Syntax.pretty_term ctxt equiv_rel, + Pretty.str "equiv. thm:", + Syntax.pretty_term ctxt (prop_of equiv_thm)]) in QuotData.get (ProofContext.theory_of ctxt) |> Symtab.dest @@ -206,9 +206,9 @@ val merge = Symtab.merge_list qconsts_info_eq) fun transform_qconsts phi {qconst, rconst, def} = - {qconst = Morphism.term phi qconst, - rconst = Morphism.term phi rconst, - def = Morphism.thm phi def} + {qconst = Morphism.term phi qconst, + rconst = Morphism.term phi rconst, + def = Morphism.thm phi def} fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I @@ -237,12 +237,12 @@ 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, - Pretty.str "as", - Syntax.pretty_term ctxt (prop_of def)]) + Pretty.block (separate (Pretty.brk 1) + [Syntax.pretty_term ctxt qconst, + Pretty.str ":=", + Syntax.pretty_term ctxt rconst, + Pretty.str "as", + Syntax.pretty_term ctxt (prop_of def)]) in QConstsData.get (ProofContext.theory_of ctxt) |> Symtab.dest @@ -253,9 +253,6 @@ |> Pretty.writeln end -(* FIXME/TODO: check the various lemmas conform *) -(* with the required shape *) - (* equivalence relation theorems *) structure EquivRules = Named_Thms (val name = "quot_equiv" @@ -297,22 +294,22 @@ (* setup of the theorem lists *) val _ = Context.>> (Context.map_theory - (EquivRules.setup #> - RspRules.setup #> - PrsRules.setup #> - IdSimps.setup #> - QuotientRules.setup)) + (EquivRules.setup #> + RspRules.setup #> + PrsRules.setup #> + IdSimps.setup #> + QuotientRules.setup)) (* setup of the printing commands *) -fun improper_command (pp_fn, cmd_name, descr_str) = - OuterSyntax.improper_command cmd_name descr_str +fun improper_command (pp_fn, cmd_name, descr_str) = + OuterSyntax.improper_command cmd_name descr_str OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) -val _ = map improper_command - [(print_mapsinfo, "print_maps", "prints out all map functions"), - (print_quotinfo, "print_quotients", "prints out all quotients"), - (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] +val _ = map improper_command + [(print_mapsinfo, "print_maps", "prints out all map functions"), + (print_quotinfo, "print_quotients", "prints out all quotients"), + (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] end; (* structure *) diff -r 139b257e10d2 -r 551eacf071d7 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Tue Feb 09 14:32:37 2010 +0100 +++ b/Quot/quotient_term.ML Tue Feb 09 15:28:15 2010 +0100 @@ -9,7 +9,7 @@ sig exception LIFT_MATCH of string - datatype flag = absF | repF + datatype flag = AbsF | RepF val absrep_fun: flag -> Proof.context -> typ * typ -> term val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term @@ -41,15 +41,15 @@ (*** Aggregate Rep/Abs Function ***) -(* The flag repF is for types in negative position; absF is for types +(* The flag RepF is for types in negative position; AbsF is for types in positive position. Because of this, function types need to be treated specially, since there the polarity changes. *) -datatype flag = absF | repF +datatype flag = AbsF | RepF -fun negF absF = repF - | negF repF = absF +fun negF AbsF = RepF + | negF RepF = AbsF fun is_identity (Const (@{const_name "id"}, _)) = true | is_identity _ = false @@ -58,8 +58,8 @@ fun mk_fun_compose flag (trm1, trm2) = case flag of - absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 - | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 + AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 + | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 fun get_mapfun ctxt s = let @@ -134,8 +134,8 @@ val qty_name = Long_Name.base_name qty_str in case flag of - absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) - | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) + AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) + | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) end (* Lets Nitpick represent elements of quotient types as elements of the raw type *) @@ -620,7 +620,7 @@ *) fun mk_repabs ctxt (T, T') trm = - absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm) + absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) fun inj_repabs_err ctxt msg rtrm qtrm = let