more work on new Skolemizer without Hilbert_Choice
authorblanchet
Fri Oct 29 12:49:05 2010 +0200 (2010-10-29)
changeset 402617a02144874f3
parent 40260 73ecbe2d432b
child 40262 8403085384eb
more work on new Skolemizer without Hilbert_Choice
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4  fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
     1.5    (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
     1.6    "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
     1.7 -  string_of_int index_no ^ "_" ^ s
     1.8 +  string_of_int index_no ^ "_" ^ Name.desymbolize false s
     1.9  
    1.10  fun cluster_of_zapped_var_name s =
    1.11    let val get_int = the o Int.fromString o nth (space_explode "_" s) in
    1.12 @@ -299,7 +299,7 @@
    1.13  
    1.14  fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
    1.15  
    1.16 -val no_choice =
    1.17 +val cheat_choice =
    1.18    @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
    1.19    |> Logic.varify_global
    1.20    |> Skip_Proof.make_thm @{theory}
    1.21 @@ -324,11 +324,16 @@
    1.22            #> simplify (ss_only @{thms all_simps[symmetric]})
    1.23          val pull_out =
    1.24            simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
    1.25 +        val no_choice = null choice_ths
    1.26          val discharger_th =
    1.27 -          th |> (if null choice_ths then pull_out else skolemize choice_ths)
    1.28 +          th |> (if no_choice then pull_out else skolemize choice_ths)
    1.29          val fully_skolemized_t =
    1.30 -          th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
    1.31 -             |> Skip_Proof.make_thm thy |> skolemize [no_choice] |> cprop_of
    1.32 +          th |> prop_of
    1.33 +             |> no_choice ? rename_bound_vars_to_be_zapped ax_no
    1.34 +             |> Skip_Proof.make_thm thy |> skolemize [cheat_choice] |> cprop_of
    1.35 +             |> not no_choice
    1.36 +                ? (term_of #> rename_bound_vars_to_be_zapped ax_no
    1.37 +                   #> cterm_of thy)
    1.38               |> zap true |> Drule.export_without_context
    1.39               |> cprop_of |> Thm.dest_equals |> snd |> term_of
    1.40        in
     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     2.3 @@ -628,7 +628,14 @@
     2.4          (case find_index (fn (s', _) => s' = s) params of
     2.5             ~1 => t
     2.6           | j => Bound j)
     2.7 -      | repair (t $ u) = repair t $ repair u
     2.8 +      | repair (t $ u) =
     2.9 +        (case (repair t, repair u) of
    2.10 +           (t as Bound j, u as Bound k) =>
    2.11 +           (* This is a rather subtle trick to repair the discrepancy between
    2.12 +              the fully skolemized term that MESON gives us (where existentials
    2.13 +              were pulled out) and the reality. *)
    2.14 +           if k > j then t else t $ u
    2.15 +         | (t, u) => t $ u)
    2.16        | repair t = t
    2.17      val t' = t |> repair |> fold (curry absdummy) (map snd params)
    2.18      fun do_instantiate th =
    2.19 @@ -641,24 +648,32 @@
    2.20       THEN PRIMITIVE do_instantiate) st
    2.21    end
    2.22  
    2.23 +fun fix_exists_tac thy t =
    2.24 +  etac @{thm exE}
    2.25 +  THEN' rename_tac [t |> dest_Var |> fst |> fst]
    2.26 +
    2.27 +fun release_quantifier_tac thy (skolem, t) =
    2.28 +  (if skolem then fix_exists_tac else instantiate_forall_tac) thy t
    2.29 +
    2.30  fun release_clusters_tac _ _ _ [] = K all_tac
    2.31    | release_clusters_tac thy ax_counts substs
    2.32                           ((ax_no, cluster_no) :: clusters) =
    2.33      let
    2.34 -      fun in_right_cluster s =
    2.35 -        (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
    2.36 -        = cluster_no
    2.37 +      val cluster_of_var =
    2.38 +        Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
    2.39 +      fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
    2.40        val cluster_substs =
    2.41          substs
    2.42          |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
    2.43                            if ax_no' = ax_no then
    2.44 -                            tsubst |> filter (in_right_cluster
    2.45 -                                              o fst o fst o dest_Var o fst)
    2.46 -                                   |> map snd |> SOME
    2.47 -                           else
    2.48 -                             NONE)
    2.49 +                            tsubst |> map (apfst cluster_of_var)
    2.50 +                                   |> filter (in_right_cluster o fst)
    2.51 +                                   |> map (apfst snd)
    2.52 +                                   |> SOME
    2.53 +                          else
    2.54 +                            NONE)
    2.55        fun do_cluster_subst cluster_subst =
    2.56 -        map (instantiate_forall_tac thy) cluster_subst @ [rotate_tac 1]
    2.57 +        map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
    2.58        val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
    2.59      in
    2.60        rotate_tac first_prem
    2.61 @@ -695,6 +710,7 @@
    2.62      let
    2.63        val thy = ProofContext.theory_of ctxt
    2.64        (* distinguish variables with same name but different types *)
    2.65 +      (* ### FIXME: needed? *)
    2.66        val prems_imp_false' =
    2.67          prems_imp_false |> try (forall_intr_vars #> gen_all)
    2.68                          |> the_default prems_imp_false
    2.69 @@ -779,7 +795,6 @@
    2.70        val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
    2.71                         cat_lines (map string_for_subst_info substs))
    2.72        val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
    2.73 -      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
    2.74        val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
    2.75  *)
    2.76        fun rotation_for_subgoal i =