# HG changeset patch # User wenzelm # Date 1014318489 -3600 # Node ID bca45be2d25b75f6a0aa48cb87bebb50876cf5b4 # Parent 0fd3caa5d8b2b4aa643f686435d64cc655d1b976 theory Option has been assimilated by Datatype; diff -r 0fd3caa5d8b2 -r bca45be2d25b src/HOL/Datatype.ML --- a/src/HOL/Datatype.ML Thu Feb 21 20:06:39 2002 +0100 +++ b/src/HOL/Datatype.ML Thu Feb 21 20:08:09 2002 +0100 @@ -62,34 +62,31 @@ val size = thms "prod.size"; end; - -(** sum_case -- the selection operator for sums **) - -(*compatibility*) -val [sum_case_Inl, sum_case_Inr] = sum.cases; -bind_thm ("sum_case_Inl", sum_case_Inl); -bind_thm ("sum_case_Inr", sum_case_Inr); - -Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; -by (EVERY1 [res_inst_tac [("s","s")] sumE, - etac ssubst, rtac sum_case_Inl, - etac ssubst, rtac sum_case_Inr]); -qed "surjective_sum"; +structure option = +struct + val distinct = thms "option.distinct"; + val inject = thms "option.inject"; + val exhaust = thm "option.exhaust"; + val cases = thms "option.cases"; + val split = thm "option.split"; + val split_asm = thm "option.split_asm"; + val induct = thm "option.induct"; + val recs = thms "option.recs"; + val simps = thms "option.simps"; + val size = thms "option.size"; +end; -(*Prevents simplification of f and g: much faster*) -Goal "s=t ==> sum_case f g s = sum_case f g t"; -by (etac arg_cong 1); -qed "sum_case_weak_cong"; - -val [p1,p2] = Goal - "[| sum_case f1 f2 = sum_case g1 g2; \ -\ [| f1 = g1; f2 = g2 |] ==> P |] \ -\ ==> P"; -by (rtac p2 1); -by (rtac ext 1); -by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1); -by (Asm_full_simp_tac 1); -by (rtac ext 1); -by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1); -by (Asm_full_simp_tac 1); -qed "sum_case_inject"; +val elem_o2s = thm "elem_o2s"; +val not_None_eq = thm "not_None_eq"; +val not_Some_eq = thm "not_Some_eq"; +val o2s_empty_eq = thm "o2s_empty_eq"; +val option_caseE = thm "option_caseE"; +val option_map_None = thm "option_map_None"; +val option_map_Some = thm "option_map_Some"; +val option_map_def = thm "option_map_def"; +val option_map_eq_Some = thm "option_map_eq_Some"; +val option_map_o_sum_case = thm "option_map_o_sum_case"; +val ospec = thm "ospec"; +val sum_case_inject = thm "sum_case_inject"; +val sum_case_weak_cong = thm "sum_case_weak_cong"; +val surjective_sum = thm "surjective_sum"; diff -r 0fd3caa5d8b2 -r bca45be2d25b src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Thu Feb 21 20:06:39 2002 +0100 +++ b/src/HOL/Datatype.thy Thu Feb 21 20:08:09 2002 +0100 @@ -4,10 +4,12 @@ License: GPL (GNU GENERAL PUBLIC LICENSE) *) -header {* Final stage of datatype setup *} +header {* Datatypes *} theory Datatype = Datatype_Universe: +subsection {* Finishing the datatype package setup *} + text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} hide const Node Atom Leaf Numb Lim Funs Split Case hide type node item @@ -22,11 +24,6 @@ declare case_split [cases type: bool] -- "prefer plain propositional version" -rep_datatype sum - distinct Inl_not_Inr Inr_not_Inl - inject Inl_eq Inr_eq - induction sum_induct - rep_datatype unit induction unit_induct @@ -34,7 +31,47 @@ inject Pair_eq induction prod_induct -text {* Further cases/induct rules for 3--7 tuples. *} +rep_datatype sum + distinct Inl_not_Inr Inr_not_Inl + inject Inl_eq Inr_eq + induction sum_induct + +ML {* + val [sum_case_Inl, sum_case_Inr] = thms "sum.cases"; + bind_thm ("sum_case_Inl", sum_case_Inl); + bind_thm ("sum_case_Inr", sum_case_Inr); +*} -- {* compatibility *} + +lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" + apply (rule_tac s = s in sumE) + apply (erule ssubst) + apply (rule sum_case_Inl) + apply (erule ssubst) + apply (rule sum_case_Inr) + done + +lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" + -- {* Prevents simplification of @{text f} and @{text g}: much faster. *} + by (erule arg_cong) + +lemma sum_case_inject: + "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" +proof - + assume a: "sum_case f1 f2 = sum_case g1 g2" + assume r: "f1 = g1 ==> f2 = g2 ==> P" + show P + apply (rule r) + apply (rule ext) + apply (cut_tac x = "Inl x" in a [THEN fun_cong]) + apply simp + apply (rule ext) + apply (cut_tac x = "Inr x" in a [THEN fun_cong]) + apply simp + done +qed + + +subsection {* Further cases/induct rules for tuples *} lemma prod_cases3 [case_names fields, cases type]: "(!!a b c. y = (a, b, c) ==> P) ==> P" @@ -91,4 +128,67 @@ "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" by (cases x) blast + +subsection {* The option type *} + +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 + +lemma option_caseE: + "(case x of None => P | Some y => Q y) ==> + (x = None ==> P ==> R) ==> + (!!y. x = Some y ==> Q y ==> R) ==> R" + 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 {* claset_ref() := claset() 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)" + +lemma option_map_None [simp]: "option_map f None = None" + by (simp add: option_map_def) + +lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" + by (simp add: option_map_def) + +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_o_sum_case [simp]: + "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" + apply (rule ext) + apply (simp split add: sum.split) + done + end diff -r 0fd3caa5d8b2 -r bca45be2d25b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Feb 21 20:06:39 2002 +0100 +++ b/src/HOL/IsaMakefile Thu Feb 21 20:08:09 2002 +0100 @@ -89,11 +89,10 @@ Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \ Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \ Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \ - Option.ML Option.thy Power.ML Power.thy PreList.thy \ - Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \ - Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \ - Set.ML Set.thy SetInterval.ML SetInterval.thy Sum_Type.ML Sum_Type.thy \ - Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ + Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \ + Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \ + Relation_Power.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \ + Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ Tools/datatype_rep_proofs.ML \ Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \ diff -r 0fd3caa5d8b2 -r bca45be2d25b src/HOL/Option.ML --- a/src/HOL/Option.ML Thu Feb 21 20:06:39 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,93 +0,0 @@ -(* Title: Option.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1996 TU Muenchen - -Derived rules -*) - -Goal "(x ~= None) = (? y. x = Some y)"; -by (induct_tac "x" 1); -by Auto_tac; -qed "not_None_eq"; -AddIffs[not_None_eq]; - -Goal "(!y. x ~= Some y) = (x = None)"; -by (induct_tac "x" 1); -by Auto_tac; -qed "not_Some_eq"; -AddIffs[not_Some_eq]; - - -section "case analysis in premises"; - -val prems = Goal - "[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P"; -by (case_tac "opt = None" 1); -by (eresolve_tac prems 1); -by (dtac (not_None_eq RS iffD1) 1); -by (etac exE 1); -by (eresolve_tac prems 1); -qed "optionE"; - -val prems = Goal - "[| case x of None => P | Some y => Q y; \ -\ [| x = None; P |] ==> R; \ -\ !!y. [|x = Some y; Q y|] ==> R|] ==> R"; -by (cut_facts_tac prems 1); -by (res_inst_tac [("opt","x")] optionE 1); -by (forward_tac prems 1); -by (forward_tac prems 3); -by Auto_tac; -qed "option_caseE"; - - -section "option_map"; - -Goalw [option_map_def] "option_map f None = None"; -by (Simp_tac 1); -qed "option_map_None"; - -Goalw [option_map_def] "option_map f (Some x) = Some (f x)"; -by (Simp_tac 1); -qed "option_map_Some"; - -Addsimps [option_map_None, option_map_Some]; - -Goalw [option_map_def] - "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)"; -by (asm_full_simp_tac (simpset() addsplits [option.split]) 1); -qed "option_map_eq_Some"; -AddIffs[option_map_eq_Some]; - -Goal -"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"; -by (rtac ext 1); -by (simp_tac (simpset() addsplits [sum.split]) 1); -qed "option_map_o_sum_case"; -Addsimps [option_map_o_sum_case]; - - -section "o2s"; - -Goal "[| !x:o2s A. P x; A = Some x |] ==> P x"; -by Auto_tac; -qed "ospec"; -AddDs[ospec]; - -claset_ref() := claset() addSD2 ("ospec", ospec); - - -Goal "(x : o2s xo) = (xo = Some x)"; -by (case_tac "xo" 1); -by Auto_tac; -qed "elem_o2s"; -AddIffs [elem_o2s]; - -Goal "(o2s xo = {}) = (xo = None)"; -by (case_tac "xo" 1); -by Auto_tac; -qed "o2s_empty_eq"; - -Addsimps [o2s_empty_eq]; - diff -r 0fd3caa5d8b2 -r bca45be2d25b src/HOL/Option.thy --- a/src/HOL/Option.thy Thu Feb 21 20:06:39 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: Option.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1994 TU Muenchen - -Datatype 'a option -*) - -Option = Datatype + - -datatype 'a option = None | Some 'a - -consts - the :: "'a option => 'a" - o2s :: "'a option => 'a set" - -primrec - "the (Some x) = x" - -primrec - "o2s None = {}" - "o2s (Some x) = {x}" - -constdefs - option_map :: "('a => 'b) => ('a option => 'b option)" - "option_map == %f y. case y of None => None | Some x => Some (f x)" - -end