Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
--- a/src/HOL/Imperative_HOL/Array.thy Fri Feb 06 08:22:32 2009 +0000
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Feb 06 08:23:15 2009 +0000
@@ -124,47 +124,47 @@
subsubsection {* Logical intermediate layer *}
definition new' where
- [code del]: "new' = Array.new o nat_of_index"
+ [code del]: "new' = Array.new o Code_Index.nat_of"
hide (open) const new'
lemma [code]:
- "Array.new = Array.new' o index_of_nat"
+ "Array.new = Array.new' o Code_Index.of_nat"
by (simp add: new'_def o_def)
definition of_list' where
- [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
+ [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
hide (open) const of_list'
lemma [code]:
- "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
+ "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
by (simp add: of_list'_def)
definition make' where
- [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
+ [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
hide (open) const make'
lemma [code]:
- "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
+ "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
by (simp add: make'_def o_def)
definition length' where
- [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
+ [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
hide (open) const length'
lemma [code]:
- "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
+ "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
by (simp add: length'_def monad_simp',
simp add: liftM_def comp_def monad_simp,
simp add: monad_simp')
definition nth' where
- [code del]: "nth' a = Array.nth a o nat_of_index"
+ [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
hide (open) const nth'
lemma [code]:
- "Array.nth a n = Array.nth' a (index_of_nat n)"
+ "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
by (simp add: nth'_def)
definition upd' where
- [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
+ [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
hide (open) const upd'
lemma [code]:
- "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
+ "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- a/src/HOL/Library/Code_Index.thy Fri Feb 06 08:22:32 2009 +0000
+++ b/src/HOL/Library/Code_Index.thy Fri Feb 06 08:23:15 2009 +0000
@@ -1,6 +1,4 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
header {* Type of indices *}
@@ -15,78 +13,77 @@
subsection {* Datatype of indices *}
-typedef index = "UNIV \<Colon> nat set"
- morphisms nat_of_index index_of_nat by rule
+typedef (open) index = "UNIV \<Colon> nat set"
+ morphisms nat_of of_nat by rule
-lemma index_of_nat_nat_of_index [simp]:
- "index_of_nat (nat_of_index k) = k"
- by (rule nat_of_index_inverse)
+lemma of_nat_nat_of [simp]:
+ "of_nat (nat_of k) = k"
+ by (rule nat_of_inverse)
-lemma nat_of_index_index_of_nat [simp]:
- "nat_of_index (index_of_nat n) = n"
- by (rule index_of_nat_inverse)
- (unfold index_def, rule UNIV_I)
+lemma nat_of_of_nat [simp]:
+ "nat_of (of_nat n) = n"
+ by (rule of_nat_inverse) (rule UNIV_I)
lemma [measure_function]:
- "is_measure nat_of_index" by (rule is_measure_trivial)
+ "is_measure nat_of" by (rule is_measure_trivial)
lemma index:
- "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
+ "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
proof
fix n :: nat
assume "\<And>n\<Colon>index. PROP P n"
- then show "PROP P (index_of_nat n)" .
+ then show "PROP P (of_nat n)" .
next
fix n :: index
- assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"
- then have "PROP P (index_of_nat (nat_of_index n))" .
+ assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
+ then have "PROP P (of_nat (nat_of n))" .
then show "PROP P n" by simp
qed
lemma index_case:
- assumes "\<And>n. k = index_of_nat n \<Longrightarrow> P"
+ assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
shows P
- by (rule assms [of "nat_of_index k"]) simp
+ by (rule assms [of "nat_of k"]) simp
lemma index_induct_raw:
- assumes "\<And>n. P (index_of_nat n)"
+ assumes "\<And>n. P (of_nat n)"
shows "P k"
proof -
- from assms have "P (index_of_nat (nat_of_index k))" .
+ from assms have "P (of_nat (nat_of k))" .
then show ?thesis by simp
qed
-lemma nat_of_index_inject [simp]:
- "nat_of_index k = nat_of_index l \<longleftrightarrow> k = l"
- by (rule nat_of_index_inject)
+lemma nat_of_inject [simp]:
+ "nat_of k = nat_of l \<longleftrightarrow> k = l"
+ by (rule nat_of_inject)
-lemma index_of_nat_inject [simp]:
- "index_of_nat n = index_of_nat m \<longleftrightarrow> n = m"
- by (auto intro!: index_of_nat_inject simp add: index_def)
+lemma of_nat_inject [simp]:
+ "of_nat n = of_nat m \<longleftrightarrow> n = m"
+ by (rule of_nat_inject) (rule UNIV_I)+
instantiation index :: zero
begin
definition [simp, code del]:
- "0 = index_of_nat 0"
+ "0 = of_nat 0"
instance ..
end
definition [simp]:
- "Suc_index k = index_of_nat (Suc (nat_of_index k))"
+ "Suc_index k = of_nat (Suc (nat_of k))"
rep_datatype "0 \<Colon> index" Suc_index
proof -
fix P :: "index \<Rightarrow> bool"
fix k :: index
- assume "P 0" then have init: "P (index_of_nat 0)" by simp
+ assume "P 0" then have init: "P (of_nat 0)" by simp
assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
- then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" .
- then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp
- from init step have "P (index_of_nat (nat_of_index k))"
- by (induct "nat_of_index k") simp_all
+ then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
+ then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
+ from init step have "P (of_nat (nat_of k))"
+ by (induct "nat_of k") simp_all
then show "P k" by simp
qed simp_all
@@ -96,25 +93,25 @@
declare index.induct [case_names nat, induct type: index]
lemma [code]:
- "index_size = nat_of_index"
+ "index_size = nat_of"
proof (rule ext)
fix k
- have "index_size k = nat_size (nat_of_index k)"
+ have "index_size k = nat_size (nat_of k)"
by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
- also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all
- finally show "index_size k = nat_of_index k" .
+ also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+ finally show "index_size k = nat_of k" .
qed
lemma [code]:
- "size = nat_of_index"
+ "size = nat_of"
proof (rule ext)
fix k
- show "size k = nat_of_index k"
+ show "size k = nat_of k"
by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
qed
lemma [code]:
- "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
+ "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
by (cases k, cases l) (simp add: eq)
lemma [code nbe]:
@@ -128,14 +125,14 @@
begin
definition
- "number_of = index_of_nat o nat"
+ "number_of = of_nat o nat"
instance ..
end
-lemma nat_of_index_number [simp]:
- "nat_of_index (number_of k) = number_of k"
+lemma nat_of_number [simp]:
+ "nat_of (number_of k) = number_of k"
by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
code_datatype "number_of \<Colon> int \<Rightarrow> index"
@@ -147,30 +144,31 @@
begin
definition [simp, code del]:
- "(1\<Colon>index) = index_of_nat 1"
+ "(1\<Colon>index) = of_nat 1"
definition [simp, code del]:
- "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
+ "n + m = of_nat (nat_of n + nat_of m)"
definition [simp, code del]:
- "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
+ "n - m = of_nat (nat_of n - nat_of m)"
definition [simp, code del]:
- "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
+ "n * m = of_nat (nat_of n * nat_of m)"
definition [simp, code del]:
- "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
+ "n div m = of_nat (nat_of n div nat_of m)"
definition [simp, code del]:
- "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
+ "n mod m = of_nat (nat_of n mod nat_of m)"
definition [simp, code del]:
- "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
+ "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
definition [simp, code del]:
- "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
+ "n < m \<longleftrightarrow> nat_of n < nat_of m"
-instance by default (auto simp add: left_distrib index)
+instance proof
+qed (auto simp add: left_distrib)
end
@@ -187,14 +185,14 @@
using one_index_code ..
lemma plus_index_code [code nbe]:
- "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
+ "of_nat n + of_nat m = of_nat (n + m)"
by simp
definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
[simp, code del]: "subtract_index = op -"
lemma subtract_index_code [code nbe]:
- "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)"
+ "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
by simp
lemma minus_index_code [code]:
@@ -202,42 +200,42 @@
by simp
lemma times_index_code [code nbe]:
- "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
+ "of_nat n * of_nat m = of_nat (n * m)"
by simp
lemma less_eq_index_code [code nbe]:
- "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
+ "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
by simp
lemma less_index_code [code nbe]:
- "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
+ "of_nat n < of_nat m \<longleftrightarrow> n < m"
by simp
lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
-lemma index_of_nat_code [code]:
- "index_of_nat = of_nat"
+lemma of_nat_code [code]:
+ "of_nat = Nat.of_nat"
proof
fix n :: nat
- have "of_nat n = index_of_nat n"
+ have "Nat.of_nat n = of_nat n"
by (induct n) simp_all
- then show "index_of_nat n = of_nat n"
+ then show "of_nat n = Nat.of_nat n"
by (rule sym)
qed
-lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
+lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
by (cases i) auto
-definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
- "nat_of_index_aux i n = nat_of_index i + n"
+definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
+ "nat_of_aux i n = nat_of i + n"
-lemma nat_of_index_aux_code [code]:
- "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))"
- by (auto simp add: nat_of_index_aux_def index_not_eq_zero)
+lemma nat_of_aux_code [code]:
+ "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
+ by (auto simp add: nat_of_aux_def index_not_eq_zero)
-lemma nat_of_index_code [code]:
- "nat_of_index i = nat_of_index_aux i 0"
- by (simp add: nat_of_index_aux_def)
+lemma nat_of_code [code]:
+ "nat_of i = nat_of_aux i 0"
+ by (simp add: nat_of_aux_def)
definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
[code del]: "div_mod_index n m = (n div m, n mod m)"
@@ -254,6 +252,7 @@
"n mod m = snd (div_mod_index n m)"
unfolding div_mod_index_def by simp
+hide (open) const of_nat nat_of
subsection {* ML interface *}
--- a/src/HOL/Library/Efficient_Nat.thy Fri Feb 06 08:22:32 2009 +0000
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Feb 06 08:23:15 2009 +0000
@@ -376,12 +376,12 @@
text {* Conversion from and to indices. *}
-code_const index_of_nat
+code_const Code_Index.of_nat
(SML "IntInf.toInt")
(OCaml "Big'_int.int'_of'_big'_int")
(Haskell "fromEnum")
-code_const nat_of_index
+code_const Code_Index.nat_of
(SML "IntInf.fromInt")
(OCaml "Big'_int.big'_int'_of'_int")
(Haskell "toEnum")
--- a/src/HOL/Library/Mapping.thy Fri Feb 06 08:22:32 2009 +0000
+++ b/src/HOL/Library/Mapping.thy Fri Feb 06 08:23:15 2009 +0000
@@ -33,6 +33,9 @@
definition size :: "('a, 'b) map \<Rightarrow> nat" where
"size m = (if finite (keys m) then card (keys m) else 0)"
+definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
+ "replace k v m = (if lookup m k = None then m else update k v m)"
+
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
"tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
@@ -65,6 +68,11 @@
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
by (cases m, simp add: expand_fun_eq)+
+lemma replace_update:
+ "lookup m k = None \<Longrightarrow> replace k v m = m"
+ "lookup m k \<noteq> None \<Longrightarrow> replace k v m = update k v m"
+ by (auto simp add: replace_def)
+
lemma delete_empty [simp]:
"delete k empty = empty"
by (simp add: empty_def)
--- a/src/HOL/Library/Random.thy Fri Feb 06 08:22:32 2009 +0000
+++ b/src/HOL/Library/Random.thy Fri Feb 06 08:23:15 2009 +0000
@@ -1,5 +1,4 @@
-(* Author: Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
header {* A HOL random engine *}
@@ -77,7 +76,7 @@
in range_aux (k - 1) (v + l * 2147483561) s')"
by pat_completeness auto
termination
- by (relation "measure (nat_of_index o fst)")
+ by (relation "measure (Code_Index.nat_of o fst)")
(auto simp add: index)
definition
@@ -103,19 +102,19 @@
select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
where
"select xs = (do
- k \<leftarrow> range (index_of_nat (length xs));
- return (nth xs (nat_of_index k))
+ k \<leftarrow> range (Code_Index.of_nat (length xs));
+ return (nth xs (Code_Index.nat_of k))
done)"
lemma select:
assumes "xs \<noteq> []"
shows "fst (select xs s) \<in> set xs"
proof -
- from assms have "index_of_nat (length xs) > 0" by simp
+ from assms have "Code_Index.of_nat (length xs) > 0" by simp
with range have
- "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
+ "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
then have
- "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
+ "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
then show ?thesis
by (auto simp add: monad_collapse select_def)
qed
--- a/src/Pure/Isar/class.ML Fri Feb 06 08:22:32 2009 +0000
+++ b/src/Pure/Isar/class.ML Fri Feb 06 08:23:15 2009 +0000
@@ -122,19 +122,19 @@
val inferred_sort = extract
(fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
val fixate_sort = if null tfrees then inferred_sort
- else let val a_sort = (snd o the_single) tfrees
- in if Sorts.sort_le algebra (a_sort, inferred_sort)
- then Sorts.inter_sort algebra (a_sort, inferred_sort)
- else error ("Type inference imposes additional sort constraint "
- ^ Syntax.string_of_sort_global thy inferred_sort
- ^ " of type parameter " ^ Name.aT ^ " of sort "
- ^ Syntax.string_of_sort_global thy a_sort)
- end
+ else case tfrees
+ of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
+ then Sorts.inter_sort algebra (a_sort, inferred_sort)
+ else error ("Type inference imposes additional sort constraint "
+ ^ Syntax.string_of_sort_global thy inferred_sort
+ ^ " of type parameter " ^ Name.aT ^ " of sort "
+ ^ Syntax.string_of_sort_global thy a_sort ^ ".")
+ | _ => error "Multiple type variables in class specification.";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
- (* preproceesing elements, retrieving base sort from type-checked elements *)
+ (* preprocessing elements, retrieving base sort from type-checked elements *)
val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
#> redeclare_operations thy sups
#> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
@@ -188,9 +188,6 @@
(* process elements as class specification *)
val class_ctxt = begin sups base_sort (ProofContext.init thy)
val ((_, _, syntax_elems), _) = class_ctxt
- (*#> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
- (K (TFree (Name.aT, base_sort))) supparams) FIXME really necessary?*)
- (*FIXME should constraints be issued in begin?*)
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs = if null vs
then error ("No type variable in part of specification element "
@@ -210,7 +207,7 @@
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
val constrain = Element.Constrains ((map o apsnd o map_atyps)
(K (TFree (Name.aT, base_sort))) supparams);
- (*FIXME 2009 perhaps better: control type variable by explicit
+ (*FIXME perhaps better: control type variable by explicit
parameter instantiation of import expression*)
in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
@@ -223,7 +220,7 @@
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
- (*FIXME 2009 simplify*)
+ (*FIXME simplify*)
val supconsts = supparams
|> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
@@ -253,7 +250,7 @@
fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
let
- (*FIXME 2009 simplify*)
+ (*FIXME simplify*)
fun globalize param_map = map_aterms
(fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
| t => t);