# HG changeset patch
# User nipkow
# Date 843548364 -7200
# Node ID bcd69cc47cf03202ee591947ab32f08cca281d1a
# Parent  dd3e2a91aeca8e27423931398ccc1f3c93df3321
Moved Option into core HOL which caused a few local changes.

diff -r dd3e2a91aeca -r bcd69cc47cf0 src/HOL/IOA/meta_theory/Asig.thy
--- a/src/HOL/IOA/meta_theory/Asig.thy	Mon Sep 23 18:26:51 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Asig.thy	Tue Sep 24 08:59:24 1996 +0200
@@ -6,7 +6,7 @@
 Action signatures
 *)
 
-Asig = Option +
+Asig = Prod +
 
 types 
 
diff -r dd3e2a91aeca -r bcd69cc47cf0 src/HOL/IOA/meta_theory/IOA.ML
--- a/src/HOL/IOA/meta_theory/IOA.ML	Mon Sep 23 18:26:51 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Tue Sep 24 08:59:24 1996 +0200
@@ -6,6 +6,8 @@
 The I/O automata of Lynch and Tuttle.
 *)
 
+Addsimps [Let_def];
+
 open IOA Asig;
 
 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
@@ -81,7 +83,7 @@
   by (nat_ind_tac "n" 1);
   by (fast_tac (!claset addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","n1")]allE 1);
-  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1);
+  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optionE 1);
   by (Asm_simp_tac 1);
   by (safe_tac (!claset));
   by (etac (p2 RS mp) 1);
diff -r dd3e2a91aeca -r bcd69cc47cf0 src/HOL/IOA/meta_theory/IOA.thy
--- a/src/HOL/IOA/meta_theory/IOA.thy	Mon Sep 23 18:26:51 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.thy	Tue Sep 24 08:59:24 1996 +0200
@@ -6,7 +6,7 @@
 The I/O automata of Lynch and Tuttle.
 *)
 
-IOA = Asig +
+IOA = Asig + Option +
 
 types
    'a seq            =   "nat => 'a"
diff -r dd3e2a91aeca -r bcd69cc47cf0 src/HOL/IOA/meta_theory/Option.ML
--- a/src/HOL/IOA/meta_theory/Option.ML	Mon Sep 23 18:26:51 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      Option.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994  TU Muenchen
-
-Derived rules
-*)
-
-Addsimps [Let_def];
-
-val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
- br (prem RS rev_mp) 1;
- by (Option.option.induct_tac "opt" 1);
- by (ALLGOALS(Fast_tac));
-val optE = store_thm("optE", standard(result() RS disjE));
-
-goal Option.thy "x=None | (? y.x=Some(y))"; 
-by (Option.option.induct_tac "x" 1);
-by (Asm_full_simp_tac 1);
-by (rtac disjI2 1);
-by (rtac exI 1);
-by (Asm_full_simp_tac 1);
-qed"opt_cases";
diff -r dd3e2a91aeca -r bcd69cc47cf0 src/HOL/IOA/meta_theory/Option.thy
--- a/src/HOL/IOA/meta_theory/Option.thy	Mon Sep 23 18:26:51 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  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 dd3e2a91aeca -r bcd69cc47cf0 src/HOL/IOA/meta_theory/Solve.ML
--- a/src/HOL/IOA/meta_theory/Solve.ML	Mon Sep 23 18:26:51 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Tue Sep 24 08:59:24 1996 +0200
@@ -75,25 +75,13 @@
  by (Simp_tac 1);
  by (Fast_tac 1);
 (* projected execution is indeed an execution *)
-by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
-    par_def, starts_of_def,trans_of_def]) 1);
-by (simp_tac (!simpset addsimps [filter_oseq_def]) 1);
- by (REPEAT(rtac allI 1));
- by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
- by (etac disjE 1);
-(* case 1: action sequence of || had already a None *)
-by (Asm_full_simp_tac 1);
- by (REPEAT(etac exE 1));
- by (case_tac "y:actions(asig_of(C1))" 1);
-(* case 2: action sequence of || had Some(a) and 
-           filtered sequence also       *)
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac
+      (!simpset addsimps [executions_def,is_execution_fragment_def,
+                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
+                setloop (split_tac[expand_if,expand_option_case])) 1);
  by (strip_tac 1);
  by (REPEAT(hyp_subst_tac 1)); 
  by (Asm_full_simp_tac 1);
-(* case 3: action sequence pf || had Some(a) but
-           filtered sequence has None      *)
- by (Asm_full_simp_tac 1);
 qed"comp1_reachable";
 
 
@@ -110,20 +98,13 @@
  by (Simp_tac 1);
  by (Fast_tac 1);
 (* projected execution is indeed an execution *)
- by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
-    par_def, starts_of_def,trans_of_def]) 1);
- by (simp_tac (!simpset addsimps [filter_oseq_def]) 1);
- by (REPEAT(rtac allI 1));
- by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
- by (etac disjE 1);
- by (Asm_full_simp_tac 1);
- by (REPEAT(etac exE 1));
- by (case_tac "y:actions(asig_of(C2))" 1);
- by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac
+      (!simpset addsimps [executions_def,is_execution_fragment_def,
+                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
+                setloop (split_tac[expand_if,expand_option_case])) 1);
  by (strip_tac 1);
  by (REPEAT(hyp_subst_tac 1)); 
  by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
 qed"comp2_reachable";
 
 
@@ -183,11 +164,11 @@
 \          | Some(x) => g x) ,snd ex)")]  bexI 1);
 by (Simp_tac 1);
 (* execution is indeed an execution of C *)
-by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
-    par_def, starts_of_def,trans_of_def,rename_def]) 1);
-by (REPEAT(rtac allI 1));
-by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
-by (Auto_tac());
+by (asm_full_simp_tac
+      (!simpset addsimps [executions_def,is_execution_fragment_def,
+                          par_def,starts_of_def,trans_of_def,rename_def]
+                setloop (split_tac[expand_option_case])) 1);
+by(Auto_tac());
 qed"reachable_rename_ioa";