three new theorems
authorpaulson
Mon Aug 06 13:12:06 2001 +0200 (2001-08-06)
changeset 1146396b5b27da55c
parent 11462 cf3e7f5ad0e1
child 11464 ddea204de5bc
three new theorems
src/HOL/Auth/Event.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Mon Aug 06 12:46:21 2001 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon Aug 06 13:12:06 2001 +0200
     1.3 @@ -79,6 +79,22 @@
     1.4  		      | Notes A X  => parts {X} Un (used evs))"
     1.5  
     1.6  
     1.7 +lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
     1.8 +apply (induct_tac evs);
     1.9 +apply (auto split: event.split) 
    1.10 +done
    1.11 +
    1.12 +lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
    1.13 +apply (induct_tac evs);
    1.14 +apply (auto split: event.split) 
    1.15 +done
    1.16 +
    1.17 +lemma MPair_used [rule_format]:
    1.18 +     "MPair X Y : used evs --> X : used evs & Y : used evs"
    1.19 +apply (induct_tac evs);
    1.20 +apply (auto split: event.split) 
    1.21 +done
    1.22 +
    1.23  use "Event_lemmas.ML"
    1.24  
    1.25  method_setup analz_mono_contra = {*