ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
authorblanchet
Fri Oct 29 12:49:05 2010 +0200 (2010-10-29)
changeset 402628403085384eb
parent 40261 7a02144874f3
child 40263 51ed7a5ad4c5
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -111,39 +111,57 @@
     1.4      SOME th => th
     1.5    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
     1.6  
     1.7 -(* Applying "choice" swaps the bound variable names. We tweak
     1.8 -   "Thm.rename_boundvars"'s input to get the desired names. *)
     1.9 -fun fix_bounds (_ $ (Const (@{const_name Ex}, _)
    1.10 -                     $ Abs (_, _, Const (@{const_name All}, _) $ _)))
    1.11 -               (t0 $ (Const (@{const_name All}, T1)
    1.12 -                      $ Abs (a1, T1', Const (@{const_name Ex}, T2)
    1.13 -                                      $ Abs (a2, T2', t')))) =
    1.14 -    t0 $ (Const (@{const_name All}, T1)
    1.15 -          $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t')))
    1.16 -  | fix_bounds _ t = t
    1.17 +(* Hack to make it less likely that we lose our precious bound variable names in
    1.18 +   "rename_bound_vars_RS" below, because of a clash. *)
    1.19 +val protect_prefix = "Meson_xyzzy"
    1.20 +
    1.21 +fun protect_bound_var_names (t $ u) =
    1.22 +    protect_bound_var_names t $ protect_bound_var_names u
    1.23 +  | protect_bound_var_names (Abs (s, T, t')) =
    1.24 +    Abs (protect_prefix ^ s, T, protect_bound_var_names t')
    1.25 +  | protect_bound_var_names t = t
    1.26  
    1.27 -(* Hack to make it less likely that we lose our precious bound variable names in
    1.28 -   "rename_bvs_RS" below, because of a clash. *)
    1.29 -val protect_prefix = "_"
    1.30 +fun fix_bound_var_names old_t new_t =
    1.31 +  let
    1.32 +    fun quant_of @{const_name All} = SOME true
    1.33 +      | quant_of @{const_name Ball} = SOME true
    1.34 +      | quant_of @{const_name Ex} = SOME false
    1.35 +      | quant_of @{const_name Bex} = SOME false
    1.36 +      | quant_of _ = NONE
    1.37 +    val flip_quant = Option.map not
    1.38 +    fun some_eq (SOME x) (SOME y) = x = y
    1.39 +      | some_eq _ _ = false
    1.40 +    fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) =
    1.41 +        add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s
    1.42 +      | add_names quant (@{const Not} $ t) = add_names (flip_quant quant) t
    1.43 +      | add_names quant (@{const implies} $ t1 $ t2) =
    1.44 +        add_names (flip_quant quant) t1 #> add_names quant t2
    1.45 +      | add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2]
    1.46 +      | add_names _ _ = I
    1.47 +    fun lost_names quant =
    1.48 +      subtract (op =) (add_names quant new_t []) (add_names quant old_t [])
    1.49 +    fun aux ((t1 as Const (quant_s, _)) $ (Abs (s, T, t'))) =
    1.50 +      t1 $ Abs (s |> String.isPrefix protect_prefix s
    1.51 +                   ? perhaps (try (fn _ => hd (lost_names (quant_of quant_s)))),
    1.52 +                T, aux t')
    1.53 +      | aux (t1 $ t2) = aux t1 $ aux t2
    1.54 +      | aux t = t
    1.55 +  in aux new_t end
    1.56  
    1.57 -fun protect_bounds (t $ u) = protect_bounds t $ protect_bounds u
    1.58 -  | protect_bounds (Abs (s, T, t')) =
    1.59 -    Abs (protect_prefix ^ s, T, protect_bounds t')
    1.60 -  | protect_bounds t = t
    1.61 -
    1.62 -(* Forward proof while preserving bound variables names*)
    1.63 -fun rename_bvs_RS th rl =
    1.64 +(* Forward proof while preserving bound variables names *)
    1.65 +fun rename_bound_vars_RS th rl =
    1.66    let
    1.67      val t = concl_of th
    1.68      val r = concl_of rl
    1.69 -    val th' = th RS Thm.rename_boundvars r (protect_bounds r) rl
    1.70 +    val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl
    1.71      val t' = concl_of th'
    1.72 -  in Thm.rename_boundvars t' (fix_bounds t' t) th' end
    1.73 +  in Thm.rename_boundvars t' (fix_bound_var_names t t') th' end
    1.74  
    1.75  (*raises exception if no rules apply*)
    1.76  fun tryres (th, rls) =
    1.77    let fun tryall [] = raise THM("tryres", 0, th::rls)
    1.78 -        | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
    1.79 +        | tryall (rl::rls) =
    1.80 +          (rename_bound_vars_RS th rl handle THM _ => tryall rls)
    1.81    in  tryall rls  end;
    1.82  
    1.83  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    1.84 @@ -577,7 +595,7 @@
    1.85                 |> forward_res ctxt aux
    1.86                 |> aux
    1.87                 handle THM ("tryres", _, _) =>
    1.88 -                      rename_bvs_RS th ex_forward
    1.89 +                      rename_bound_vars_RS th ex_forward
    1.90                        |> forward_res ctxt aux
    1.91    in aux o make_nnf ctxt end
    1.92  
     2.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
     2.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
     2.3 @@ -346,13 +346,13 @@
     2.4                |>> the_single |>> cterm_of thy
     2.5            in
     2.6              (SOME (discharger_th, fully_skolemized_ct),
     2.7 -                   Thm.assume fully_skolemized_ct, ctxt)
     2.8 +             (Thm.assume fully_skolemized_ct, ctxt))
     2.9            end
    2.10         else
    2.11 -         (NONE, th, ctxt)
    2.12 +         (NONE, (th, ctxt))
    2.13        end
    2.14      else
    2.15 -      (NONE, th, ctxt)
    2.16 +      (NONE, (th, ctxt))
    2.17    end
    2.18  
    2.19  (* Convert a theorem to CNF, with additional premises due to skolemization. *)
    2.20 @@ -360,7 +360,8 @@
    2.21    let
    2.22      val thy = ProofContext.theory_of ctxt0
    2.23      val choice_ths = choice_theorems thy
    2.24 -    val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    2.25 +    val (opt, (nnf_th, ctxt)) =
    2.26 +      nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    2.27      fun clausify th =
    2.28        make_cnf (if new_skolemizer orelse null choice_ths then
    2.29                    []
    2.30 @@ -370,6 +371,7 @@
    2.31      val (cnf_ths, ctxt) =
    2.32        clausify nnf_th
    2.33        |> (fn ([], _) =>
    2.34 +             (* FIXME: This probably doesn't work with the new Skolemizer *)
    2.35               clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
    2.36             | p => p)
    2.37      fun intr_imp ct th =
     3.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Fri Oct 29 12:49:05 2010 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Fri Oct 29 12:49:05 2010 +0200
     3.3 @@ -157,7 +157,7 @@
     3.4        (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     3.5      else
     3.6        Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
     3.7 -                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt [] (cls @ ths)) 1)
     3.8 +                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
     3.9                    ctxt i st0
    3.10    end
    3.11