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.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