isabelle: src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy@6f79698f294d (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
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	8	oracle sim_oracle ("term * thm list") =
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	9	mk_sim_oracle
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	10
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	11	ML {*
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	12	(* call_sim_tac invokes oracle "Sim" *)
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	13	fun call_sim_tac thm_list i state =
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	14	let val thy = Thm.theory_of_thm state;
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	15	val (subgoal::_) = Library.drop(i-1,prems_of state);
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	16	val OraAss = sim_oracle thy (subgoal,thm_list);
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	17	in cut_facts_tac [OraAss] i state end;
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	18
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	19
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	20	val ioa_implements_def = thm "ioa_implements_def";
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	21
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	22	(* is_sim_tac makes additionally to call_sim_tac some simplifications,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	23	which are suitable for implementation realtion formulas *)
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	24	fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	25	EVERY [REPEAT (etac thin_rl i),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	26	simp_tac (simpset() addsimps [ioa_implements_def]) i,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	27	rtac conjI i,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	28	rtac conjI (i+1),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	29	TRY(call_sim_tac thm_list (i+2)),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	30	TRY(atac (i+2)),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	31	REPEAT(rtac refl (i+2)),
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+1),
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	35	simp_tac (simpset() addsimps (thm_list @
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	36	comp_simps @ restrict_simps @ hide_simps @
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	37	rename_simps @ ioa_simps @ asig_simps)) (i)]);
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	38
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	39	*}
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	40
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	41	end

author	wenzelm
	Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456	6f79698f294d
parent 22819	a7b425bb668c
child 28290	4cc2b6046258
permissions	-rw-r--r--