# HG changeset patch # User Christian Urban # Date 1263467859 -3600 # Node ID f14e41e9b08faafcc7ebb182da744036c15cdd69 # Parent 2605ea41bbddd384bd089fd547ddcca569996bad# Parent 4163fe3dbf8c976d75bf0bd9076b8654eac55987 merged diff -r 2605ea41bbdd -r f14e41e9b08f Quot/QuotMain.thy --- 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 \ Trueprop B) \ (A \ B)" -proof - assume "A \ B" - then show "Trueprop A \ Trueprop B" by unfold -next - assume *: "Trueprop A \ 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 "\A" by fact - then show "A = B" using * by auto - qed - then show "A \ B" by (rule eq_reflection) -qed -*) - section {* Methods / Interface *} ML {* diff -r 2605ea41bbdd -r f14e41e9b08f Quot/quotient_def.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 diff -r 2605ea41bbdd -r f14e41e9b08f Quot/quotient_info.ML --- 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 diff -r 2605ea41bbdd -r f14e41e9b08f Quot/quotient_tacs.ML --- 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 diff -r 2605ea41bbdd -r f14e41e9b08f Unused.thy --- 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 \ Trueprop B) \ (A \ B)" +proof + assume "A \ B" + then show "Trueprop A \ Trueprop B" by unfold +next + assume *: "Trueprop A \ 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 "\A" by fact + then show "A = B" using * by auto + qed + then show "A \ B" by (rule eq_reflection) +qed +*) + ML {* fun dest_cbinop t =