src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 40261 7a02144874f3
parent 40259 c0e34371c2e2
child 40264 b91e2e16d994
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -628,7 +628,14 @@
     1.4          (case find_index (fn (s', _) => s' = s) params of
     1.5             ~1 => t
     1.6           | j => Bound j)
     1.7 -      | repair (t $ u) = repair t $ repair u
     1.8 +      | repair (t $ u) =
     1.9 +        (case (repair t, repair u) of
    1.10 +           (t as Bound j, u as Bound k) =>
    1.11 +           (* This is a rather subtle trick to repair the discrepancy between
    1.12 +              the fully skolemized term that MESON gives us (where existentials
    1.13 +              were pulled out) and the reality. *)
    1.14 +           if k > j then t else t $ u
    1.15 +         | (t, u) => t $ u)
    1.16        | repair t = t
    1.17      val t' = t |> repair |> fold (curry absdummy) (map snd params)
    1.18      fun do_instantiate th =
    1.19 @@ -641,24 +648,32 @@
    1.20       THEN PRIMITIVE do_instantiate) st
    1.21    end
    1.22  
    1.23 +fun fix_exists_tac thy t =
    1.24 +  etac @{thm exE}
    1.25 +  THEN' rename_tac [t |> dest_Var |> fst |> fst]
    1.26 +
    1.27 +fun release_quantifier_tac thy (skolem, t) =
    1.28 +  (if skolem then fix_exists_tac else instantiate_forall_tac) thy t
    1.29 +
    1.30  fun release_clusters_tac _ _ _ [] = K all_tac
    1.31    | release_clusters_tac thy ax_counts substs
    1.32                           ((ax_no, cluster_no) :: clusters) =
    1.33      let
    1.34 -      fun in_right_cluster s =
    1.35 -        (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
    1.36 -        = cluster_no
    1.37 +      val cluster_of_var =
    1.38 +        Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
    1.39 +      fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
    1.40        val cluster_substs =
    1.41          substs
    1.42          |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
    1.43                            if ax_no' = ax_no then
    1.44 -                            tsubst |> filter (in_right_cluster
    1.45 -                                              o fst o fst o dest_Var o fst)
    1.46 -                                   |> map snd |> SOME
    1.47 -                           else
    1.48 -                             NONE)
    1.49 +                            tsubst |> map (apfst cluster_of_var)
    1.50 +                                   |> filter (in_right_cluster o fst)
    1.51 +                                   |> map (apfst snd)
    1.52 +                                   |> SOME
    1.53 +                          else
    1.54 +                            NONE)
    1.55        fun do_cluster_subst cluster_subst =
    1.56 -        map (instantiate_forall_tac thy) cluster_subst @ [rotate_tac 1]
    1.57 +        map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
    1.58        val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
    1.59      in
    1.60        rotate_tac first_prem
    1.61 @@ -695,6 +710,7 @@
    1.62      let
    1.63        val thy = ProofContext.theory_of ctxt
    1.64        (* distinguish variables with same name but different types *)
    1.65 +      (* ### FIXME: needed? *)
    1.66        val prems_imp_false' =
    1.67          prems_imp_false |> try (forall_intr_vars #> gen_all)
    1.68                          |> the_default prems_imp_false
    1.69 @@ -779,7 +795,6 @@
    1.70        val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
    1.71                         cat_lines (map string_for_subst_info substs))
    1.72        val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
    1.73 -      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
    1.74        val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
    1.75  *)
    1.76        fun rotation_for_subgoal i =