1.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Oct 06 03:49:36 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Oct 06 11:16:40 2006 +0200
     1.3 @@ -55,12 +55,17 @@
     1.4    extensionality in proofs.
     1.5    FIXME!  Store in theory data!!*)
     1.6  
     1.7 +(*Populate the abstraction cache with common combinators.*)
     1.8  fun seed th net =
     1.9    let val (_,ct) = Thm.dest_abs NONE (Drule.crhs_of th)
    1.10 -  in  Net.insert_term eq_thm (term_of ct, th) net end;
    1.11 +      val t = Logic.legacy_varify (term_of ct)
    1.12 +  in  Net.insert_term eq_thm (t, th) net end;
    1.13    
    1.14  val abstraction_cache = ref 
    1.15 -  (seed (thm"COMBI1") (seed (thm"COMBB1") (seed (thm"COMBK1") Net.empty)));
    1.16 +      (seed (thm"Reconstruction.I_simp") 
    1.17 +       (seed (thm"Reconstruction.B_simp") 
    1.18 +	(seed (thm"Reconstruction.K_simp") Net.empty)));
    1.19 +
    1.20  
    1.21  (**** Transformation of Elimination Rules into First-Order Formulas****)
    1.22  
    1.23 @@ -286,13 +291,11 @@
    1.24  val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
    1.25  
    1.26  (*Does an existing abstraction definition have an RHS that matches the one we need now?*)
    1.27 -fun match_rhs thy0 t th =
    1.28 +fun match_rhs t th =
    1.29    let val thy = theory_of_thm th
    1.30        val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
    1.31                                            " against\n" ^ string_of_thm th) else ();
    1.32 -      val (tyenv,tenv) = if Context.joinable (thy0,thy) then
    1.33 -                            Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
    1.34 -                         else raise Pattern.MATCH
    1.35 +      val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
    1.36        val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
    1.37        val ct_pairs = if forall lambda_free (map #2 term_insts) then
    1.38                           map (pairself (cterm_of thy)) term_insts
    1.39 @@ -325,10 +328,9 @@
    1.40                  val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
    1.41                  val rhs = list_abs_free (map dest_Free args, abs_v_u)
    1.42                        (*Forms a lambda-abstraction over the formal parameters*)
    1.43 -                val v_rhs = Logic.varify rhs
    1.44                  val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
    1.45                  val (ax,ax',thy) =
    1.46 -                 case List.mapPartial (match_rhs thy abs_v_u) (Net.match_term (!abstraction_cache) u')
    1.47 +                 case List.mapPartial (match_rhs abs_v_u) (Net.match_term (!abstraction_cache) u')
    1.48                          of
    1.49                       (ax,ax')::_ => 
    1.50                         (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
    1.51 @@ -351,7 +353,7 @@
    1.52                            val ax = get_axiom thy cdef |> freeze_thm
    1.53                                       |> mk_object_eq |> strip_lambdas (length args)
    1.54                                       |> mk_meta_eq |> Meson.generalize
    1.55 -                          val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
    1.56 +                          val (_,ax') = Option.valOf (match_rhs abs_v_u ax)
    1.57                            val _ = if !trace_abs then 
    1.58                                      (warning ("Declaring: " ^ string_of_thm ax);
    1.59                                       warning ("Instance: " ^ string_of_thm ax')) 
    1.60 @@ -403,7 +405,7 @@
    1.61                        (*Forms a lambda-abstraction over the formal parameters*)
    1.62                  val rhs = term_of crhs
    1.63                  val (ax,ax') =
    1.64 -                 case List.mapPartial (match_rhs thy abs_v_u) 
    1.65 +                 case List.mapPartial (match_rhs abs_v_u) 
    1.66                          (Net.match_term (!abstraction_cache) u') of
    1.67                       (ax,ax')::_ => 
    1.68                         (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
    1.69 @@ -415,7 +417,7 @@
    1.70                            val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
    1.71                                       |> mk_object_eq |> strip_lambdas (length args)
    1.72                                       |> mk_meta_eq |> Meson.generalize
    1.73 -                          val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
    1.74 +                          val (_,ax') = Option.valOf (match_rhs abs_v_u ax)
    1.75                            val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
    1.76                                      (!abstraction_cache)
    1.77                              handle Net.INSERT =>
    1.78 @@ -645,8 +647,11 @@
    1.79  fun skolem_cache (name,th) thy =
    1.80    let val prop = Thm.prop_of th
    1.81    in
    1.82 -      if lambda_free prop (*orelse monomorphic prop*)
    1.83 -      then thy    (*monomorphic theorems can be Skolemized on demand*)
    1.84 +      if lambda_free prop 
    1.85 +         (*orelse monomorphic prop? Monomorphic theorems can be Skolemized on demand,
    1.86 +           but there are problems with re-use of abstraction functions if we don't
    1.87 +           do them now, even for monomorphic theorems.*)
    1.88 +      then thy  
    1.89        else #2 (skolem_cache_thm (name,th) thy)
    1.90    end;
    1.91