isabelle: src/HOLCF/IOA/ex/TrivEx2.ML@e73f8140af78 (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
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 8600 diff changeset	5	Trivial Abstraction Example.
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	6	*)
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	Goalw [is_abstraction_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	9	"is_abstraction h_abs C_ioa A_ioa";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	10	by (rtac conjI 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	11	(* ------------- start states ------------ *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	12	by (simp_tac (simpset() addsimps
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	13	[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	14	(* -------------- step case ---------------- *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	15	by (REPEAT (rtac allI 1));
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	16	by (rtac imp_conj_lemma 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	17	by (simp_tac (simpset() addsimps [trans_of_def,
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	18	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	19	by (induct_tac "a" 1);
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	20	by (simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	21	qed"h_abs_is_abstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	22
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	Goalw [xt2_def,plift,option_lift]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	26	"(xt2 (plift afun)) (s,a,t) = (afun a)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	27	(* !!!!!!!!!!!!! Occurs check !!!! *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28	by (induct_tac "a" 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	29
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	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	33	C_trans_def,trans_of_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	34	"!!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	35	by Auto_tac;
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	36	qed"Enabled_implication";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	37
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	Goalw [is_live_abstraction_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	40	"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	41	by Auto_tac;
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	42	(* is_abstraction *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	43	by (rtac h_abs_is_abstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	44	(* temp_weakening *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	45	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	46	by (etac Enabled_implication 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	47	qed"h_abs_is_liveabstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	48
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	Goalw [C_live_ioa_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	51	"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	52	by (rtac AbsRuleT2 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	53	by (rtac h_abs_is_liveabstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	54	by (rtac MC_result 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	55	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	56	by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	57	qed"TrivEx2_abstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	58
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	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	62	IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	63
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

author	kleing
	Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981	e73f8140af78
parent 13524	604d0f3622d6
child 19360	f47412f922ab
permissions	-rw-r--r--