isabelle: src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy@83b373f61d41 (annotated)

7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	1
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	2	(* $Id$ *)
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	3
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	4	theory MuIOAOracle
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	5	imports MuIOA
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	6	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	7
28290 4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	8	oracle sim_oracle = mk_sim_oracle
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	9
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	10	ML {*
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	11	(* call_sim_tac invokes oracle "Sim" *)
28290 4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	12	fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) =>
4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	13	let val OraAss = sim_oracle (csubgoal,thm_list);
4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	14	in cut_facts_tac [OraAss] i end);
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	15
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	16
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	17	val ioa_implements_def = thm "ioa_implements_def";
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	18
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	19	(* is_sim_tac makes additionally to call_sim_tac some simplifications,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	20	which are suitable for implementation realtion formulas *)
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	21	fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	22	EVERY [REPEAT (etac thin_rl i),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	23	simp_tac (simpset() addsimps [ioa_implements_def]) i,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	24	rtac conjI i,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	25	rtac conjI (i+1),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	26	TRY(call_sim_tac thm_list (i+2)),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	27	TRY(atac (i+2)),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	28	REPEAT(rtac refl (i+2)),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	29	simp_tac (simpset() addsimps (thm_list @
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	30	comp_simps @ restrict_simps @ hide_simps @
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	31	rename_simps @ ioa_simps @ asig_simps)) (i+1),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	32	simp_tac (simpset() addsimps (thm_list @
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	33	comp_simps @ restrict_simps @ hide_simps @
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	34	rename_simps @ ioa_simps @ asig_simps)) (i)]);
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	35
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	36	*}
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	37
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	38	end

author	haftmann
	Mon, 16 Feb 2009 19:11:55 +0100
changeset 29940	83b373f61d41
parent 28290	4cc2b6046258
child 30609	983e8b6e4e69
permissions	-rw-r--r--