--- a/UnusedQuotMain.thy	Tue Dec 01 12:16:45 2009 +0100
+++ b/UnusedQuotMain.thy	Tue Dec 01 14:04:00 2009 +0100
@@ -3,6 +3,51 @@
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 
 
+section {*  Infrastructure about definitions *}
+
+(* Does the same as 'subst' in a given theorem *)
+ML {*
+fun eqsubst_thm ctxt thms thm =
+  let
+    val goalstate = Goal.init (Thm.cprop_of thm)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_thm"
+    | SOME th => cprem_of th 1
+    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+    val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
+  in
+    @{thm equal_elim_rule1} OF [rt, thm]
+  end
+*}
+
+(* expects atomized definitions *)
+ML {*
+fun add_lower_defs_aux lthy thm =
+  let
+    val e1 = @{thm fun_cong} OF [thm];
+    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
+    val g = simp_ids f
+  in
+    (simp_ids thm) :: (add_lower_defs_aux lthy g)
+  end
+  handle _ => [simp_ids thm]
+*}
+
+ML {*
+fun add_lower_defs lthy def =
+  let
+    val def_pre_sym = symmetric def
+    val def_atom = atomize_thm def_pre_sym
+    val defs_all = add_lower_defs_aux lthy def_atom
+  in
+    map Thm.varifyT defs_all
+  end
+*}
+
+
+
 ML {*
 fun repeat_eqsubst_thm ctxt thms thm =
   repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)