isabelle: src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML@af2932baf068 (annotated)

16152 7294283b0c45 no_tac; wenzelm parents: 15570 diff changeset	1
7294283b0c45 no_tac; wenzelm parents: 15570 diff changeset	2	(* $Id$ *)
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	3
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	4	(* call_sim_tac invokes oracle "Sim" *)
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	5	fun call_sim_tac thm_list i state =
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	6	let val sign = #sign (rep_thm state);
15570 8d8c70b41bab Move towards standard functions. skalberg parents: 7299 diff changeset	7	val (subgoal::_) = Library.drop(i-1,prems_of state);
17241 62bb8dcc316e simplified oracle; wenzelm parents: 16152 diff changeset	8	val OraAss = sim_oracle sign (subgoal,thm_list);
19741 f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	9	in cut_facts_tac [OraAss] i state end;
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	10
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	11
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	12	val ioa_implements_def = thm "ioa_implements_def";
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	13
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	14	(* is_sim_tac makes additionally to call_sim_tac some simplifications,
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	15	which are suitable for implementation realtion formulas *)
19741 f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	16	fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	17	EVERY [REPEAT (etac thin_rl i),
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	18	simp_tac (simpset() addsimps [ioa_implements_def]) i,
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	19	rtac conjI i,
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	20	rtac conjI (i+1),
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	21	TRY(call_sim_tac thm_list (i+2)),
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	22	TRY(atac (i+2)),
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	23	REPEAT(rtac refl (i+2)),
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	24	simp_tac (simpset() addsimps (thm_list @
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	25	comp_simps @ restrict_simps @ hide_simps @
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	26	rename_simps @ ioa_simps @ asig_simps)) (i+1),
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	27	simp_tac (simpset() addsimps (thm_list @
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	28	comp_simps @ restrict_simps @ hide_simps @
f65265d71426 removed legacy ML scripts; wenzelm parents: 17241 diff changeset	29	rename_simps @ ioa_simps @ asig_simps)) (i)]);

author	wenzelm
	Tue, 28 Nov 2006 00:35:21 +0100
changeset 21566	af2932baf068
parent 19741	f65265d71426
child 22596	d0d2af4db18f
permissions	-rw-r--r--