# HG changeset patch # User haftmann # Date 1186667562 -7200 # Node ID 96013f81faef75f6fc338cae32f3b4acca9cb0b2 # Parent 926dde4d96de206481ac99854c7bb84e8bf0f4b9 re-eliminated Option.thy diff -r 926dde4d96de -r 96013f81faef src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/Bali/Basis.thy Thu Aug 09 15:52:42 2007 +0200 @@ -236,7 +236,7 @@ (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) translations - "option"<= (type) "Option.option" + "option"<= (type) "Datatype.option" "list" <= (type) "List.list" "sum3" <= (type) "Basis.sum3" diff -r 926dde4d96de -r 96013f81faef src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/Bali/Table.thy Thu Aug 09 15:52:42 2007 +0200 @@ -44,7 +44,7 @@ translations "table_of" == "map_of" - (type)"'a \ 'b" <= (type)"'a \ 'b Option.option" + (type)"'a \ 'b" <= (type)"'a \ 'b Datatype.option" (type)"('a, 'b) table" <= (type)"'a \ 'b" (* ### To map *) diff -r 926dde4d96de -r 96013f81faef src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/Datatype.thy Thu Aug 09 15:52:42 2007 +0200 @@ -539,9 +539,23 @@ subsection {* Representing primitive types *} +rep_datatype bool + distinct True_not_False False_not_True + induction bool_induct + declare case_split [cases type: bool] -- "prefer plain propositional version" +lemma size_bool [code func]: + "size (b\bool) = 0" by (cases b) auto + +rep_datatype unit + induction unit_induct + +rep_datatype prod + inject Pair_eq + induction prod_induct + lemmas prod_caseI = prod.cases [THEN iffD2, standard] lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" @@ -568,6 +582,14 @@ lemmas [code inline] = prod_case_split [symmetric] +rep_datatype sum + distinct Inl_not_Inr Inr_not_Inl + inject Inl_eq Inr_eq + induction sum_induct + +lemma size_sum [code func]: + "size (x \ 'a + 'b) = 0" by (cases x) auto + lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)" by (rule ext) (simp split: sum.split) @@ -655,4 +677,125 @@ "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" by (cases x) blast + +subsection {* The option datatype *} + +datatype 'a option = None | Some 'a + +lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" + by (induct x) auto + +lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" + by (induct x) auto + +text{*Although it may appear that both of these equalities are helpful +only when applied to assumptions, in practice it seems better to give +them the uniform iff attribute. *} + +lemma option_caseE: + assumes c: "(case x of None => P | Some y => Q y)" + obtains + (None) "x = None" and P + | (Some) y where "x = Some y" and "Q y" + using c by (cases x) simp_all + + +subsubsection {* Operations *} + +consts + the :: "'a option => 'a" +primrec + "the (Some x) = x" + +consts + o2s :: "'a option => 'a set" +primrec + "o2s None = {}" + "o2s (Some x) = {x}" + +lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" + by simp + +ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} + +lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" + by (cases xo) auto + +lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" + by (cases xo) auto + + +constdefs + option_map :: "('a => 'b) => ('a option => 'b option)" + "option_map == %f y. case y of None => None | Some x => Some (f x)" + +lemmas [code func del] = option_map_def + +lemma option_map_None [simp, code]: "option_map f None = None" + by (simp add: option_map_def) + +lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)" + by (simp add: option_map_def) + +lemma option_map_is_None [iff]: + "(option_map f opt = None) = (opt = None)" + by (simp add: option_map_def split add: option.split) + +lemma option_map_eq_Some [iff]: + "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" + by (simp add: option_map_def split add: option.split) + +lemma option_map_comp: + "option_map f (option_map g opt) = option_map (f o g) opt" + by (simp add: option_map_def split add: option.split) + +lemma option_map_o_sum_case [simp]: + "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" + by (rule ext) (simp split: sum.split) + + +subsubsection {* Code generator setup *} + +definition + is_none :: "'a option \ bool" where + is_none_none [code post, symmetric, code inline]: "is_none x \ x = None" + +lemma is_none_code [code]: + shows "is_none None \ True" + and "is_none (Some x) \ False" + unfolding is_none_none [symmetric] by simp_all + +hide (open) const is_none + +code_type option + (SML "_ option") + (OCaml "_ option") + (Haskell "Maybe _") + +code_const None and Some + (SML "NONE" and "SOME") + (OCaml "None" and "Some _") + (Haskell "Nothing" and "Just") + +code_instance option :: eq + (Haskell -) + +code_const "op = \ 'a\eq option \ 'a option \ bool" + (Haskell infixl 4 "==") + +code_reserved SML + option NONE SOME + +code_reserved OCaml + option None Some + +code_modulename SML + Datatype Nat + +code_modulename OCaml + Datatype Nat + +code_modulename Haskell + Datatype Nat + end diff -r 926dde4d96de -r 96013f81faef src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/Extraction.thy Thu Aug 09 15:52:42 2007 +0200 @@ -6,7 +6,7 @@ header {* Program extraction for HOL *} theory Extraction -imports Datatype Option +imports Datatype uses "Tools/rewrite_hol_proof.ML" begin diff -r 926dde4d96de -r 96013f81faef src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/Finite_Set.thy Thu Aug 09 15:52:42 2007 +0200 @@ -7,7 +7,7 @@ header {* Finite sets *} theory Finite_Set -imports IntDef Divides Option +imports IntDef Divides begin subsection {* Definition and basic properties *} diff -r 926dde4d96de -r 96013f81faef src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/FunDef.thy Thu Aug 09 15:52:42 2007 +0200 @@ -6,7 +6,7 @@ header {* General recursive function definitions *} theory FunDef -imports Datatype Option Accessible_Part +imports Datatype Accessible_Part uses ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/fundef_common.ML") diff -r 926dde4d96de -r 96013f81faef src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/IsaMakefile Thu Aug 09 15:52:42 2007 +0200 @@ -88,7 +88,7 @@ Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy \ Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \ Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \ - Numeral.thy Option.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \ + Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \ Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \ Record.thy Refute.thy Relation.thy Relation_Power.thy \ Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \ @@ -223,7 +223,7 @@ Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \ Library/SCT_Examples.thy Library/sct.ML \ Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \ - Library/Pretty_Char.thy Library/Pretty_Char_chr.thy + Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library @@ -648,7 +648,7 @@ ex/BT.thy ex/BinEx.thy ex/CTL.thy \ ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \ ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \ - ex/Codegenerator.thy ex/Codegenerator_Rat.thy \ + ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \ ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \ ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \ ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \ diff -r 926dde4d96de -r 96013f81faef src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Thu Aug 09 15:52:38 2007 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu Aug 09 15:52:42 2007 +0200 @@ -456,7 +456,7 @@ thy |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) - |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) + |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) @@ -524,7 +524,7 @@ |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) - |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) + |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) end) ak_names thy20; (******** cp__ class instances ********) @@ -607,7 +607,7 @@ |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) - |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) + |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn) |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set) end) ak_names thy) ak_names thy25; diff -r 926dde4d96de -r 96013f81faef src/HOL/Option.thy --- a/src/HOL/Option.thy Thu Aug 09 15:52:38 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,123 +0,0 @@ -(* Title: HOL/Datatype.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Stefan Berghofer and Markus Wenzel, TU Muenchen - Author: Florian Haftmann, TU Muenchen -*) - -header {* The option datatype *} - -theory Option -imports Datatype -begin - -subsection {* Type declaration *} - -datatype 'a option = None | Some 'a - -lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" - by (induct x) auto - -lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" - by (induct x) auto - -text{*Although it may appear that both of these equalities are helpful -only when applied to assumptions, in practice it seems better to give -them the uniform iff attribute. *} - -lemma option_caseE: - assumes c: "(case x of None => P | Some y => Q y)" - obtains - (None) "x = None" and P - | (Some) y where "x = Some y" and "Q y" - using c by (cases x) simp_all - - -subsection {* Operations *} - -consts - the :: "'a option => 'a" -primrec - "the (Some x) = x" - -consts - o2s :: "'a option => 'a set" -primrec - "o2s None = {}" - "o2s (Some x) = {x}" - -lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" - by simp - -ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} - -lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" - by (cases xo) auto - -lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" - by (cases xo) auto - - -constdefs - option_map :: "('a => 'b) => ('a option => 'b option)" - [code func del]: "option_map == %f y. case y of None => None | Some x => Some (f x)" - -lemma option_map_None [simp, code]: "option_map f None = None" - by (simp add: option_map_def) - -lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)" - by (simp add: option_map_def) - -lemma option_map_is_None [iff]: - "(option_map f opt = None) = (opt = None)" - by (simp add: option_map_def split add: option.split) - -lemma option_map_eq_Some [iff]: - "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" - by (simp add: option_map_def split add: option.split) - -lemma option_map_comp: - "option_map f (option_map g opt) = option_map (f o g) opt" - by (simp add: option_map_def split add: option.split) - -lemma option_map_o_sum_case [simp]: - "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" - by (rule ext) (simp split: sum.split) - - -subsection {* Code generator setup *} - -definition - is_none :: "'a option \ bool" where - is_none_none [code post, symmetric, code inline]: "is_none x \ x = None" - -lemma is_none_code [code]: - shows "is_none None \ True" - and "is_none (Some x) \ False" - unfolding is_none_none [symmetric] by simp_all - -hide (open) const is_none - -code_type option - (SML "_ option") - (OCaml "_ option") - (Haskell "Maybe _") - -code_const None and Some - (SML "NONE" and "SOME") - (OCaml "None" and "Some _") - (Haskell "Nothing" and "Just") - -code_instance option :: eq - (Haskell -) - -code_const "op = \ 'a\eq option \ 'a option \ bool" - (Haskell infixl 4 "==") - -code_reserved SML - option NONE SOME - -code_reserved OCaml - option None Some - -end