--- 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 "\<exists>!!"
--- 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 \<times> 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 \<Rightarrow> 'a list"},
@{typ "('a fset) fset \<Rightarrow> 'a fset"})
*}
--- 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'
--- 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 *)
--- 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