# HG changeset patch # User cek@localhost.localdomain # Date 1256366054 -7200 # Node ID 22cd68da9ae4cba3ba1553c3c508a93e7ba649f9 # Parent ae83e5b6b141ff10c50a8b8b8771023cb21c0ac1# Parent c1e76f09db70e1712f8bde5d52406c9be200f25f Undid wrong merge diff -r c1e76f09db70 -r 22cd68da9ae4 QuotMain.thy --- a/QuotMain.thy Sat Oct 24 08:24:26 2009 +0200 +++ b/QuotMain.thy Sat Oct 24 08:34:14 2009 +0200 @@ -3,8 +3,16 @@ uses ("quotient.ML") begin -ML {* Pretty.writeln *} -ML {* LocalTheory.theory_result *} +definition + EQ_TRUE +where + "EQ_TRUE X \ (X = True)" + +lemma test: "EQ_TRUE ?X" + unfolding EQ_TRUE_def + by (rule refl) + +thm test locale QUOT_TYPE = fixes R :: "'a \ 'a \ bool" @@ -150,12 +158,12 @@ use "quotient.ML" (* mapfuns for some standard types *) -setup {* - maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> - maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> - maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} -*} +ML {* quotdata_lookup @{theory} *} +setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*} +ML {* quotdata_lookup @{theory} *} + +ML {* print_quotdata @{context} *} ML {* maps_lookup @{theory} @{type_name list} *} @@ -208,8 +216,10 @@ (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) end - fun get_const absF = (Const ("FSet.ABS_" ^ qty_name, rty --> qty), (rty, qty)) - | get_const repF = (Const ("FSet.REP_" ^ qty_name, qty --> rty), (qty, rty)) + val thy = ProofContext.theory_of lthy + + fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) + | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) fun mk_identity ty = Abs ("", ty, Bound 0) diff -r c1e76f09db70 -r 22cd68da9ae4 quotient.ML --- a/quotient.ML Sat Oct 24 08:24:26 2009 +0200 +++ b/quotient.ML Sat Oct 24 08:34:14 2009 +0200 @@ -1,6 +1,7 @@ signature QUOTIENT = sig type maps_info = {mapfun: string, relfun: string} + type quotient_info = {qtyp: typ, rtyp: typ, rel: term} val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state 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 @@ -8,6 +9,9 @@ val maps_lookup: theory -> string -> maps_info option val maps_update: string -> maps_info -> theory -> theory val print_quotdata: Proof.context -> unit + val quotdata_lookup: theory -> quotient_info list + val quotdata_update_thy: (typ * typ * term) -> theory -> theory + val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context end; structure Quotient: QUOTIENT = @@ -41,9 +45,11 @@ fun merge _ = (op @)) val quotdata_lookup = QuotData.get -fun quotdata_update (qty, rty, rel) = +fun quotdata_update_thy (qty, rty, rel) = QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) +fun quotdata_update (qty, rty, rel) = ProofContext.theory (quotdata_update_thy (qty, rty, rel)) + fun print_quotdata ctxt = let val quots = QuotData.get (ProofContext.theory_of ctxt) @@ -174,7 +180,7 @@ val rep = Const (rep_name, abs_ty --> rep_ty) (* storing the quot-info *) - val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy) + (*val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)*) (* ABS and REP definitions *) val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) @@ -211,11 +217,7 @@ val mthdt = Method.Basic (fn _ => mthd) val bymt = Proof.global_terminal_proof (mthdt, NONE) val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), - Expression.Named [ - ("R", rel), - ("Abs", abs), - ("Rep", rep) - ]))] + Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] in lthy4 |> note (quot_thm_name, quot_thm)