src/Pure/drule.ML
changeset 9554 1b0f02abbde8
parent 9547 8dad21f06b24
child 9829 bf49c3796599
     1.1 --- a/src/Pure/drule.ML	Tue Aug 08 01:17:59 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Aug 08 01:26:34 2000 +0200
     1.3 @@ -29,6 +29,7 @@
     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 forall_elim_vars_safe  : thm -> thm
     1.8    val freeze_thaw       : thm -> thm * (thm -> thm)
     1.9    val implies_elim_list : thm -> thm list -> thm
    1.10    val implies_intr_list : cterm list -> thm -> thm
    1.11 @@ -99,6 +100,7 @@
    1.12    val has_internal	: tag list -> bool
    1.13    val compose_single    : thm * int * thm -> thm
    1.14    val merge_rules	: thm list * thm list -> thm list
    1.15 +  val norm_hhf_eq	: thm
    1.16    val triv_goal         : thm
    1.17    val rev_triv_goal     : thm
    1.18    val freeze_all        : thm -> thm
    1.19 @@ -283,6 +285,11 @@
    1.20  val forall_elim_var = PureThy.forall_elim_var;
    1.21  val forall_elim_vars = PureThy.forall_elim_vars;
    1.22  
    1.23 +fun forall_elim_vars_safe th =
    1.24 +  forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th)
    1.25 +    handle THM _ => th;
    1.26 +
    1.27 +
    1.28  (*Specialization over a list of cterms*)
    1.29  fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
    1.30  
    1.31 @@ -492,9 +499,9 @@
    1.32  fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
    1.33  
    1.34  (*Rewrite a theorem*)
    1.35 -fun rewrite_rule_aux _ []   th = th
    1.36 -  | rewrite_rule_aux prover thms th =
    1.37 -      fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
    1.38 +fun rewrite_rule_aux _ [] = (fn th => th)
    1.39 +  | rewrite_rule_aux prover thms =
    1.40 +      fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms));
    1.41  
    1.42  fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
    1.43  fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
    1.44 @@ -580,6 +587,43 @@
    1.45    end;
    1.46  
    1.47  
    1.48 +(*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
    1.49 +  Rewrite rule for HHF normalization.
    1.50 +
    1.51 +  Note: the syntax of ProtoPure is insufficient to handle this
    1.52 +  statement; storing it would be asking for trouble, e.g. when someone
    1.53 +  tries to print the theory later.
    1.54 +*)
    1.55 +
    1.56 +val norm_hhf_eq =
    1.57 +  let
    1.58 +    val cert = Thm.cterm_of proto_sign;
    1.59 +    val aT = TFree ("'a", Term.logicS);
    1.60 +    val all = Term.all aT;
    1.61 +    val x = Free ("x", aT);
    1.62 +    val phi = Free ("phi", propT);
    1.63 +    val psi = Free ("psi", aT --> propT);
    1.64 +
    1.65 +    val cx = cert x;
    1.66 +    val cphi = cert phi;
    1.67 +    val lhs = cert (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0)));
    1.68 +    val rhs = cert (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0)));
    1.69 +  in
    1.70 +    Thm.equal_intr
    1.71 +      (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi)
    1.72 +        |> Thm.forall_elim cx
    1.73 +        |> Thm.implies_intr cphi
    1.74 +        |> Thm.forall_intr cx
    1.75 +        |> Thm.implies_intr lhs)
    1.76 +      (Thm.implies_elim
    1.77 +          (Thm.assume rhs |> Thm.forall_elim cx) (Thm.assume cphi)
    1.78 +        |> Thm.forall_intr cx
    1.79 +        |> Thm.implies_intr cphi
    1.80 +        |> Thm.implies_intr rhs)
    1.81 +    |> standard |> curry Thm.name_thm "ProtoPure.norm_hhf_eq"
    1.82 +  end;
    1.83 +
    1.84 +
    1.85  (*** Instantiate theorem th, reading instantiations under signature sg ****)
    1.86  
    1.87  (*Version that normalizes the result: Thm.instantiate no longer does that*)