# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259839043 -3600
# Node ID 8f1bf5266ebc89dc7dca79f4096fde57e0acdce4
# Parent  76fa93b1fe8b93c95d25d730f903e9f96029a497
Added the definition to quotient constant data.

diff -r 76fa93b1fe8b -r 8f1bf5266ebc FSet.thy
--- a/FSet.thy	Thu Dec 03 11:58:46 2009 +0100
+++ b/FSet.thy	Thu Dec 03 12:17:23 2009 +0100
@@ -481,4 +481,8 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 done
 
+ML {* qconsts_lookup @{theory} "EMPTY" *}
+thm EMPTY_def
+
+
 end
diff -r 76fa93b1fe8b -r 8f1bf5266ebc LFex.thy
--- a/LFex.thy	Thu Dec 03 11:58:46 2009 +0100
+++ b/LFex.thy	Thu Dec 03 12:17:23 2009 +0100
@@ -264,16 +264,20 @@
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
+apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+prefer 2
+apply(tactic {* clean_tac @{context} quot defs 1 *})
+
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *}
 *)
-apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} quot defs 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2  1*})
+ML_prf {* PolyML.profiling 1 *}
+ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
+
+apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
 done
 
 (* Does not work:
diff -r 76fa93b1fe8b -r 8f1bf5266ebc quotient_def.ML
--- a/quotient_def.ML	Thu Dec 03 11:58:46 2009 +0100
+++ b/quotient_def.ML	Thu Dec 03 12:17:23 2009 +0100
@@ -97,7 +97,7 @@
   val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
 
   val qconst_str = Binding.name_of qconst_bname
-  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs}
+  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
                  (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy'
 in
diff -r 76fa93b1fe8b -r 8f1bf5266ebc quotient_info.ML
--- a/quotient_info.ML	Thu Dec 03 11:58:46 2009 +0100
+++ b/quotient_info.ML	Thu Dec 03 12:17:23 2009 +0100
@@ -13,7 +13,7 @@
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
   val quotdata_dest: theory -> quotient_info list
 
-  type qconsts_info = {qconst: term, rconst: term}
+  type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
@@ -118,7 +118,7 @@
 
 
 (* info about quotient constants *)
-type qconsts_info = {qconst: term, rconst: term}
+type qconsts_info = {qconst: term, rconst: term, def: thm}
 
 structure QConstsData = Theory_Data
   (type T = qconsts_info Symtab.table
@@ -126,18 +126,20 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
-fun qconsts_transfer phi {qconst, rconst} =
+fun qconsts_transfer phi {qconst, rconst, def} =
     {qconst = Morphism.term phi qconst,
-     rconst = Morphism.term phi rconst}
+     rconst = Morphism.term phi rconst,
+     def = Morphism.thm phi def}
 
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
 
+(* We don't print the definition *)
 fun print_qconstinfo ctxt =
 let
-  fun prt_qconst {qconst, rconst} = 
+  fun prt_qconst {qconst, rconst, def} =
       Pretty.block (separate (Pretty.brk 1)
           [Syntax.pretty_term ctxt qconst,
            Pretty.str ":=",