src/HOL/Tools/Meson/meson.ML
 changeset 40262 8403085384eb parent 39979 b13515940b53 child 40724 d01a1b3ab23d
```     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.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
```