src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 40258 2c0d8fe36c21
parent 40221 d10b68c6e6d4
child 40259 c0e34371c2e2
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 11:35:28 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -609,10 +609,6 @@
     1.4        | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
     1.5    in th |> term_instantiate thy (unify_terms (prem, concl) []) end
     1.6  
     1.7 -fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
     1.8 -fun shuffle_ord p =
     1.9 -  rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
    1.10 -
    1.11  val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
    1.12  
    1.13  fun copy_prems_tac [] ns i =
    1.14 @@ -622,10 +618,11 @@
    1.15    | copy_prems_tac (m :: ms) ns i =
    1.16      etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
    1.17  
    1.18 -fun instantiate_forall_tac thy params t i =
    1.19 +fun instantiate_forall_tac thy t i st =
    1.20    let
    1.21 +    val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
    1.22      fun repair (t as (Var ((s, _), _))) =
    1.23 -        (case find_index (fn ((s', _), _) => s' = s) params of
    1.24 +        (case find_index (fn (s', _) => s' = s) params of
    1.25             ~1 => t
    1.26           | j => Bound j)
    1.27        | repair (t $ u) = repair t $ repair u
    1.28 @@ -636,13 +633,13 @@
    1.29          th |> term_instantiate thy [(Var var, t')]
    1.30        end
    1.31    in
    1.32 -    etac @{thm allE} i
    1.33 -    THEN rotate_tac ~1 i
    1.34 -    THEN PRIMITIVE do_instantiate
    1.35 +    (etac @{thm allE} i
    1.36 +     THEN rotate_tac ~1 i
    1.37 +     THEN PRIMITIVE do_instantiate) st
    1.38    end
    1.39  
    1.40 -fun release_clusters_tac _ _ _ _ [] = K all_tac
    1.41 -  | release_clusters_tac thy ax_counts substs params
    1.42 +fun release_clusters_tac _ _ _ [] = K all_tac
    1.43 +  | release_clusters_tac thy ax_counts substs
    1.44                           ((ax_no, cluster_no) :: clusters) =
    1.45      let
    1.46        fun in_right_cluster s =
    1.47 @@ -657,16 +654,14 @@
    1.48                                     |> map snd |> SOME
    1.49                             else
    1.50                               NONE)
    1.51 -      val n = length cluster_substs
    1.52        fun do_cluster_subst cluster_subst =
    1.53 -        map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
    1.54 -      val params' = params (* FIXME ### existentials! *)
    1.55 +        map (instantiate_forall_tac thy) cluster_subst @ [rotate_tac 1]
    1.56        val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
    1.57      in
    1.58        rotate_tac first_prem
    1.59        THEN' (EVERY' (maps do_cluster_subst cluster_substs))
    1.60        THEN' rotate_tac (~ first_prem - length cluster_substs)
    1.61 -      THEN' release_clusters_tac thy ax_counts substs params' clusters
    1.62 +      THEN' release_clusters_tac thy ax_counts substs clusters
    1.63      end
    1.64  
    1.65  val cluster_ord =
    1.66 @@ -683,6 +678,9 @@
    1.67  structure Int_Pair_Graph =
    1.68    Graph(type key = int * int val ord = prod_ord int_ord int_ord)
    1.69  
    1.70 +fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
    1.71 +fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
    1.72 +
    1.73  (* Attempts to derive the theorem "False" from a theorem of the form
    1.74     "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
    1.75     specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
    1.76 @@ -757,12 +755,12 @@
    1.77          handle Int_Pair_Graph.CYCLES _ =>
    1.78                 error "Cannot replay Metis proof in Isabelle without \
    1.79                       \\"Hilbert_Choice\"."
    1.80 -      val params0 =
    1.81 -        [] |> fold (Term.add_vars o snd) (map_filter I axioms)
    1.82 -           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
    1.83 +      val outer_param_names =
    1.84 +        [] |> fold (Term.add_var_names o snd) (map_filter I axioms)
    1.85 +           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
    1.86             |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
    1.87                           cluster_no = 0 andalso skolem)
    1.88 -           |> sort shuffle_ord |> map snd
    1.89 +           |> sort shuffle_ord |> map (fst o snd)
    1.90        val ax_counts =
    1.91          Int_Tysubst_Table.empty
    1.92          |> fold (fn (ax_no, (_, (tysubst, _))) =>
    1.93 @@ -777,8 +775,8 @@
    1.94                       o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
    1.95        val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
    1.96                         cat_lines (map string_for_subst_info substs))
    1.97 -      val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
    1.98        val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
    1.99 +      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
   1.100        val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
   1.101  *)
   1.102        fun rotation_for_subgoal i =
   1.103 @@ -788,14 +786,14 @@
   1.104            (K (cut_rules_tac
   1.105                    (map (fst o the o nth axioms o fst o fst) ax_counts) 1
   1.106                THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
   1.107 +              THEN rename_tac outer_param_names 1
   1.108                THEN copy_prems_tac (map snd ax_counts) [] 1
   1.109 -              THEN release_clusters_tac thy ax_counts substs params0
   1.110 -                                        ordered_clusters 1
   1.111 +              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
   1.112                THEN match_tac [prems_imp_false] 1
   1.113                THEN ALLGOALS (fn i =>
   1.114                         rtac @{thm Meson.skolem_COMBK_I} i
   1.115                         THEN rotate_tac (rotation_for_subgoal i) i
   1.116 -(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*)
   1.117 +(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i) ### FIXME: needed? *)
   1.118                         THEN assume_tac i)))
   1.119        handle ERROR _ =>
   1.120               error ("Cannot replay Metis proof in Isabelle:\n\