Tidying; rotate_prems; moved freeze_thaw from tactic.ML
authorpaulson
Sat Feb 07 14:39:35 1998 +0100 (1998-02-07)
changeset 4610b1322be47244
parent 4609 b435c5a320b0
child 4611 18a3f33f2097
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Feb 07 14:38:57 1998 +0100
     1.2 +++ b/src/Pure/drule.ML	Sat Feb 07 14:39:35 1998 +0100
     1.3 @@ -26,10 +26,12 @@
     1.4    val forall_elim_list	: cterm list -> thm -> thm
     1.5    val forall_elim_var	: int -> thm -> thm
     1.6    val forall_elim_vars	: int -> thm -> thm
     1.7 +  val freeze_thaw	: thm -> thm * (thm -> thm)
     1.8    val implies_elim_list	: thm -> thm list -> thm
     1.9    val implies_intr_list	: cterm list -> thm -> thm
    1.10    val zero_var_indexes	: thm -> thm
    1.11    val standard		: thm -> thm
    1.12 +  val rotate_prems      : int -> thm -> thm
    1.13    val assume_ax		: theory -> string -> thm
    1.14    val RSN		: thm * (int * thm) -> thm
    1.15    val RS		: thm * thm -> thm
    1.16 @@ -240,6 +242,41 @@
    1.17    end;
    1.18  
    1.19  
    1.20 +(*Convert all Vars in a theorem to Frees.  Also return a function for 
    1.21 +  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
    1.22 +  Similar code in type/freeze_thaw*)
    1.23 +fun freeze_thaw th =
    1.24 +  let val fth = freezeT th
    1.25 +      val {prop,sign,...} = rep_thm fth
    1.26 +      val used = add_term_names (prop, [])
    1.27 +      and vars = term_vars prop
    1.28 +      fun newName (Var(ix,_), (pairs,used)) = 
    1.29 +	    let val v = variant used (string_of_indexname ix)
    1.30 +	    in  ((ix,v)::pairs, v::used)  end;
    1.31 +      val (alist, _) = foldr newName (vars, ([], used))
    1.32 +      fun mk_inst (Var(v,T)) = 
    1.33 +	  (cterm_of sign (Var(v,T)),
    1.34 +	   cterm_of sign (Free(the (assoc(alist,v)), T)))
    1.35 +      val insts = map mk_inst vars
    1.36 +      fun thaw th' = 
    1.37 +	  th' |> forall_intr_list (map #2 insts)
    1.38 +	      |> forall_elim_list (map #1 insts)
    1.39 +  in  (instantiate ([],insts) fth, thaw)  end;
    1.40 +
    1.41 +
    1.42 +(*Rotates a rule's premises to the left by k.  Does nothing if k=0 or
    1.43 +  if k equals the number of premises.  Useful, for instance, with etac.
    1.44 +  Similar to tactic/defer_tac*)
    1.45 +fun rotate_prems k rl = 
    1.46 +    let val (rl',thaw) = freeze_thaw rl
    1.47 +	val hyps = strip_imp_prems (adjust_maxidx (cprop_of rl'))
    1.48 +	val hyps' = List.drop(hyps, k)
    1.49 +    in  implies_elim_list rl' (map assume hyps)
    1.50 +        |> implies_intr_list (hyps' @ List.take(hyps, k))
    1.51 +        |> thaw |> varifyT
    1.52 +    end;
    1.53 +
    1.54 +
    1.55  (*Assume a new formula, read following the same conventions as axioms.
    1.56    Generalizes over Free variables,
    1.57    creates the assumption, and then strips quantifiers.
    1.58 @@ -247,8 +284,7 @@
    1.59               [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
    1.60  fun assume_ax thy sP =
    1.61      let val sign = sign_of thy
    1.62 -        val prop = Logic.close_form (term_of (read_cterm sign
    1.63 -                         (sP, propT)))
    1.64 +        val prop = Logic.close_form (term_of (read_cterm sign (sP, propT)))
    1.65      in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
    1.66  
    1.67  (*Resolution: exactly one resolvent must be produced.*)
    1.68 @@ -362,25 +398,32 @@
    1.69  
    1.70  (*** Meta-Rewriting Rules ***)
    1.71  
    1.72 +val proto_sign = sign_of ProtoPure.thy;
    1.73 +
    1.74 +fun read_prop s = read_cterm proto_sign (s, propT);
    1.75 +
    1.76  fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
    1.77  
    1.78  val reflexive_thm =
    1.79 -  let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
    1.80 +  let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
    1.81    in store_thm "reflexive" (Thm.reflexive cx) end;
    1.82  
    1.83  val symmetric_thm =
    1.84 -  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
    1.85 -  in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
    1.86 +  let val xy = read_prop "x::'a::logic == y"
    1.87 +  in store_thm "symmetric" 
    1.88 +      (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy)))
    1.89 +   end;
    1.90  
    1.91  val transitive_thm =
    1.92 -  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
    1.93 -      val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
    1.94 +  let val xy = read_prop "x::'a::logic == y"
    1.95 +      val yz = read_prop "y::'a::logic == z"
    1.96        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.97 -  in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.98 +  in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm))
    1.99 +  end;
   1.100  
   1.101  (** Below, a "conversion" has type cterm -> thm **)
   1.102  
   1.103 -val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
   1.104 +val refl_implies = reflexive (cterm_of proto_sign implies);
   1.105  
   1.106  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   1.107  (*Do not rewrite flex-flex pairs*)
   1.108 @@ -463,18 +506,18 @@
   1.109  
   1.110  (*The rule V/V, obtains assumption solving for eresolve_tac*)
   1.111  val asm_rl =
   1.112 -  store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)));
   1.113 +  store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
   1.114  
   1.115  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   1.116  val cut_rl =
   1.117    store_thm "cut_rl"
   1.118 -    (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT)));
   1.119 +    (trivial(read_prop "PROP ?psi ==> PROP ?theta"));
   1.120  
   1.121  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   1.122       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   1.123  val revcut_rl =
   1.124 -  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   1.125 -      and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
   1.126 +  let val V = read_prop "PROP V"
   1.127 +      and VW = read_prop "PROP V ==> PROP W";
   1.128    in
   1.129      store_thm "revcut_rl"
   1.130        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   1.131 @@ -482,16 +525,16 @@
   1.132  
   1.133  (*for deleting an unwanted assumption*)
   1.134  val thin_rl =
   1.135 -  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   1.136 -      and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
   1.137 +  let val V = read_prop "PROP V"
   1.138 +      and W = read_prop "PROP W";
   1.139    in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   1.140    end;
   1.141  
   1.142  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   1.143  val triv_forall_equality =
   1.144 -  let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   1.145 -      and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
   1.146 -      and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
   1.147 +  let val V  = read_prop "PROP V"
   1.148 +      and QV = read_prop "!!x::'a. PROP V"
   1.149 +      and x  = read_cterm proto_sign ("x", TFree("'a",logicS));
   1.150    in
   1.151      store_thm "triv_forall_equality"
   1.152        (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.153 @@ -503,12 +546,11 @@
   1.154     `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   1.155  *)
   1.156  val swap_prems_rl =
   1.157 -  let val cmajor = read_cterm (sign_of ProtoPure.thy)
   1.158 -            ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
   1.159 +  let val cmajor = read_prop "PROP PhiA ==> PROP PhiB ==> PROP Psi";
   1.160        val major = assume cmajor;
   1.161 -      val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
   1.162 +      val cminor1 = read_prop "PROP PhiA";
   1.163        val minor1 = assume cminor1;
   1.164 -      val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
   1.165 +      val cminor2 = read_prop "PROP PhiB";
   1.166        val minor2 = assume cminor2;
   1.167    in store_thm "swap_prems_rl"
   1.168         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.169 @@ -517,11 +559,11 @@
   1.170  
   1.171  (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
   1.172     ==> PROP ?phi == PROP ?psi
   1.173 -   Introduction rule for == using ==> not meta-hyps.
   1.174 +   Introduction rule for == as a meta-theorem.  
   1.175  *)
   1.176  val equal_intr_rule =
   1.177 -  let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
   1.178 -      and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   1.179 +  let val PQ = read_prop "PROP phi ==> PROP psi"
   1.180 +      and QP = read_prop "PROP psi ==> PROP phi"
   1.181    in
   1.182      store_thm "equal_intr_rule"
   1.183        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))