isabelle: src/HOLCF/IOA/NTP/Abschannel.ML@0b2ff9541727 (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Abschannel.ML
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 5068 diff changeset	3	Author: Olaf M�ller
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 5068 diff changeset	5	Derived rules.
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	val unfold_renaming =
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	[srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def,
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def,
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	11	actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def,
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	trans_of_def] @ asig_projections;
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	14	Goal
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	"S_msg(m) ~: actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	\ R_msg(m) ~: actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	\ S_pkt(pkt) : actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	\ R_pkt(pkt) : actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	\ S_ack(b) ~: actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20	\ R_ack(b) ~: actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21	\ C_m_s ~: actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22	\ C_m_r ~: actions(srch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	\ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	25	by (simp_tac (simpset() addsimps unfold_renaming) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	qed"in_srch_asig";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	28	Goal
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29	"S_msg(m) ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	\ R_msg(m) ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	\ S_pkt(pkt) ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32	\ R_pkt(pkt) ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	\ S_ack(b) : actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	\ R_ack(b) : actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	\ C_m_s ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36	\ C_m_r ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	\ C_r_s ~: actions(rsch_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38	\ C_r_r(m) ~: actions(rsch_asig)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	39
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	40	by (simp_tac (simpset() addsimps unfold_renaming) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41	qed"in_rsch_asig";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	42
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	43	Goal "srch_ioa = \
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	44	\ (srch_asig, {{\|}}, srch_trans,srch_wfair,srch_sfair)";
4098 71e05eb27fb6 isatool fixclasimp; wenzelm parents: 3523 diff changeset	45	by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	46	wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1);
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	47	by (simp_tac (simpset() addsimps unfold_renaming) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	48	qed"srch_ioa_thm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	49
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	50	Goal "rsch_ioa = \
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	51	\ (rsch_asig, {{\|}}, rsch_trans,rsch_wfair,rsch_sfair)";
4098 71e05eb27fb6 isatool fixclasimp; wenzelm parents: 3523 diff changeset	52	by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	53	wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	54	by (simp_tac (simpset() addsimps unfold_renaming) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	55	qed"rsch_ioa_thm";

author	wenzelm
	Sat, 03 Sep 2005 16:50:22 +0200
changeset 17244	0b2ff9541727
parent 14981	e73f8140af78
child 19360	f47412f922ab
permissions	-rw-r--r--