isabelle: src/HOLCF/IOA/Modelcheck/Ring3.ML@743b22579a2f (annotated)

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	(*
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	12	FIXME
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	13	by (is_sim_tac aut_simps 1);
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	14	by Auto_tac;
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	15	qed"at_most_one_leader";
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	16	*)

author	wenzelm
	Thu, 19 Aug 1999 21:49:10 +0200
changeset 7299	743b22579a2f
parent 6471	08d12ef5fc19
child 7310	298b0dcadf2e
permissions	-rw-r--r--