moved a theorem
authorpaulson
Mon Oct 19 11:25:37 1998 +0200 (1998-10-19)
changeset 56689ddc4e836d3e
parent 5667 2df6fccf5719
child 5669 f5d9caafc3bd
moved a theorem
src/HOL/UNITY/Comp.ML
     1.1 --- a/src/HOL/UNITY/Comp.ML	Mon Oct 19 11:24:55 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.ML	Mon Oct 19 11:25:37 1998 +0200
     1.3 @@ -100,6 +100,12 @@
     1.4  
     1.5  (*** guarantees ***)
     1.6  
     1.7 +(*This equation is more intuitive than the official definition*)
     1.8 +Goalw [guarantees_def, component_def]
     1.9 +      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
    1.10 +by (Blast_tac 1);
    1.11 +qed "guarantees_eq";
    1.12 +
    1.13  Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
    1.14  by (Blast_tac 1);
    1.15  qed "subset_imp_guarantees";
    1.16 @@ -148,11 +154,6 @@
    1.17  by (Blast_tac 1);
    1.18  qed "ex_guarantees";
    1.19  
    1.20 -Goalw [guarantees_def, component_def]
    1.21 -      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
    1.22 -by (Blast_tac 1);
    1.23 -qed "guarantees_eq";
    1.24 -
    1.25  val prems = Goalw [guarantees_def, component_def]
    1.26        "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
    1.27  by (blast_tac (claset() addIs prems) 1);