--- 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";
--- 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
--- 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 \
--- 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];
-
--- 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