isabelle: src/HOLCF/IOA/ex/TrivEx.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	Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	25	by (rtac AbsRuleT1 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	26	by (rtac h_abs_is_abstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	27	by (rtac MC_result 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	29	by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	30	qed"TrivEx_abstraction";
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

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