the is now defined using primrec, avoiding explicit use of arbitrary.
authorberghofe
Tue May 30 18:02:49 2000 +0200 (2000-05-30)
changeset 900193af64f54bf2
parent 9000 c20d58286a51
child 9002 a752f2499dae
the is now defined using primrec, avoiding explicit use of arbitrary.
src/HOL/Option.ML
src/HOL/Option.thy
     1.1 --- a/src/HOL/Option.ML	Tue May 30 16:08:38 2000 +0200
     1.2 +++ b/src/HOL/Option.ML	Tue May 30 18:02:49 2000 +0200
     1.3 @@ -42,16 +42,6 @@
     1.4  qed "option_caseE";
     1.5  
     1.6  
     1.7 -section "the";
     1.8 -
     1.9 -Goalw [the_def] "the (Some x) = x";
    1.10 -by (Simp_tac 1);
    1.11 -qed "the_Some";
    1.12 -
    1.13 -Addsimps [the_Some];
    1.14 -
    1.15 -
    1.16 -
    1.17  section "option_map";
    1.18  
    1.19  Goalw [option_map_def] "option_map f None = None";
     2.1 --- a/src/HOL/Option.thy	Tue May 30 16:08:38 2000 +0200
     2.2 +++ b/src/HOL/Option.thy	Tue May 30 18:02:49 2000 +0200
     2.3 @@ -10,21 +10,19 @@
     2.4  
     2.5  datatype 'a option = None | Some 'a
     2.6  
     2.7 -constdefs
     2.8 +consts
     2.9 +  the :: "'a option => 'a"
    2.10 +  o2s :: "'a option => 'a set"
    2.11  
    2.12 -  the		:: "'a option => 'a"
    2.13 - "the == %y. case y of None => arbitrary | Some x => x"
    2.14 +primrec
    2.15 + "the (Some x) = x"
    2.16  
    2.17 +primrec
    2.18 + "o2s  None    = {}"
    2.19 + "o2s (Some x) = {x}"
    2.20 +
    2.21 +constdefs
    2.22    option_map	:: "('a => 'b) => ('a option => 'b option)"
    2.23   "option_map == %f y. case y of None => None | Some x => Some (f x)"
    2.24  
    2.25 -consts
    2.26 -
    2.27 -  o2s	   :: "'a option => 'a set"
    2.28 -
    2.29 -primrec
    2.30 -
    2.31 - "o2s  None    = {}"
    2.32 - "o2s (Some x) = {x}"
    2.33 -
    2.34  end