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 =
```