# HG changeset patch
# User nipkow
# Date 843548554 -7200
# Node ID b45d9f2042e050c9e25461f25c3a3372181e3a0f
# Parent  bcd69cc47cf03202ee591947ab32f08cca281d1a
Moved Option out of IOA into core HOL

diff -r bcd69cc47cf0 -r b45d9f2042e0 src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Sep 24 08:59:24 1996 +0200
+++ b/src/HOL/Makefile	Tue Sep 24 09:02:34 1996 +0200
@@ -23,7 +23,7 @@
 COMP = $(ISABELLECOMP)
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
         mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
-        Sexp Univ List RelPow
+        Sexp Univ List RelPow Option
 
 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
 	ind_syntax.ML cladata.ML simpdata.ML\
@@ -111,7 +111,7 @@
 IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
                 Receiver Sender
 IOA_ABP_NAMES = Action Correctness Lemmas
-IOA_MT_NAMES = Asig IOA Option Solve
+IOA_MT_NAMES = Asig IOA Solve
 
 IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy\
  $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML)\
diff -r bcd69cc47cf0 -r b45d9f2042e0 src/HOL/Option.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Option.ML	Tue Sep 24 09:02:34 1996 +0200
@@ -0,0 +1,31 @@
+(*  Title:      Option.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996  TU Muenchen
+
+Derived rules
+*)
+
+open Option;
+
+val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
+ br (prem RS rev_mp) 1;
+ by (option.induct_tac "opt" 1);
+ by (ALLGOALS(Fast_tac));
+bind_thm("optionE", standard(result() RS disjE));
+(*
+goal Option.thy "opt=None | (? x.opt=Some(x))"; 
+by (option.induct_tac "opt" 1);
+by (Simp_tac 1);
+by (rtac disjI2 1);
+by (rtac exI 1);
+by (Asm_full_simp_tac 1);
+qed"option_cases";
+*)
+goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
+\                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
+by (option.induct_tac "opt" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by(Fast_tac 1);
+qed"expand_option_case";
diff -r bcd69cc47cf0 -r b45d9f2042e0 src/HOL/Option.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Option.thy	Tue Sep 24 09:02:34 1996 +0200
@@ -0,0 +1,11 @@
+(*  Title:      Option.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1994  TU Muenchen
+
+Datatype 'a option
+*)
+
+Option = Arith +
+datatype 'a option = None | Some 'a
+end
diff -r bcd69cc47cf0 -r b45d9f2042e0 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Sep 24 08:59:24 1996 +0200
+++ b/src/HOL/ROOT.ML	Tue Sep 24 09:02:34 1996 +0200
@@ -38,6 +38,7 @@
 use_thy "RelPow";
 use_thy "Finite";
 use_thy "Sexp";
+use_thy "Option";
 use_thy "List";
 
 init_pps ();