src/HOL/Tools/Meson/meson_clausify.ML
changeset 40261 7a02144874f3
parent 40260 73ecbe2d432b
child 40262 8403085384eb
     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