isabelle: src/HOLCF/IOA/ex/TrivEx.ML@a901bafe4578 (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$
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	3	Author: Olaf Mueller
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	4	Copyright 1995 TU Muenchen
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	5
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	6	Trivial Abstraction Example
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	val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	10	by (fast_tac (claset() addDs prems) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	11	qed "imp_conj_lemma";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	12
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	13
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	14	Goalw [is_abstraction_def]
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	15	"is_abstraction h_abs C_ioa A_ioa";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	16	by (rtac conjI 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	17	(* ------------- start states ------------ *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	18	by (simp_tac (simpset() addsimps
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	19	[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	20	(* -------------- step case ---------------- *)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	21	by (REPEAT (rtac allI 1));
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	22	by (rtac imp_conj_lemma 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	23	by (simp_tac (simpset() addsimps [trans_of_def,
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	24	C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	25	by (simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	26	by (induct_tac "a" 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	27	by Auto_tac;
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28	qed"h_abs_is_abstraction";
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	Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	32	by (rtac AbsRuleT1 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	33	by (rtac h_abs_is_abstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	34	by (rtac MC_result 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	35	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	36	by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	37	qed"TrivEx_abstraction";
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

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 6470	f3015fd68d66
child 8600	a466c687c726
permissions	-rw-r--r--