generalized qed_spec_mp code to work for ZF
authorpaulson
Wed Jan 13 12:08:18 1999 +0100 (1999-01-13)
changeset 6113b321f5aaa5f4
parent 6112 5e4871c5136b
child 6114 45958e54d72e
generalized qed_spec_mp code to work for ZF
src/FOL/IFOL.ML
     1.1 --- a/src/FOL/IFOL.ML	Wed Jan 13 11:57:09 1999 +0100
     1.2 +++ b/src/FOL/IFOL.ML	Wed Jan 13 12:08:18 1999 +0100
     1.3 @@ -6,9 +6,6 @@
     1.4  Tactics and lemmas for IFOL.thy (intuitionistic first-order logic)
     1.5  *)
     1.6  
     1.7 -open IFOL;
     1.8 -
     1.9 -
    1.10  qed_goalw "TrueI" IFOL.thy [True_def] "True"
    1.11   (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]);
    1.12  
    1.13 @@ -242,7 +239,8 @@
    1.14  val prems = goal IFOL.thy "(A == B) ==> A = B";
    1.15  by (rewrite_goals_tac prems);
    1.16  by (rtac refl 1);
    1.17 -qed "def_imp_eq";
    1.18 +qed "meta_eq_to_obj_eq";
    1.19 +
    1.20  
    1.21  (*Substitution: rule and tactic*)
    1.22  bind_thm ("ssubst", sym RS subst);
    1.23 @@ -250,7 +248,7 @@
    1.24  (*Apply an equality or definition ONCE.
    1.25    Fails unless the substitution has an effect*)
    1.26  fun stac th = 
    1.27 -  let val th' = th RS def_imp_eq handle _ => th
    1.28 +  let val th' = th RS meta_eq_to_obj_eq handle _ => th
    1.29    in  CHANGED_GOAL (rtac (th' RS ssubst))
    1.30    end;
    1.31  
    1.32 @@ -397,21 +395,25 @@
    1.33  
    1.34  (** strip ALL and --> from proved goal while preserving ALL-bound var names **)
    1.35  
    1.36 +fun make_new_spec rl =
    1.37 +  (* Use a crazy name to avoid forall_intr failing because of
    1.38 +     duplicate variable name *)
    1.39 +  let val myspec = read_instantiate [("P","?wlzickd")] rl
    1.40 +      val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
    1.41 +      val cvx = cterm_of (#sign(rep_thm myspec)) vx
    1.42 +  in (vxT, forall_intr cvx myspec) end;
    1.43 +
    1.44  local
    1.45  
    1.46 -(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
    1.47 -val myspec = read_instantiate [("P","?XXX")] spec;
    1.48 -val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
    1.49 -val cvx = cterm_of (#sign(rep_thm myspec)) vx;
    1.50 -val aspec = forall_intr cvx myspec;
    1.51 +val (specT,  spec')  = make_new_spec spec
    1.52  
    1.53  in
    1.54  
    1.55  fun RSspec th =
    1.56    (case concl_of th of
    1.57       _ $ (Const("All",_) $ Abs(a,_,_)) =>
    1.58 -         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
    1.59 -         in th RS forall_elim ca aspec end
    1.60 +         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT))
    1.61 +         in th RS forall_elim ca spec' end
    1.62    | _ => raise THM("RSspec",0,[th]));
    1.63  
    1.64  fun RSmp th =
    1.65 @@ -420,9 +422,9 @@
    1.66    | _ => raise THM("RSmp",0,[th]));
    1.67  
    1.68  fun normalize_thm funs =
    1.69 -let fun trans [] th = th
    1.70 -      | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
    1.71 -in trans funs end;
    1.72 +  let fun trans [] th = th
    1.73 +	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
    1.74 +  in trans funs end;
    1.75  
    1.76  fun qed_spec_mp name =
    1.77    let val thm = normalize_thm [RSspec,RSmp] (result())