# HG changeset patch # User Christian Urban # Date 1256422480 -7200 # Node ID c7eff9882bd8236662f35ff608054c83e9042826 # Parent 3e53081ad53a9b369df1ab1ac3331ff10e3e1a6f added data-storage about the quotients diff -r 3e53081ad53a -r c7eff9882bd8 QuotMain.thy --- a/QuotMain.thy Sat Oct 24 22:52:23 2009 +0200 +++ b/QuotMain.thy Sun Oct 25 00:14:40 2009 +0200 @@ -164,15 +164,6 @@ 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} *} - ML {* val no_vars = Thm.rule_attribute (fn context => fn th => let diff -r 3e53081ad53a -r c7eff9882bd8 quotient.ML --- a/quotient.ML Sat Oct 24 22:52:23 2009 +0200 +++ b/quotient.ML Sun Oct 25 00:14:40 2009 +0200 @@ -45,10 +45,12 @@ fun merge _ = (op @)) val quotdata_lookup = QuotData.get + 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 quotdata_update (qty, rty, rel) = + ProofContext.theory (quotdata_update_thy (qty, rty, rel)) fun print_quotdata ctxt = let @@ -179,9 +181,6 @@ val abs = Const (abs_name, rep_ty --> abs_ty) val rep = Const (rep_name, abs_ty --> rep_ty) - (* storing the quot-info *) - (*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 ) val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) @@ -201,14 +200,18 @@ val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name + + (* storing the quot-info *) + val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 + (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) - val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2; + val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; val eqn1i = Thm.prop_of (symmetric eqn1pre) - val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3; + val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4; val eqn2i = Thm.prop_of (symmetric eqn2pre) - val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4)); + val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5)); val exp_term = Morphism.term exp_morphism; val exp = Morphism.thm exp_morphism; @@ -219,14 +222,14 @@ val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] in - lthy4 + lthy5 |> note (quot_thm_name, quot_thm) ||>> note (quotient_thm_name, quotient_thm) ||> LocalTheory.theory (fn thy => let val global_eqns = map exp_term [eqn2i, eqn1i]; (* Not sure if the following context should not be used *) - val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; + val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5; val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) end