# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261463289 -3600
# Node ID b2231990b059e24256dfdc62c0fa7ccfff287f6f
# Parent  2d21fd8114af6b697e0f10c2aa8edec6aa8f26e9
simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed

diff -r 2d21fd8114af -r b2231990b059 Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Mon Dec 21 23:13:40 2009 +0100
+++ b/Quot/Examples/LFex.thy	Tue Dec 22 07:28:09 2009 +0100
@@ -277,6 +277,7 @@
 using a0 a1 a2 a3 a4 a5 a6 a7 a8
 *)
 
+
 lemma "\<lbrakk>P TYP;
   \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);
   \<And>id. Q (TCONST id);
diff -r 2d21fd8114af -r b2231990b059 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Dec 21 23:13:40 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 07:28:09 2009 +0100
@@ -56,6 +56,13 @@
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
+fun solve_equiv_assm ctxt thm =
+  case Seq.pull (equiv_tac ctxt 1 thm) of
+    SOME (t, _) => t
+  | _ => error "solve_equiv_assm failed."
+
+
+
 fun prep_trm thy (x, (T, t)) =
   (cterm_of thy (Var (x, T)), cterm_of thy t)
 
@@ -72,23 +79,26 @@
   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 
-(* calculates the instantiations for ball_reg_eqv_range and bex_reg_eqv_range *)
+(* calculates the instantiations for te lemmas *)
+(* ball_reg_eqv_range and bex_reg_eqv_range    *)
 fun calculate_instance ctxt ball_bex_thm redex R1 R2 =
 let
+  fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
   val thy = ProofContext.theory_of ctxt
-  val eqv_ty = fastype_of R2 --> HOLogic.boolT 
-  val eqv_goal = HOLogic.mk_Trueprop 
-                     (Const (@{const_name "equivp"}, eqv_ty) $ R2)  
-  val eqv_prem = Goal.prove ctxt [] [] eqv_goal (fn _ => equiv_tac ctxt 1)
-  val thm = ball_bex_thm OF [eqv_prem]
-  val thmi = Drule.instantiate' [] [SOME (cterm_of thy R1)] thm
-  val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
-  val thm2 = Drule.instantiate inst thmi
+  val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
+  val trm_inst1 = map (SOME o cterm_of thy) [R2, R1]
+  val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm
+  val inst2 = matching_prs thy (get_lhs thm') redex
+  val thm'' =  Drule.instantiate inst2 thm'
 in
-  SOME thm2
+  SOME thm''
 end
-handle _ => NONE
-(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
+handle _ => NONE      
+(* FIXME/TODO: !!!CLEVER CODE!!!                                 *)
+(* FIXME/TODO: What is the place where the exception is raised,  *)
+(* FIXME/TODO: and which exception is it?                        *)
+(* FIXME/TODO: Can one not find out from the types of R1 or R2,  *)
+(* FIXME/TODO: or from their form, when NONE should be returned? *)
 
 
 fun ball_bex_range_simproc ss redex =