src/Pure/drule.ML
author wenzelm
Fri Nov 21 15:27:43 1997 +0100 (1997-11-21)
changeset 4270 957c887b89b5
parent 4057 edd8cb346109
child 4281 6c6073b13600
permissions -rw-r--r--
changed Sequence interface (now Seq, in seq.ML);
     1 (*  Title:      Pure/drule.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Derived rules and other operations on theorems.
     7 *)
     8 
     9 infix 0 RS RSN RL RLN MRS MRL COMP;
    10 
    11 signature DRULE =
    12 sig
    13   val asm_rl		: thm
    14   val assume_ax		: theory -> string -> thm
    15   val COMP		: thm * thm -> thm
    16   val compose		: thm * int * thm -> thm list
    17   val cprems_of		: thm -> cterm list
    18   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    19   val cut_rl		: thm
    20   val equal_abs_elim	: cterm  -> thm -> thm
    21   val equal_abs_elim_list: cterm list -> thm -> thm
    22   val equal_intr_rule   : thm
    23   val eq_thm		: thm * thm -> bool
    24   val same_thm		: thm * thm -> bool
    25   val eq_thm_sg		: thm * thm -> bool
    26   val flexpair_abs_elim_list: cterm list -> thm -> thm
    27   val forall_intr_list	: cterm list -> thm -> thm
    28   val forall_intr_frees	: thm -> thm
    29   val forall_intr_vars	: thm -> thm
    30   val forall_elim_list	: cterm list -> thm -> thm
    31   val forall_elim_var	: int -> thm -> thm
    32   val forall_elim_vars	: int -> thm -> thm
    33   val implies_elim_list	: thm -> thm list -> thm
    34   val implies_intr_list	: cterm list -> thm -> thm
    35   val dest_implies      : cterm -> cterm * cterm
    36   val MRL		: thm list list * thm list -> thm list
    37   val MRS		: thm list * thm -> thm
    38   val read_instantiate	: (string*string)list -> thm -> thm
    39   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    40   val read_insts	:
    41           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    42                   -> (indexname -> typ option) * (indexname -> sort option)
    43                   -> string list -> (string*string)list
    44                   -> (indexname*ctyp)list * (cterm*cterm)list
    45   val reflexive_thm	: thm
    46   val refl_implies      : thm
    47   val revcut_rl		: thm
    48   val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
    49         -> meta_simpset -> int -> thm -> thm
    50   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    51   val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    52   val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
    53 	-> meta_simpset -> thm -> thm
    54   val RS		: thm * thm -> thm
    55   val RSN		: thm * (int * thm) -> thm
    56   val RL		: thm list * thm list -> thm list
    57   val RLN		: thm list * (int * thm list) -> thm list
    58   val size_of_thm	: thm -> int
    59   val skip_flexpairs	: cterm -> cterm
    60   val standard		: thm -> thm
    61   val strip_imp_prems	: cterm -> cterm list
    62   val swap_prems_rl     : thm
    63   val symmetric_thm	: thm
    64   val thin_rl		: thm
    65   val transitive_thm	: thm
    66   val triv_forall_equality: thm
    67   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    68   val zero_var_indexes	: thm -> thm
    69 end;
    70 
    71 structure Drule : DRULE =
    72 struct
    73 
    74 
    75 (** some cterm->cterm operations: much faster than calling cterm_of! **)
    76 
    77 (** SAME NAMES as in structure Logic: use compound identifiers! **)
    78 
    79 (*dest_implies for cterms. Note T=prop below*)
    80 fun dest_implies ct =
    81     case term_of ct of 
    82 	(Const("==>", _) $ _ $ _) => 
    83 	    let val (ct1,ct2) = dest_comb ct
    84 	    in  (#2 (dest_comb ct1), ct2)  end	     
    85       | _ => raise TERM ("dest_implies", [term_of ct]) ;
    86 
    87 
    88 (*Discard flexflex pairs; return a cterm*)
    89 fun skip_flexpairs ct =
    90     case term_of ct of
    91 	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
    92 	    skip_flexpairs (#2 (dest_implies ct))
    93       | _ => ct;
    94 
    95 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    96 fun strip_imp_prems ct =
    97     let val (cA,cB) = dest_implies ct
    98     in  cA :: strip_imp_prems cB  end
    99     handle TERM _ => [];
   100 
   101 (* A1==>...An==>B  goes to B, where B is not an implication *)
   102 fun strip_imp_concl ct =
   103     case term_of ct of (Const("==>", _) $ _ $ _) => 
   104 	strip_imp_concl (#2 (dest_comb ct))
   105   | _ => ct;
   106 
   107 (*The premises of a theorem, as a cterm list*)
   108 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
   109 
   110 
   111 (** reading of instantiations **)
   112 
   113 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   114         | _ => error("Lexical error in variable name " ^ quote (implode cs));
   115 
   116 fun absent ixn =
   117   error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   118 
   119 fun inst_failure ixn =
   120   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   121 
   122 (* this code is a bit of a mess. add_cterm could be simplified greatly if
   123    simultaneous instantiations were read or at least type checked
   124    simultaneously rather than one after the other. This would make the tricky
   125    composition of implicit type instantiations (parameter tye) superfluous.
   126 *)
   127 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
   128 let val {tsig,...} = Sign.rep_sg sign
   129     fun split([],tvs,vs) = (tvs,vs)
   130       | split((sv,st)::l,tvs,vs) = (case explode sv of
   131                   "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   132                 | cs => split(l,tvs,(indexname cs,st)::vs));
   133     val (tvs,vs) = split(insts,[],[]);
   134     fun readT((a,i),st) =
   135         let val ixn = ("'" ^ a,i);
   136             val S = case rsorts ixn of Some S => S | None => absent ixn;
   137             val T = Sign.read_typ (sign,sorts) st;
   138         in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   139            else inst_failure ixn
   140         end
   141     val tye = map readT tvs;
   142     fun add_cterm ((cts,tye,used), (ixn,st)) =
   143         let val T = case rtypes ixn of
   144                       Some T => typ_subst_TVars tye T
   145                     | None => absent ixn;
   146             val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
   147             val cts' = (ixn,T,ct)::cts
   148             fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
   149             val used' = add_term_tvarnames(term_of ct,used);
   150         in (map inst cts',tye2 @ tye,used') end
   151     val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
   152 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
   153     map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
   154 end;
   155 
   156 
   157 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term
   158      Used for establishing default types (of variables) and sorts (of
   159      type variables) when reading another term.
   160      Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
   161 ***)
   162 
   163 fun types_sorts thm =
   164     let val {prop,hyps,...} = rep_thm thm;
   165         val big = list_comb(prop,hyps); (* bogus term! *)
   166         val vars = map dest_Var (term_vars big);
   167         val frees = map dest_Free (term_frees big);
   168         val tvars = term_tvars big;
   169         val tfrees = term_tfrees big;
   170         fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i));
   171         fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
   172     in (typ,sort) end;
   173 
   174 (** Standardization of rules **)
   175 
   176 (*Generalization over a list of variables, IGNORING bad ones*)
   177 fun forall_intr_list [] th = th
   178   | forall_intr_list (y::ys) th =
   179         let val gth = forall_intr_list ys th
   180         in  forall_intr y gth   handle THM _ =>  gth  end;
   181 
   182 (*Generalization over all suitable Free variables*)
   183 fun forall_intr_frees th =
   184     let val {prop,sign,...} = rep_thm th
   185     in  forall_intr_list
   186          (map (cterm_of sign) (sort atless (term_frees prop)))
   187          th
   188     end;
   189 
   190 (*Replace outermost quantified variable by Var of given index.
   191     Could clash with Vars already present.*)
   192 fun forall_elim_var i th =
   193     let val {prop,sign,...} = rep_thm th
   194     in case prop of
   195           Const("all",_) $ Abs(a,T,_) =>
   196               forall_elim (cterm_of sign (Var((a,i), T)))  th
   197         | _ => raise THM("forall_elim_var", i, [th])
   198     end;
   199 
   200 (*Repeat forall_elim_var until all outer quantifiers are removed*)
   201 fun forall_elim_vars i th =
   202     forall_elim_vars i (forall_elim_var i th)
   203         handle THM _ => th;
   204 
   205 (*Specialization over a list of cterms*)
   206 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
   207 
   208 (* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
   209 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
   210 
   211 (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
   212 fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
   213 
   214 (*Reset Var indexes to zero, renaming to preserve distinctness*)
   215 fun zero_var_indexes th =
   216     let val {prop,sign,...} = rep_thm th;
   217         val vars = term_vars prop
   218         val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
   219         val inrs = add_term_tvars(prop,[]);
   220         val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
   221         val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
   222 	             (inrs, nms')
   223         val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
   224         fun varpairs([],[]) = []
   225           | varpairs((var as Var(v,T)) :: vars, b::bs) =
   226                 let val T' = typ_subst_TVars tye T
   227                 in (cterm_of sign (Var(v,T')),
   228                     cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   229                 end
   230           | varpairs _ = raise TERM("varpairs", []);
   231     in instantiate (ctye, varpairs(vars,rev bs)) th end;
   232 
   233 
   234 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
   235     all generality expressed by Vars having index 0.*)
   236 fun standard th =
   237   let val {maxidx,...} = rep_thm th
   238   in
   239     th |> implies_intr_hyps
   240        |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
   241        |> Thm.strip_shyps |> Thm.implies_intr_shyps
   242        |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   243   end;
   244 
   245 
   246 (*Assume a new formula, read following the same conventions as axioms.
   247   Generalizes over Free variables,
   248   creates the assumption, and then strips quantifiers.
   249   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   250              [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
   251 fun assume_ax thy sP =
   252     let val sign = sign_of thy
   253         val prop = Logic.close_form (term_of (read_cterm sign
   254                          (sP, propT)))
   255     in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
   256 
   257 (*Resolution: exactly one resolvent must be produced.*)
   258 fun tha RSN (i,thb) =
   259   case Seq.chop (2, biresolution false [(false,tha)] i thb) of
   260       ([th],_) => th
   261     | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
   262     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
   263 
   264 (*resolution: P==>Q, Q==>R gives P==>R. *)
   265 fun tha RS thb = tha RSN (1,thb);
   266 
   267 (*For joining lists of rules*)
   268 fun thas RLN (i,thbs) =
   269   let val resolve = biresolution false (map (pair false) thas) i
   270       fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
   271   in  List.concat (map resb thbs)  end;
   272 
   273 fun thas RL thbs = thas RLN (1,thbs);
   274 
   275 (*Resolve a list of rules against bottom_rl from right to left;
   276   makes proof trees*)
   277 fun rls MRS bottom_rl =
   278   let fun rs_aux i [] = bottom_rl
   279         | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
   280   in  rs_aux 1 rls  end;
   281 
   282 (*As above, but for rule lists*)
   283 fun rlss MRL bottom_rls =
   284   let fun rs_aux i [] = bottom_rls
   285         | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
   286   in  rs_aux 1 rlss  end;
   287 
   288 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   289   with no lifting or renaming!  Q may contain ==> or meta-quants
   290   ALWAYS deletes premise i *)
   291 fun compose(tha,i,thb) =
   292     Seq.list_of (bicompose false (false,tha,0) i thb);
   293 
   294 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
   295 fun tha COMP thb =
   296     case compose(tha,1,thb) of
   297         [th] => th
   298       | _ =>   raise THM("COMP", 1, [tha,thb]);
   299 
   300 (*Instantiate theorem th, reading instantiations under signature sg*)
   301 fun read_instantiate_sg sg sinsts th =
   302     let val ts = types_sorts th;
   303         val used = add_term_tvarnames(#prop(rep_thm th),[]);
   304     in  instantiate (read_insts sg ts ts used sinsts) th  end;
   305 
   306 (*Instantiate theorem th, reading instantiations under theory of th*)
   307 fun read_instantiate sinsts th =
   308     read_instantiate_sg (#sign (rep_thm th)) sinsts th;
   309 
   310 
   311 (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   312   Instantiates distinct Vars by terms, inferring type instantiations. *)
   313 local
   314   fun add_types ((ct,cu), (sign,tye,maxidx)) =
   315     let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   316         and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   317         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   318         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   319         val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
   320           handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   321     in  (sign', tye', maxi')  end;
   322 in
   323 fun cterm_instantiate ctpairs0 th =
   324   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
   325       val tsig = #tsig(Sign.rep_sg sign);
   326       fun instT(ct,cu) = let val inst = subst_TVars tye
   327                          in (cterm_fun inst ct, cterm_fun inst cu) end
   328       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   329   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   330   handle TERM _ =>
   331            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   332        | TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th])
   333 end;
   334 
   335 
   336 (** theorem equality **)
   337 
   338 val eq_thm = Thm.eq_thm;
   339 
   340 (*equality of theorems using similarity of signatures,
   341   i.e. the theorems belong to the same theory but not necessarily to the same
   342   version of this theory*)
   343 fun same_thm (th1,th2) =
   344     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   345         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   346     in  Sign.same_sg (sg1,sg2) andalso
   347         eq_set_sort (shyps1, shyps2) andalso
   348         aconvs(hyps1,hyps2) andalso
   349         prop1 aconv prop2
   350     end;
   351 
   352 (*Do the two theorems have the same signature?*)
   353 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   354 
   355 (*Useful "distance" function for BEST_FIRST*)
   356 val size_of_thm = size_of_term o #prop o rep_thm;
   357 
   358 
   359 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
   360     (some) type variable renaming **)
   361 
   362  (* Can't use term_vars, because it sorts the resulting list of variable names.
   363     We instead need the unique list noramlised by the order of appearance
   364     in the term. *)
   365 fun term_vars' (t as Var(v,T)) = [t]
   366   | term_vars' (Abs(_,_,b)) = term_vars' b
   367   | term_vars' (f$a) = (term_vars' f) @ (term_vars' a)
   368   | term_vars' _ = [];
   369 
   370 fun forall_intr_vars th =
   371   let val {prop,sign,...} = rep_thm th;
   372       val vars = distinct (term_vars' prop);
   373   in forall_intr_list (map (cterm_of sign) vars) th end;
   374 
   375 fun weak_eq_thm (tha,thb) =
   376     eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
   377 
   378 
   379 
   380 (*** Meta-Rewriting Rules ***)
   381 
   382 fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
   383 
   384 val reflexive_thm =
   385   let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
   386   in store_thm "reflexive" (Thm.reflexive cx) end;
   387 
   388 val symmetric_thm =
   389   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   390   in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   391 
   392 val transitive_thm =
   393   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   394       val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
   395       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   396   in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   397 
   398 (** Below, a "conversion" has type cterm -> thm **)
   399 
   400 val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
   401 
   402 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   403 (*Do not rewrite flex-flex pairs*)
   404 fun goals_conv pred cv =
   405   let fun gconv i ct =
   406         let val (A,B) = dest_implies ct
   407             val (thA,j) = case term_of A of
   408                   Const("=?=",_)$_$_ => (reflexive A, i)
   409                 | _ => (if pred i then cv A else reflexive A, i+1)
   410         in  combination (combination refl_implies thA) (gconv j B) end
   411         handle TERM _ => reflexive ct
   412   in gconv 1 end;
   413 
   414 (*Use a conversion to transform a theorem*)
   415 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   416 
   417 (*rewriting conversion*)
   418 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   419 
   420 (*Rewrite a theorem*)
   421 fun rewrite_rule_aux _ []   th = th
   422   | rewrite_rule_aux prover thms th =
   423       fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
   424 
   425 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
   426 
   427 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   428 fun rewrite_goals_rule_aux _ []   th = th
   429   | rewrite_goals_rule_aux prover thms th =
   430       fconv_rule (goals_conv (K true) (rew_conv (true, true) prover
   431         (Thm.mss_of thms))) th;
   432 
   433 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   434 fun rewrite_goal_rule mode prover mss i thm =
   435   if 0 < i  andalso  i <= nprems_of thm
   436   then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
   437   else raise THM("rewrite_goal_rule",i,[thm]);
   438 
   439 
   440 (** Derived rules mainly for METAHYPS **)
   441 
   442 (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   443 fun equal_abs_elim ca eqth =
   444   let val {sign=signa, t=a, ...} = rep_cterm ca
   445       and combth = combination eqth (reflexive ca)
   446       val {sign,prop,...} = rep_thm eqth
   447       val (abst,absu) = Logic.dest_equals prop
   448       val cterm = cterm_of (Sign.merge (sign,signa))
   449   in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   450            (transitive combth (beta_conversion (cterm (absu$a))))
   451   end
   452   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   453 
   454 (*Calling equal_abs_elim with multiple terms*)
   455 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   456 
   457 local
   458   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   459   fun err th = raise THM("flexpair_inst: ", 0, [th])
   460   fun flexpair_inst def th =
   461     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   462         val cterm = cterm_of sign
   463         fun cvar a = cterm(Var((a,0),alpha))
   464         val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
   465                    def
   466     in  equal_elim def' th
   467     end
   468     handle THM _ => err th | bind => err th
   469 in
   470 val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
   471 and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
   472 end;
   473 
   474 (*Version for flexflex pairs -- this supports lifting.*)
   475 fun flexpair_abs_elim_list cts =
   476     flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
   477 
   478 
   479 (*** Some useful meta-theorems ***)
   480 
   481 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   482 val asm_rl =
   483   store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)));
   484 
   485 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   486 val cut_rl =
   487   store_thm "cut_rl"
   488     (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT)));
   489 
   490 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   491      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   492 val revcut_rl =
   493   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   494       and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
   495   in
   496     store_thm "revcut_rl"
   497       (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   498   end;
   499 
   500 (*for deleting an unwanted assumption*)
   501 val thin_rl =
   502   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   503       and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
   504   in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   505   end;
   506 
   507 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   508 val triv_forall_equality =
   509   let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   510       and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
   511       and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
   512   in
   513     store_thm "triv_forall_equality"
   514       (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   515         (implies_intr V  (forall_intr x (assume V))))
   516   end;
   517 
   518 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   519    (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
   520    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   521 *)
   522 val swap_prems_rl =
   523   let val cmajor = read_cterm (sign_of ProtoPure.thy)
   524             ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
   525       val major = assume cmajor;
   526       val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
   527       val minor1 = assume cminor1;
   528       val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
   529       val minor2 = assume cminor2;
   530   in store_thm "swap_prems_rl"
   531        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   532          (implies_elim (implies_elim major minor1) minor2))))
   533   end;
   534 
   535 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
   536    ==> PROP ?phi == PROP ?psi
   537    Introduction rule for == using ==> not meta-hyps.
   538 *)
   539 val equal_intr_rule =
   540   let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
   541       and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   542   in
   543     store_thm "equal_intr_rule"
   544       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   545   end;
   546 
   547 end;
   548 
   549 open Drule;