src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 42342 6babd86a54a4
parent 42341 5a00af7f4978
child 42344 4a58173ffb99
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -611,7 +611,50 @@
     1.4                    (fn () => "=============================================")
     1.5      in (fol_th, th) :: thpairs end
     1.6  
     1.7 -fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
     1.8 +(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
     1.9 +   one of the premises. Unfortunately, this sometimes yields "Variable
    1.10 +   ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
    1.11 +   variables before applying "assume_tac". Typical constraints are of the form
    1.12 +     ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
    1.13 +   where the nonvariables are goal parameters. *)
    1.14 +fun unify_first_prem_with_concl thy i th =
    1.15 +  let
    1.16 +    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
    1.17 +    val prem = goal |> Logic.strip_assums_hyp |> hd
    1.18 +    val concl = goal |> Logic.strip_assums_concl
    1.19 +    fun pair_untyped_aconv (t1, t2) (u1, u2) =
    1.20 +      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    1.21 +    fun add_terms tp inst =
    1.22 +      if exists (pair_untyped_aconv tp) inst then inst
    1.23 +      else tp :: map (apsnd (subst_atomic [tp])) inst
    1.24 +    fun is_flex t =
    1.25 +      case strip_comb t of
    1.26 +        (Var _, args) => forall is_Bound args
    1.27 +      | _ => false
    1.28 +    fun unify_flex flex rigid =
    1.29 +      case strip_comb flex of
    1.30 +        (Var (z as (_, T)), args) =>
    1.31 +        add_terms (Var z,
    1.32 +          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
    1.33 +      | _ => I
    1.34 +    fun unify_potential_flex comb atom =
    1.35 +      if is_flex comb then unify_flex comb atom
    1.36 +      else if is_Var atom then add_terms (atom, comb)
    1.37 +      else I
    1.38 +    fun unify_terms (t, u) =
    1.39 +      case (t, u) of
    1.40 +        (t1 $ t2, u1 $ u2) =>
    1.41 +        if is_flex t then unify_flex t u
    1.42 +        else if is_flex u then unify_flex u t
    1.43 +        else fold unify_terms [(t1, u1), (t2, u2)]
    1.44 +      | (_ $ _, _) => unify_potential_flex t u
    1.45 +      | (_, _ $ _) => unify_potential_flex u t
    1.46 +      | (Var _, _) => add_terms (t, u)
    1.47 +      | (_, Var _) => add_terms (u, t)
    1.48 +      | _ => I
    1.49 +    val t_inst = [] |> unify_terms (prem, concl)
    1.50 +                    |> map (pairself (cterm_of thy))
    1.51 +  in th |> cterm_instantiate t_inst end
    1.52  
    1.53  val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
    1.54  
    1.55 @@ -663,9 +706,7 @@
    1.56                          tyenv []
    1.57            val t_inst =
    1.58              [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
    1.59 -        in
    1.60 -          th |> instantiate (ty_inst, t_inst)
    1.61 -        end
    1.62 +        in th |> instantiate (ty_inst, t_inst) end
    1.63        | _ => raise Fail "expected a single non-zapped, non-Metis Var"
    1.64    in
    1.65      (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
    1.66 @@ -841,6 +882,7 @@
    1.67                THEN ALLGOALS (fn i =>
    1.68                         rtac @{thm Meson.skolem_COMBK_I} i
    1.69                         THEN rotate_tac (rotation_for_subgoal i) i
    1.70 +                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    1.71                         THEN assume_tac i
    1.72                         THEN flexflex_tac)))
    1.73        handle ERROR _ =>