isabelle: src/HOL/IOA/meta_theory/Option.ML@e044350bfa52 (annotated)

966 3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	1	(* Title: Option.ML
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	2	ID: $Id$
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	4	Copyright 1994 TU Muenchen
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	5
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	6	Derived rules
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	7	*)
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	8
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	9	val option_rws = Let_def :: Option.option.simps;
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	10	val SS = arith_ss addsimps option_rws;
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	11
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	12	val [prem] = goal Option.thy "P(opt) ==> P(None) \| (? x. P(Some(x)))";
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	13	br (prem RS rev_mp) 1;
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	14	by (Option.option.induct_tac "opt" 1);
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	15	by (ALLGOALS(fast_tac HOL_cs));
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	16	val optE = store_thm("optE", standard(result() RS disjE));
1052 e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	17
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	18	goal Option.thy "x=None \| (? y.x=Some(y))";
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	19	by (Option.option.induct_tac "x" 1);
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	20	by (asm_full_simp_tac list_ss 1);
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	21	by (rtac disjI2 1);
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	22	by (rtac exI 1);
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	23	by (asm_full_simp_tac list_ss 1);
e044350bfa52 Olafs new version. nipkow parents: 966 diff changeset	24	qed"opt_cases";

author	nipkow
	Thu, 13 Apr 1995 17:05:41 +0200
changeset 1052	e044350bfa52
parent 966	3fd66f245ad7
child 1266	3ae9fe3c0f68
permissions	-rw-r--r--