Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/Modelcheck/Ring3.ML
author nipkow
Mon, 13 May 2002 15:27:28 +0200
changeset 13145 59bc43b51aa2
parent 7310 298b0dcadf2e
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7299
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset 
     1
 







6471






08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




     2


val aut_simps = [Greater_def,one_leader_def,








7299






743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




     3


  one_leader_asig_def,one_leader_trans_def,one_leader_initial_def,













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




     4


  ring_def,aut0_asig_def,aut0_trans_def,aut0_initial_def,aut0_def,













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




     5


  aut1_asig_def,aut1_trans_def,aut1_initial_def,aut1_def,













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




     6


  aut2_asig_def,aut2_trans_def,aut2_initial_def,aut2_def];








6471






08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




     7














08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




     8


(* property to prove: at most one (of 3) members of the ring will













08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




     9


	declare itself to leader *)








7299






743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    10


Goal "ring =<| one_leader";













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    11


by (is_sim_tac aut_simps 1); 








6471






08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




    12


by Auto_tac;













08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




    13


qed"at_most_one_leader";















isabelle