handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
authorblanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 423426babd86a54a4
parent 42341 5a00af7f4978
child 42343 118cc349de35
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
src/HOL/Metis_Examples/Clausify.thy
src/HOL/Tools/Metis/metis_reconstruct.ML
     1.1 --- a/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -8,15 +8,6 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -text {* Outstanding issues *}
     1.8 -
     1.9 -lemma ex_tl: "EX ys. tl ys = xs"
    1.10 -using tl.simps(2) by fast
    1.11 -
    1.12 -lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
    1.13 -using [[metis_new_skolemizer = false]] (* FAILS with "= true" *)
    1.14 -by (metis ex_tl)
    1.15 -
    1.16  text {* Definitional CNF for goal *}
    1.17  
    1.18  (* FIXME: shouldn't need this *)
    1.19 @@ -52,7 +43,7 @@
    1.20  
    1.21  lemma
    1.22    fixes x :: real
    1.23 -  assumes fn_le: "!!n. f n \<le> x" and 1: "f----> lim f"
    1.24 +  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
    1.25    shows "lim f \<le> x"
    1.26  by (metis 1 LIMSEQ_le_const2 fn_le)
    1.27  
    1.28 @@ -71,7 +62,13 @@
    1.29  
    1.30  lemma
    1.31    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    1.32 -   (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.33 +   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.34  by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
    1.35  
    1.36 +lemma ex_tl: "EX ys. tl ys = xs"
    1.37 +using tl.simps(2) by fast
    1.38 +
    1.39 +lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
    1.40 +by (metis ex_tl)
    1.41 +
    1.42  end
     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     2.3 @@ -611,7 +611,50 @@
     2.4                    (fn () => "=============================================")
     2.5      in (fol_th, th) :: thpairs end
     2.6  
     2.7 -fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
     2.8 +(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
     2.9 +   one of the premises. Unfortunately, this sometimes yields "Variable
    2.10 +   ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
    2.11 +   variables before applying "assume_tac". Typical constraints are of the form
    2.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,
    2.13 +   where the nonvariables are goal parameters. *)
    2.14 +fun unify_first_prem_with_concl thy i th =
    2.15 +  let
    2.16 +    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
    2.17 +    val prem = goal |> Logic.strip_assums_hyp |> hd
    2.18 +    val concl = goal |> Logic.strip_assums_concl
    2.19 +    fun pair_untyped_aconv (t1, t2) (u1, u2) =
    2.20 +      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    2.21 +    fun add_terms tp inst =
    2.22 +      if exists (pair_untyped_aconv tp) inst then inst
    2.23 +      else tp :: map (apsnd (subst_atomic [tp])) inst
    2.24 +    fun is_flex t =
    2.25 +      case strip_comb t of
    2.26 +        (Var _, args) => forall is_Bound args
    2.27 +      | _ => false
    2.28 +    fun unify_flex flex rigid =
    2.29 +      case strip_comb flex of
    2.30 +        (Var (z as (_, T)), args) =>
    2.31 +        add_terms (Var z,
    2.32 +          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
    2.33 +      | _ => I
    2.34 +    fun unify_potential_flex comb atom =
    2.35 +      if is_flex comb then unify_flex comb atom
    2.36 +      else if is_Var atom then add_terms (atom, comb)
    2.37 +      else I
    2.38 +    fun unify_terms (t, u) =
    2.39 +      case (t, u) of
    2.40 +        (t1 $ t2, u1 $ u2) =>
    2.41 +        if is_flex t then unify_flex t u
    2.42 +        else if is_flex u then unify_flex u t
    2.43 +        else fold unify_terms [(t1, u1), (t2, u2)]
    2.44 +      | (_ $ _, _) => unify_potential_flex t u
    2.45 +      | (_, _ $ _) => unify_potential_flex u t
    2.46 +      | (Var _, _) => add_terms (t, u)
    2.47 +      | (_, Var _) => add_terms (u, t)
    2.48 +      | _ => I
    2.49 +    val t_inst = [] |> unify_terms (prem, concl)
    2.50 +                    |> map (pairself (cterm_of thy))
    2.51 +  in th |> cterm_instantiate t_inst end
    2.52  
    2.53  val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
    2.54  
    2.55 @@ -663,9 +706,7 @@
    2.56                          tyenv []
    2.57            val t_inst =
    2.58              [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
    2.59 -        in
    2.60 -          th |> instantiate (ty_inst, t_inst)
    2.61 -        end
    2.62 +        in th |> instantiate (ty_inst, t_inst) end
    2.63        | _ => raise Fail "expected a single non-zapped, non-Metis Var"
    2.64    in
    2.65      (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
    2.66 @@ -841,6 +882,7 @@
    2.67                THEN ALLGOALS (fn i =>
    2.68                         rtac @{thm Meson.skolem_COMBK_I} i
    2.69                         THEN rotate_tac (rotation_for_subgoal i) i
    2.70 +                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    2.71                         THEN assume_tac i
    2.72                         THEN flexflex_tac)))
    2.73        handle ERROR _ =>