isabelle: src/HOLCF/IOA/ex/TrivEx.ML@772ac061bd76 (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);
8600 a466c687c726 mods because of weak_case_cong nipkow parents: 6470 diff changeset	25	by (induct_tac "a" 1);
6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	26	by (simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	27	qed"h_abs_is_abstraction";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	28
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	Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	31	by (rtac AbsRuleT1 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	32	by (rtac h_abs_is_abstraction 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	33	by (rtac MC_result 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	34	by (abstraction_tac 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	35	by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	36	qed"TrivEx_abstraction";
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

author	paulson
	Fri, 25 Aug 2000 12:15:35 +0200
changeset 9687	772ac061bd76
parent 8600	a466c687c726
child 12218	6597093b77e7
permissions	-rw-r--r--