# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261432918 -3600
# Node ID d89851ebac9b6b57e40025d4952ba69edea4182e
# Parent  e9e205b904e243779516c3ead5fbbf4694e878b9
cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)

diff -r e9e205b904e2 -r d89851ebac9b Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Dec 21 22:36:31 2009 +0100
+++ b/Quot/quotient_tacs.ML	Mon Dec 21 23:01:58 2009 +0100
@@ -16,16 +16,16 @@
 open Quotient_Term;
 
 
-(* Since HOL_basic_ss is too "big" for us,    *)
-(* we need to set up our own minimal simpset. *)
+(* Since HOL_basic_ss is too "big" for us, we *)
+(* need to set up our own minimal simpset.    *)
 fun  mk_minimal_ss ctxt =
   Simplifier.context ctxt empty_ss
     setsubgoaler asm_simp_tac
     setmksimps (mksimps [])
 
-
+(* various helper fuctions *)
 
-(* various helper functions *)
+(* composition of two theorems, used in map *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
 (* makes sure a subgoal is solved *)
@@ -48,8 +48,6 @@
 end
 
 
-
-
 (* Regularize Tactic *)
 
 fun equiv_tac ctxt =
@@ -74,24 +72,25 @@
   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 
-fun calculate_instance ctxt thm redex R1 R2 =
+(* calculates the instantiations for ball_reg_eqv_range and bex_reg_eqv_range *)
+fun calculate_instance ctxt ball_bex_thm redex R1 R2 =
 let
   val thy = ProofContext.theory_of ctxt
-  val goal = Const (@{const_name "equivp"}, dummyT) $ R2  
-             |> Syntax.check_term ctxt
-             |> HOLogic.mk_Trueprop 
-  val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1)
-  val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
-  val R1c = cterm_of thy R1
-  val thmi = Drule.instantiate' [] [SOME R1c] thm
+  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 = (@{thm eq_reflection} OF [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.eta_contraction_rule (Drule.instantiate inst thmi)
+  val thm2 = Drule.instantiate inst thmi
 in
   SOME thm2
 end
 handle _ => NONE
 (* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
 
+
 fun ball_bex_range_simproc ss redex =
 let
   val ctxt = Simplifier.the_context ss
@@ -116,10 +115,10 @@
 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 
-fun solve_quotient_assum ctxt thm =
+fun solve_quotient_assm ctxt thm =
   case Seq.pull (quotient_tac ctxt 1 thm) of
     SOME (t, _) => t
-  | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing"
+  | _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing"
 
 
 (* 0. preliminary simplification step according to *)
@@ -458,7 +457,7 @@
        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
-       val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)]
+       val te = @{thm eq_reflection} OF [solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)]
        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
        val make_inst = if ty_c = ty_d then make_inst_id else make_inst
        val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)