isabelle: src/HOLCF/IOA/ex/TrivEx2.ML@213dcc39358f (annotated)

6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/TrivEx.thy
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 8600 diff changeset	3	Author: Olaf M�ller
6597093b77e7 GPLed; wenzelm parents: 8600 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	5
12218 6597093b77e7 GPLed; wenzelm parents: 8600 diff changeset	6	Trivial Abstraction Example.
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	7	*)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	8
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	9	Goalw [is_abstraction_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	10	"is_abstraction h_abs C_ioa A_ioa";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	11	by (rtac conjI 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	12	(* ------------- start states ------------ *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	13	by (simp_tac (simpset() addsimps
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	14	[h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	15	(* -------------- step case ---------------- *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	16	by (REPEAT (rtac allI 1));
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	17	by (rtac imp_conj_lemma 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	18	by (simp_tac (simpset() addsimps [trans_of_def,
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	19	C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
8600 a466c687c726 mods because of weak_case_cong nipkow parents: 6470 diff changeset	20	by (induct_tac "a" 1);
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	21	by (simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	22	qed"h_abs_is_abstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	23
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	24
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	25	(*
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	26	Goalw [xt2_def,plift,option_lift]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	27	"(xt2 (plift afun)) (s,a,t) = (afun a)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28	(* !!!!!!!!!!!!! Occurs check !!!! *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	29	by (induct_tac "a" 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	30
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	31	*)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	32
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	33	Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	34	C_trans_def,trans_of_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	35	"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	36	by Auto_tac;
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	37	qed"Enabled_implication";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	38
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	39
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	40	Goalw [is_live_abstraction_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	41	"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	42	by Auto_tac;
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	43	(* is_abstraction *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	44	by (rtac h_abs_is_abstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	45	(* temp_weakening *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	46	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	47	by (etac Enabled_implication 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	48	qed"h_abs_is_liveabstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	49
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	50
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	51	Goalw [C_live_ioa_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	52	"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	53	by (rtac AbsRuleT2 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	54	by (rtac h_abs_is_liveabstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	55	by (rtac MC_result 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	56	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	57	by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	58	qed"TrivEx2_abstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	59
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	60
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	61	(*
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	62	Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR))))
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	63	IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	64
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	65	*)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	66

author	kleing
	Tue, 13 May 2003 08:59:21 +0200
changeset 14024	213dcc39358f
parent 13524	604d0f3622d6
child 14981	e73f8140af78
permissions	-rw-r--r--