--- a/Quot/QuotMain.thy Thu Jan 14 12:14:35 2010 +0100
+++ b/Quot/QuotMain.thy Thu Jan 14 12:17:39 2010 +0100
@@ -95,6 +95,7 @@
section {* ML setup *}
(* Auxiliary data for the quotient package *)
+
use "quotient_info.ML"
declare [[map "fun" = (fun_map, fun_rel)]]
@@ -147,30 +148,6 @@
use "quotient_tacs.ML"
-(* Atomize infrastructure *)
-(* FIXME/TODO: is this really needed? *)
-(*
-lemma atomize_eqv[atomize]:
- shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-proof
- assume "A \<equiv> B"
- then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
- assume *: "Trueprop A \<equiv> Trueprop B"
- have "A = B"
- proof (cases A)
- case True
- have "A" by fact
- then show "A = B" using * by simp
- next
- case False
- have "\<not>A" by fact
- then show "A = B" using * by auto
- qed
- then show "A \<equiv> B" by (rule eq_reflection)
-qed
-*)
-
section {* Methods / Interface *}
ML {*
--- a/Quot/quotient_def.ML Thu Jan 14 12:14:35 2010 +0100
+++ b/Quot/quotient_def.ML Thu Jan 14 12:17:39 2010 +0100
@@ -51,8 +51,9 @@
(* data storage *)
fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
+ fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
val lthy'' = Local_Theory.declaration true
- (fn phi => qconsts_update_gen trm (qcinfo phi)) lthy'
+ (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
in
((trm, thm), lthy'')
end
--- a/Quot/quotient_info.ML Thu Jan 14 12:14:35 2010 +0100
+++ b/Quot/quotient_info.ML Thu Jan 14 12:17:39 2010 +0100
@@ -19,9 +19,9 @@
type qconsts_info = {qconst: term, rconst: term, def: thm}
val transform_qconsts: morphism -> qconsts_info -> qconsts_info
val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *)
- val qconsts_update_thy: term -> qconsts_info -> theory -> theory
- val qconsts_update_gen: term -> qconsts_info -> Context.generic -> Context.generic
- val qconsts_dest: theory -> qconsts_info list
+ val qconsts_update_thy: string -> qconsts_info -> theory -> theory
+ val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
+ val qconsts_dest: Proof.context -> qconsts_info list
val print_qconstinfo: Proof.context -> unit
val equiv_rules_get: Proof.context -> thm list
@@ -179,39 +179,45 @@
(* info about quotient constants *)
type qconsts_info = {qconst: term, rconst: term, def: thm}
+fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
+
+(* We need to be able to lookup instances of lifted constants,
+ for example given "nat fset" we need to find "'a fset";
+ but overloaded constants share the same name *)
structure QConstsData = Theory_Data
- (type T = qconsts_info Termtab.table
- val empty = Termtab.empty
+ (type T = (qconsts_info list) Symtab.table
+ val empty = Symtab.empty
val extend = I
- val merge = Termtab.merge (K true))
+ 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}
-fun qconsts_update_thy const qcinfo = QConstsData.map (Termtab.update (const, qcinfo))
-fun qconsts_update_gen const qcinfo = Context.mapping (qconsts_update_thy const qcinfo) I
+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
-fun qconsts_dest thy =
- map snd (Termtab.dest (QConstsData.get thy))
+fun qconsts_dest lthy =
+ flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))
-(* FIXME / TODO : better implementation of the lookup datastructure *)
-(* for example symtabs to alist; or tables with string type key *)
fun qconsts_lookup thy t =
let
- val smt = Termtab.dest (QConstsData.get thy);
val (name, qty) = dest_Const t
- fun matches (_, x) =
+ fun matches x =
let
val (name', qty') = dest_Const (#qconst x);
in
name = name' andalso Sign.typ_instance thy (qty, qty')
end
in
- case (find_first matches smt) of
- SOME (_, x) => x
- | _ => raise NotFound
+ case Symtab.lookup (QConstsData.get thy) name of
+ NONE => raise NotFound
+ | SOME l =>
+ (case (find_first matches l) of
+ SOME x => x
+ | NONE => raise NotFound
+ )
end
fun print_qconstinfo ctxt =
@@ -225,8 +231,10 @@
Syntax.pretty_term ctxt (prop_of def)])
in
QConstsData.get (ProofContext.theory_of ctxt)
- |> Termtab.dest
- |> map (prt_qconst o snd)
+ |> Symtab.dest
+ |> map snd
+ |> flat
+ |> map prt_qconst
|> Pretty.big_list "quotient constants:"
|> Pretty.writeln
end
--- a/Quot/quotient_tacs.ML Thu Jan 14 12:14:35 2010 +0100
+++ b/Quot/quotient_tacs.ML Thu Jan 14 12:17:39 2010 +0100
@@ -57,7 +57,7 @@
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
-fun quotient_tac ctxt = SOLVED'
+fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
resolve_tac (quotient_rules_get ctxt)]))
@@ -503,9 +503,7 @@
*)
fun clean_tac lthy =
let
- (* FIXME/TODO produce defs with lthy, like prs and ids *)
- val thy = ProofContext.theory_of lthy;
- val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+ val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy)
(* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
val prs = prs_rules_get lthy
val ids = id_simps_get lthy
--- a/Unused.thy Thu Jan 14 12:14:35 2010 +0100
+++ b/Unused.thy Thu Jan 14 12:17:39 2010 +0100
@@ -7,6 +7,30 @@
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
+lemma atomize_eqv:
+ shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+ assume "A \<equiv> B"
+ then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+ assume *: "Trueprop A \<equiv> Trueprop B"
+ have "A = B"
+ proof (cases A)
+ case True
+ have "A" by fact
+ then show "A = B" using * by simp
+ next
+ case False
+ have "\<not>A" by fact
+ then show "A = B" using * by auto
+ qed
+ then show "A \<equiv> B" by (rule eq_reflection)
+qed
+*)
+
ML {*
fun dest_cbinop t =