re-eliminated Option.thy
authorhaftmann
Thu Aug 09 15:52:42 2007 +0200 (2007-08-09)
changeset 2419496013f81faef
parent 24193 926dde4d96de
child 24195 7d1a16c77f7c
re-eliminated Option.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Table.thy
src/HOL/Datatype.thy
src/HOL/Extraction.thy
src/HOL/Finite_Set.thy
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Option.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Aug 09 15:52:38 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Aug 09 15:52:42 2007 +0200
     1.3 @@ -236,7 +236,7 @@
     1.4  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
     1.5  
     1.6  translations
     1.7 -  "option"<= (type) "Option.option"
     1.8 +  "option"<= (type) "Datatype.option"
     1.9    "list"  <= (type) "List.list"
    1.10    "sum3"  <= (type) "Basis.sum3"
    1.11  
     2.1 --- a/src/HOL/Bali/Table.thy	Thu Aug 09 15:52:38 2007 +0200
     2.2 +++ b/src/HOL/Bali/Table.thy	Thu Aug 09 15:52:42 2007 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4  translations
     2.5    "table_of" == "map_of"
     2.6    
     2.7 -  (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Option.option"
     2.8 +  (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
     2.9    (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
    2.10  
    2.11  (* ### To map *)
     3.1 --- a/src/HOL/Datatype.thy	Thu Aug 09 15:52:38 2007 +0200
     3.2 +++ b/src/HOL/Datatype.thy	Thu Aug 09 15:52:42 2007 +0200
     3.3 @@ -539,9 +539,23 @@
     3.4  
     3.5  subsection {* Representing primitive types *}
     3.6  
     3.7 +rep_datatype bool
     3.8 +  distinct True_not_False False_not_True
     3.9 +  induction bool_induct
    3.10 +
    3.11  declare case_split [cases type: bool]
    3.12    -- "prefer plain propositional version"
    3.13  
    3.14 +lemma size_bool [code func]:
    3.15 +  "size (b\<Colon>bool) = 0" by (cases b) auto
    3.16 +
    3.17 +rep_datatype unit
    3.18 +  induction unit_induct
    3.19 +
    3.20 +rep_datatype prod
    3.21 +  inject Pair_eq
    3.22 +  induction prod_induct
    3.23 +
    3.24  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    3.25  
    3.26  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
    3.27 @@ -568,6 +582,14 @@
    3.28  
    3.29  lemmas [code inline] = prod_case_split [symmetric]
    3.30  
    3.31 +rep_datatype sum
    3.32 +  distinct Inl_not_Inr Inr_not_Inl
    3.33 +  inject Inl_eq Inr_eq
    3.34 +  induction sum_induct
    3.35 +
    3.36 +lemma size_sum [code func]:
    3.37 +  "size (x \<Colon> 'a + 'b) = 0" by (cases x) auto
    3.38 +
    3.39  lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    3.40    by (rule ext) (simp split: sum.split)
    3.41  
    3.42 @@ -655,4 +677,125 @@
    3.43      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    3.44    by (cases x) blast
    3.45  
    3.46 +
    3.47 +subsection {* The option datatype *}
    3.48 +
    3.49 +datatype 'a option = None | Some 'a
    3.50 +
    3.51 +lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
    3.52 +  by (induct x) auto
    3.53 +
    3.54 +lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
    3.55 +  by (induct x) auto
    3.56 +
    3.57 +text{*Although it may appear that both of these equalities are helpful
    3.58 +only when applied to assumptions, in practice it seems better to give
    3.59 +them the uniform iff attribute. *}
    3.60 +
    3.61 +lemma option_caseE:
    3.62 +  assumes c: "(case x of None => P | Some y => Q y)"
    3.63 +  obtains
    3.64 +    (None) "x = None" and P
    3.65 +  | (Some) y where "x = Some y" and "Q y"
    3.66 +  using c by (cases x) simp_all
    3.67 +
    3.68 +
    3.69 +subsubsection {* Operations *}
    3.70 +
    3.71 +consts
    3.72 +  the :: "'a option => 'a"
    3.73 +primrec
    3.74 +  "the (Some x) = x"
    3.75 +
    3.76 +consts
    3.77 +  o2s :: "'a option => 'a set"
    3.78 +primrec
    3.79 +  "o2s None = {}"
    3.80 +  "o2s (Some x) = {x}"
    3.81 +
    3.82 +lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
    3.83 +  by simp
    3.84 +
    3.85 +ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
    3.86 +
    3.87 +lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
    3.88 +  by (cases xo) auto
    3.89 +
    3.90 +lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
    3.91 +  by (cases xo) auto
    3.92 +
    3.93 +
    3.94 +constdefs
    3.95 +  option_map :: "('a => 'b) => ('a option => 'b option)"
    3.96 +  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    3.97 +
    3.98 +lemmas [code func del] = option_map_def
    3.99 +
   3.100 +lemma option_map_None [simp, code]: "option_map f None = None"
   3.101 +  by (simp add: option_map_def)
   3.102 +
   3.103 +lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
   3.104 +  by (simp add: option_map_def)
   3.105 +
   3.106 +lemma option_map_is_None [iff]:
   3.107 +    "(option_map f opt = None) = (opt = None)"
   3.108 +  by (simp add: option_map_def split add: option.split)
   3.109 +
   3.110 +lemma option_map_eq_Some [iff]:
   3.111 +    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   3.112 +  by (simp add: option_map_def split add: option.split)
   3.113 +
   3.114 +lemma option_map_comp:
   3.115 +    "option_map f (option_map g opt) = option_map (f o g) opt"
   3.116 +  by (simp add: option_map_def split add: option.split)
   3.117 +
   3.118 +lemma option_map_o_sum_case [simp]:
   3.119 +    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   3.120 +  by (rule ext) (simp split: sum.split)
   3.121 +
   3.122 +
   3.123 +subsubsection {* Code generator setup *}
   3.124 +
   3.125 +definition
   3.126 +  is_none :: "'a option \<Rightarrow> bool" where
   3.127 +  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
   3.128 +
   3.129 +lemma is_none_code [code]:
   3.130 +  shows "is_none None \<longleftrightarrow> True"
   3.131 +    and "is_none (Some x) \<longleftrightarrow> False"
   3.132 +  unfolding is_none_none [symmetric] by simp_all
   3.133 +
   3.134 +hide (open) const is_none
   3.135 +
   3.136 +code_type option
   3.137 +  (SML "_ option")
   3.138 +  (OCaml "_ option")
   3.139 +  (Haskell "Maybe _")
   3.140 +
   3.141 +code_const None and Some
   3.142 +  (SML "NONE" and "SOME")
   3.143 +  (OCaml "None" and "Some _")
   3.144 +  (Haskell "Nothing" and "Just")
   3.145 +
   3.146 +code_instance option :: eq
   3.147 +  (Haskell -)
   3.148 +
   3.149 +code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   3.150 +  (Haskell infixl 4 "==")
   3.151 +
   3.152 +code_reserved SML
   3.153 +  option NONE SOME
   3.154 +
   3.155 +code_reserved OCaml
   3.156 +  option None Some
   3.157 +
   3.158 +code_modulename SML
   3.159 +  Datatype Nat
   3.160 +
   3.161 +code_modulename OCaml
   3.162 +  Datatype Nat
   3.163 +
   3.164 +code_modulename Haskell
   3.165 +  Datatype Nat
   3.166 +
   3.167  end
     4.1 --- a/src/HOL/Extraction.thy	Thu Aug 09 15:52:38 2007 +0200
     4.2 +++ b/src/HOL/Extraction.thy	Thu Aug 09 15:52:42 2007 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Program extraction for HOL *}
     4.5  
     4.6  theory Extraction
     4.7 -imports Datatype Option
     4.8 +imports Datatype
     4.9  uses "Tools/rewrite_hol_proof.ML"
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Finite_Set.thy	Thu Aug 09 15:52:38 2007 +0200
     5.2 +++ b/src/HOL/Finite_Set.thy	Thu Aug 09 15:52:42 2007 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* Finite sets *}
     5.5  
     5.6  theory Finite_Set
     5.7 -imports IntDef Divides Option
     5.8 +imports IntDef Divides
     5.9  begin
    5.10  
    5.11  subsection {* Definition and basic properties *}
     6.1 --- a/src/HOL/FunDef.thy	Thu Aug 09 15:52:38 2007 +0200
     6.2 +++ b/src/HOL/FunDef.thy	Thu Aug 09 15:52:42 2007 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* General recursive function definitions *}
     6.5  
     6.6  theory FunDef
     6.7 -imports Datatype Option Accessible_Part
     6.8 +imports Datatype Accessible_Part
     6.9  uses
    6.10    ("Tools/function_package/fundef_lib.ML")
    6.11    ("Tools/function_package/fundef_common.ML")
     7.1 --- a/src/HOL/IsaMakefile	Thu Aug 09 15:52:38 2007 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Thu Aug 09 15:52:42 2007 +0200
     7.3 @@ -88,7 +88,7 @@
     7.4    Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy		\
     7.5    Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy	\
     7.6    Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy	\
     7.7 -  Numeral.thy Option.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy	\
     7.8 +  Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy	\
     7.9    Predicate.thy Product_Type.thy ROOT.ML Recdef.thy			\
    7.10    Record.thy Refute.thy Relation.thy Relation_Power.thy			\
    7.11    Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy	\
    7.12 @@ -223,7 +223,7 @@
    7.13    Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
    7.14    Library/SCT_Examples.thy Library/sct.ML \
    7.15    Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \
    7.16 -  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy
    7.17 +  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy
    7.18  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    7.19  
    7.20  
    7.21 @@ -648,7 +648,7 @@
    7.22    ex/BT.thy ex/BinEx.thy ex/CTL.thy \
    7.23    ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \
    7.24    ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
    7.25 -  ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
    7.26 +  ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
    7.27    ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
    7.28    ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
    7.29    ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
     8.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Aug 09 15:52:38 2007 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Aug 09 15:52:42 2007 +0200
     8.3 @@ -456,7 +456,7 @@
     8.4          thy
     8.5          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
     8.6          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
     8.7 -        |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
     8.8 +        |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
     8.9          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    8.10          |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    8.11          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    8.12 @@ -524,7 +524,7 @@
    8.13           |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    8.14                                       (fs_proof fs_thm_nprod) 
    8.15           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    8.16 -         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    8.17 +         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    8.18          end) ak_names thy20;
    8.19  
    8.20         (********  cp_<ak>_<ai> class instances  ********)
    8.21 @@ -607,7 +607,7 @@
    8.22  	 |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
    8.23           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    8.24           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    8.25 -         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    8.26 +         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    8.27           |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    8.28           |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
    8.29          end) ak_names thy) ak_names thy25;
     9.1 --- a/src/HOL/Option.thy	Thu Aug 09 15:52:38 2007 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,123 +0,0 @@
     9.4 -(*  Title:      HOL/Datatype.thy
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     9.8 -    Author:     Florian Haftmann, TU Muenchen
     9.9 -*)
    9.10 -
    9.11 -header {* The option datatype *}
    9.12 -
    9.13 -theory Option
    9.14 -imports Datatype
    9.15 -begin
    9.16 -
    9.17 -subsection {* Type declaration *}
    9.18 -
    9.19 -datatype 'a option = None | Some 'a
    9.20 -
    9.21 -lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
    9.22 -  by (induct x) auto
    9.23 -
    9.24 -lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
    9.25 -  by (induct x) auto
    9.26 -
    9.27 -text{*Although it may appear that both of these equalities are helpful
    9.28 -only when applied to assumptions, in practice it seems better to give
    9.29 -them the uniform iff attribute. *}
    9.30 -
    9.31 -lemma option_caseE:
    9.32 -  assumes c: "(case x of None => P | Some y => Q y)"
    9.33 -  obtains
    9.34 -    (None) "x = None" and P
    9.35 -  | (Some) y where "x = Some y" and "Q y"
    9.36 -  using c by (cases x) simp_all
    9.37 -
    9.38 -
    9.39 -subsection {* Operations *}
    9.40 -
    9.41 -consts
    9.42 -  the :: "'a option => 'a"
    9.43 -primrec
    9.44 -  "the (Some x) = x"
    9.45 -
    9.46 -consts
    9.47 -  o2s :: "'a option => 'a set"
    9.48 -primrec
    9.49 -  "o2s None = {}"
    9.50 -  "o2s (Some x) = {x}"
    9.51 -
    9.52 -lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
    9.53 -  by simp
    9.54 -
    9.55 -ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
    9.56 -
    9.57 -lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
    9.58 -  by (cases xo) auto
    9.59 -
    9.60 -lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
    9.61 -  by (cases xo) auto
    9.62 -
    9.63 -
    9.64 -constdefs
    9.65 -  option_map :: "('a => 'b) => ('a option => 'b option)"
    9.66 -  [code func del]: "option_map == %f y. case y of None => None | Some x => Some (f x)"
    9.67 -
    9.68 -lemma option_map_None [simp, code]: "option_map f None = None"
    9.69 -  by (simp add: option_map_def)
    9.70 -
    9.71 -lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
    9.72 -  by (simp add: option_map_def)
    9.73 -
    9.74 -lemma option_map_is_None [iff]:
    9.75 -    "(option_map f opt = None) = (opt = None)"
    9.76 -  by (simp add: option_map_def split add: option.split)
    9.77 -
    9.78 -lemma option_map_eq_Some [iff]:
    9.79 -    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
    9.80 -  by (simp add: option_map_def split add: option.split)
    9.81 -
    9.82 -lemma option_map_comp:
    9.83 -    "option_map f (option_map g opt) = option_map (f o g) opt"
    9.84 -  by (simp add: option_map_def split add: option.split)
    9.85 -
    9.86 -lemma option_map_o_sum_case [simp]:
    9.87 -    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
    9.88 -  by (rule ext) (simp split: sum.split)
    9.89 -
    9.90 -
    9.91 -subsection {* Code generator setup *}
    9.92 -
    9.93 -definition
    9.94 -  is_none :: "'a option \<Rightarrow> bool" where
    9.95 -  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    9.96 -
    9.97 -lemma is_none_code [code]:
    9.98 -  shows "is_none None \<longleftrightarrow> True"
    9.99 -    and "is_none (Some x) \<longleftrightarrow> False"
   9.100 -  unfolding is_none_none [symmetric] by simp_all
   9.101 -
   9.102 -hide (open) const is_none
   9.103 -
   9.104 -code_type option
   9.105 -  (SML "_ option")
   9.106 -  (OCaml "_ option")
   9.107 -  (Haskell "Maybe _")
   9.108 -
   9.109 -code_const None and Some
   9.110 -  (SML "NONE" and "SOME")
   9.111 -  (OCaml "None" and "Some _")
   9.112 -  (Haskell "Nothing" and "Just")
   9.113 -
   9.114 -code_instance option :: eq
   9.115 -  (Haskell -)
   9.116 -
   9.117 -code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   9.118 -  (Haskell infixl 4 "==")
   9.119 -
   9.120 -code_reserved SML
   9.121 -  option NONE SOME
   9.122 -
   9.123 -code_reserved OCaml
   9.124 -  option None Some
   9.125 -
   9.126 -end