isabelle: src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy@05c384cb1181 (annotated)

17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	1	theory MuIOAOracle
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	2	imports MuIOA
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	3	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	4
28290 4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	5	oracle sim_oracle = mk_sim_oracle
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	6
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	7	ML {*
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	8	(* call_sim_tac invokes oracle "Sim" *)
28290 4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	9	fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) =>
4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	10	let val OraAss = sim_oracle (csubgoal,thm_list);
4cc2b6046258 simplified oracle interface; wenzelm parents: 22819 diff changeset	11	in cut_facts_tac [OraAss] i end);
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	12
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	13
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	14	val ioa_implements_def = thm "ioa_implements_def";
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	15
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	16	(* is_sim_tac makes additionally to call_sim_tac some simplifications,
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	17	which are suitable for implementation realtion formulas *)
30609 983e8b6e4e69 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory; wenzelm parents: 28290 diff changeset	18	fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) =>
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	19	EVERY [REPEAT (etac thin_rl i),
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	20	simp_tac (ss addsimps [ioa_implements_def]) i,
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	21	rtac conjI i,
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	22	rtac conjI (i+1),
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	23	TRY(call_sim_tac thm_list (i+2)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	24	TRY(atac (i+2)),
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	25	REPEAT(rtac refl (i+2)),
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	26	simp_tac (ss addsimps (thm_list @
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	27	comp_simps @ restrict_simps @ hide_simps @
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	28	rename_simps @ ioa_simps @ asig_simps)) (i+1),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	29	simp_tac (ss addsimps (thm_list @
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	30	comp_simps @ restrict_simps @ hide_simps @
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 30609 diff changeset	31	rename_simps @ ioa_simps @ asig_simps)) (i)]);
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	32
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	33	*}
a7b425bb668c removed legacy ML files; wenzelm parents: 17244 diff changeset	34
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	35	end

author	berghofe
	Sun, 08 Nov 2009 15:45:09 +0100
changeset 33525	05c384cb1181
parent 32960	69916a850301
permissions	-rw-r--r--