fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
authorblanchet
Fri Oct 29 12:49:05 2010 +0200 (2010-10-29)
changeset 4026073ecbe2d432b
parent 40259 c0e34371c2e2
child 40261 7a02144874f3
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
src/HOL/Tools/Meson/meson_clausify.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 @@ -241,10 +241,11 @@
     1.4       String.isPrefix new_skolem_var_prefix s)
     1.5    end
     1.6  
     1.7 -fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct =
     1.8 -  ct
     1.9 -  |> (case term_of ct of
    1.10 -        Const (s, _) $ Abs (s', _, _) =>
    1.11 +fun rename_bound_vars_to_be_zapped ax_no =
    1.12 +  let
    1.13 +    fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
    1.14 +      case t of
    1.15 +        (t1 as Const (s, _)) $ Abs (s', T, t') =>
    1.16          if s = @{const_name all} orelse s = @{const_name All} orelse
    1.17             s = @{const_name Ex} then
    1.18            let
    1.19 @@ -252,29 +253,48 @@
    1.20              val (cluster, index_no) =
    1.21                if skolem = cluster_skolem then (cluster, index_no)
    1.22                else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
    1.23 -          in
    1.24 -            Thm.dest_comb #> snd
    1.25 -            #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s'))
    1.26 -            #> snd #> zap cluster (index_no + 1) pos
    1.27 -          end
    1.28 +            val s' = zapped_var_name cluster index_no s'
    1.29 +          in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end
    1.30 +        else
    1.31 +          t
    1.32 +      | (t1 as Const (s, _)) $ t2 $ t3 =>
    1.33 +        if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
    1.34 +          t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
    1.35 +        else if s = @{const_name HOL.conj} orelse
    1.36 +                s = @{const_name HOL.disj} then
    1.37 +          t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3
    1.38 +        else
    1.39 +          t
    1.40 +      | (t1 as Const (s, _)) $ t2 =>
    1.41 +        if s = @{const_name Trueprop} then
    1.42 +          t1 $ aux cluster index_no pos t2
    1.43 +        else if s = @{const_name Not} then
    1.44 +          t1 $ aux cluster index_no (not pos) t2
    1.45 +        else
    1.46 +          t
    1.47 +      | _ => t
    1.48 +  in aux ((ax_no, 0), true) 0 true end
    1.49 +
    1.50 +fun zap pos ct =
    1.51 +  ct
    1.52 +  |> (case term_of ct of
    1.53 +        Const (s, _) $ Abs (s', _, _) =>
    1.54 +        if s = @{const_name all} orelse s = @{const_name All} orelse
    1.55 +           s = @{const_name Ex} then
    1.56 +          Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
    1.57          else
    1.58            Conv.all_conv
    1.59        | Const (s, _) $ _ $ _ =>
    1.60          if s = @{const_name "==>"} orelse s = @{const_name implies} then
    1.61 -          Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos)))
    1.62 -                                (zap cluster index_no pos)
    1.63 +          Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
    1.64          else if s = @{const_name conj} orelse s = @{const_name disj} then
    1.65 -          Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos))
    1.66 -                                (zap cluster index_no pos)
    1.67 +          Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
    1.68          else
    1.69            Conv.all_conv
    1.70        | Const (s, _) $ _ =>
    1.71 -        if s = @{const_name Trueprop} then
    1.72 -          Conv.arg_conv (zap cluster index_no pos)
    1.73 -        else if s = @{const_name Not} then
    1.74 -          Conv.arg_conv (zap cluster index_no (not pos))
    1.75 -        else
    1.76 -          Conv.all_conv
    1.77 +        if s = @{const_name Trueprop} then Conv.arg_conv (zap pos)
    1.78 +        else if s = @{const_name Not} then Conv.arg_conv (zap (not pos))
    1.79 +        else Conv.all_conv
    1.80        | _ => Conv.all_conv)
    1.81  
    1.82  fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
    1.83 @@ -304,24 +324,25 @@
    1.84            #> simplify (ss_only @{thms all_simps[symmetric]})
    1.85          val pull_out =
    1.86            simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
    1.87 -        val (discharger_th, fully_skolemized_th) =
    1.88 -          if null choice_ths then
    1.89 -            th |> `I |>> pull_out ||> skolemize [no_choice]
    1.90 -          else
    1.91 -            th |> skolemize choice_ths |> `I
    1.92 -        val t =
    1.93 -          fully_skolemized_th |> cprop_of
    1.94 -          |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context
    1.95 -          |> cprop_of |> Thm.dest_equals |> snd |> term_of
    1.96 +        val discharger_th =
    1.97 +          th |> (if null choice_ths then pull_out else skolemize choice_ths)
    1.98 +        val fully_skolemized_t =
    1.99 +          th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
   1.100 +             |> Skip_Proof.make_thm thy |> skolemize [no_choice] |> cprop_of
   1.101 +             |> zap true |> Drule.export_without_context
   1.102 +             |> cprop_of |> Thm.dest_equals |> snd |> term_of
   1.103        in
   1.104          if exists_subterm (fn Var ((s, _), _) =>
   1.105                                String.isPrefix new_skolem_var_prefix s
   1.106 -                            | _ => false) t then
   1.107 +                            | _ => false) fully_skolemized_t then
   1.108            let
   1.109 -            val (ct, ctxt) =
   1.110 -              Variable.import_terms true [t] ctxt
   1.111 +            val (fully_skolemized_ct, ctxt) =
   1.112 +              Variable.import_terms true [fully_skolemized_t] ctxt
   1.113                |>> the_single |>> cterm_of thy
   1.114 -          in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end
   1.115 +          in
   1.116 +            (SOME (discharger_th, fully_skolemized_ct),
   1.117 +                   Thm.assume fully_skolemized_ct, ctxt)
   1.118 +          end
   1.119         else
   1.120           (NONE, th, ctxt)
   1.121        end