src/HOLCF/IOA/meta_theory/TL.ML
changeset 4577 674b0b354feb
parent 4559 8e604d885b54
child 4681 a331c1f5a23e
     1.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Wed Jan 14 11:22:03 1998 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Wed Jan 14 16:38:04 1998 +0100
     1.3 @@ -113,6 +113,8 @@
     1.4  be STL1b 1;
     1.5  qed"STL1";
     1.6  
     1.7 +
     1.8 +
     1.9  (* Note that unlift and HD is not at all used !!! *)
    1.10  goal thy "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
    1.11  by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
    1.12 @@ -177,3 +179,13 @@
    1.13  auto();
    1.14  
    1.15  
    1.16 +
    1.17 +
    1.18 +goal thy "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
    1.19 +by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
    1.20 +qed"ModusPonens";
    1.21 +
    1.22 +(* works only if validT is defined without restriction to s~=UU, s~=nil *)
    1.23 +goal thy "!! P. validT P ==> validT (Next P)";
    1.24 +by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
    1.25 +(* qed"NextTauto"; *)
    1.26 \ No newline at end of file