--- a/doc-src/Codegen/Thy/Adaptation.thy Tue May 19 13:52:12 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed May 20 15:35:22 2009 +0200
@@ -121,14 +121,14 @@
which in general will result in higher efficiency; pattern
matching with @{term "0\<Colon>nat"} / @{const "Suc"}
is eliminated; includes @{theory "Code_Integer"}
- and @{theory "Code_Index"}.
- \item[@{theory "Code_Index"}] provides an additional datatype
+ and @{theory "Code_Numeral"}.
+ \item[@{theory "Code_Numeral"}] provides an additional datatype
@{typ index} which is mapped to target-language built-in integers.
Useful for code setups which involve e.g. indexing of
target-language arrays.
\item[@{theory "String"}] provides an additional datatype
- @{typ message_string} which is isomorphic to strings;
- @{typ message_string}s are mapped to target-language strings.
+ @{typ String.literal} which is isomorphic to strings;
+ @{typ String.literal}s are mapped to target-language strings.
Useful for code setups which involve e.g. printing (error) messages.
\end{description}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Tue May 19 13:52:12 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed May 20 15:35:22 2009 +0200
@@ -161,14 +161,14 @@
which in general will result in higher efficiency; pattern
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
- and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
- \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
+ and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}.
+ \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}] provides an additional datatype
\isa{index} which is mapped to target-language built-in integers.
Useful for code setups which involve e.g. indexing of
target-language arrays.
\item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype
- \isa{message{\isacharunderscore}string} which is isomorphic to strings;
- \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
+ \isa{String{\isachardot}literal} which is isomorphic to strings;
+ \isa{String{\isachardot}literal}s are mapped to target-language strings.
Useful for code setups which involve e.g. printing (error) messages.
\end{description}
--- a/doc-src/Codegen/Thy/document/ML.tex Tue May 19 13:52:12 2009 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex Wed May 20 15:35:22 2009 +0200
@@ -124,8 +124,8 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\
- \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+ \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
+ \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
\end{mldecls}
\begin{description}
--- a/src/HOL/Code_Eval.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Code_Eval.thy Wed May 20 15:35:22 2009 +0200
@@ -5,7 +5,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Eval
-imports Plain Typerep
+imports Plain Typerep Code_Numeral
begin
subsection {* Term representation *}
@@ -14,7 +14,7 @@
datatype "term" = dummy_term
-definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
+definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
@@ -63,10 +63,7 @@
let
val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
- in
- thy
- |> need_inst ? add_term_of tyco raw_vs
- end;
+ in if need_inst then add_term_of tyco raw_vs thy else thy end;
in
Code.type_interpretation ensure_term_of
end
@@ -102,10 +99,7 @@
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
let
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
- in
- thy
- |> has_inst ? add_term_of_code tyco raw_vs cs
- end;
+ in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
in
Code.type_interpretation ensure_term_of_code
end
@@ -119,7 +113,7 @@
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
lemma [code, code del]:
"(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
lemma [code, code del]:
@@ -137,7 +131,7 @@
code_const Const and App
(Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
-code_const "term_of \<Colon> message_string \<Rightarrow> term"
+code_const "term_of \<Colon> String.literal \<Rightarrow> term"
(Eval "HOLogic.mk'_message'_string")
code_reserved Eval HOLogic
@@ -215,6 +209,9 @@
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
by (simp only: term_of_anything)
+lemma (in term_syntax) term_of_code_numeral_code [code]:
+ "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
+ by (simp only: term_of_anything)
subsection {* Obfuscate *}
--- a/src/HOL/Code_Index.thy Tue May 19 13:52:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,330 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Type of indices *}
-
-theory Code_Index
-imports Main
-begin
-
-text {*
- Indices are isomorphic to HOL @{typ nat} but
- mapped to target-language builtin integers.
-*}
-
-subsection {* Datatype of indices *}
-
-typedef (open) index = "UNIV \<Colon> nat set"
- morphisms nat_of of_nat by rule
-
-lemma of_nat_nat_of [simp]:
- "of_nat (nat_of k) = k"
- by (rule nat_of_inverse)
-
-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" by (rule is_measure_trivial)
-
-lemma index:
- "(\<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 (of_nat n)" .
-next
- fix n :: index
- 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 = of_nat n \<Longrightarrow> P"
- shows P
- by (rule assms [of "nat_of k"]) simp
-
-lemma index_induct_raw:
- assumes "\<And>n. P (of_nat n)"
- shows "P k"
-proof -
- from assms have "P (of_nat (nat_of k))" .
- then show ?thesis by simp
-qed
-
-lemma nat_of_inject [simp]:
- "nat_of k = nat_of l \<longleftrightarrow> k = l"
- by (rule nat_of_inject)
-
-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 = of_nat 0"
-
-instance ..
-
-end
-
-definition [simp]:
- "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 (of_nat 0)" by simp
- assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
- 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
-
-declare index_case [case_names nat, cases type: index]
-declare index.induct [case_names nat, induct type: index]
-
-lemma index_decr [termination_simp]:
- "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
- by (cases k) simp
-
-lemma [simp, code]:
- "index_size = nat_of"
-proof (rule ext)
- fix 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 k) = nat_of k" by (induct "nat_of k") simp_all
- finally show "index_size k = nat_of k" .
-qed
-
-lemma [simp, code]:
- "size = nat_of"
-proof (rule ext)
- fix k
- show "size k = nat_of k"
- by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
-qed
-
-lemmas [code del] = index.recs index.cases
-
-lemma [code]:
- "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]:
- "eq_class.eq (k::index) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
-
-
-subsection {* Indices as datatype of ints *}
-
-instantiation index :: number
-begin
-
-definition
- "number_of = of_nat o nat"
-
-instance ..
-
-end
-
-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"
-
-
-subsection {* Basic arithmetic *}
-
-instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
- "(1\<Colon>index) = of_nat 1"
-
-definition [simp, code del]:
- "n + m = of_nat (nat_of n + nat_of m)"
-
-definition [simp, code del]:
- "n - m = of_nat (nat_of n - nat_of m)"
-
-definition [simp, code del]:
- "n * m = of_nat (nat_of n * nat_of m)"
-
-definition [simp, code del]:
- "n div m = of_nat (nat_of n div nat_of m)"
-
-definition [simp, code del]:
- "n mod m = of_nat (nat_of n mod nat_of m)"
-
-definition [simp, code del]:
- "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
- "n < m \<longleftrightarrow> nat_of n < nat_of m"
-
-instance proof
-qed (auto simp add: index left_distrib div_mult_self1)
-
-end
-
-lemma zero_index_code [code inline, code]:
- "(0\<Colon>index) = Numeral0"
- by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
- using zero_index_code ..
-
-lemma one_index_code [code inline, code]:
- "(1\<Colon>index) = Numeral1"
- by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
- using one_index_code ..
-
-lemma plus_index_code [code nbe]:
- "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 (of_nat n) (of_nat m) = of_nat (n - m)"
- by simp
-
-lemma minus_index_code [code]:
- "n - m = subtract_index n m"
- by simp
-
-lemma times_index_code [code nbe]:
- "of_nat n * of_nat m = of_nat (n * m)"
- by simp
-
-lemma less_eq_index_code [code nbe]:
- "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
- by simp
-
-lemma less_index_code [code nbe]:
- "of_nat n < of_nat m \<longleftrightarrow> n < m"
- by simp
-
-lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
-
-lemma of_nat_code [code]:
- "of_nat = Nat.of_nat"
-proof
- fix n :: nat
- have "Nat.of_nat n = of_nat n"
- by (induct n) simp_all
- then show "of_nat n = Nat.of_nat n"
- by (rule sym)
-qed
-
-lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
- by (cases i) auto
-
-definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
- "nat_of_aux i n = nat_of i + n"
-
-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_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)"
-
-lemma [code]:
- "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
- unfolding div_mod_index_def by auto
-
-lemma [code]:
- "n div m = fst (div_mod_index n m)"
- unfolding div_mod_index_def by simp
-
-lemma [code]:
- "n mod m = snd (div_mod_index n m)"
- unfolding div_mod_index_def by simp
-
-definition int_of :: "index \<Rightarrow> int" where
- "int_of = Nat.of_nat o nat_of"
-
-lemma int_of_code [code]:
- "int_of k = (if k = 0 then 0
- else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
- by (auto simp add: int_of_def mod_div_equality')
-
-lemma (in term_syntax) term_of_index_code [code]:
- "Code_Eval.term_of k =
- Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k"
- by (simp only: term_of_anything)
-
-hide (open) const of_nat nat_of int_of
-
-
-subsection {* Code generator setup *}
-
-text {* Implementation of indices by bounded integers *}
-
-code_type index
- (SML "int")
- (OCaml "int")
- (Haskell "Int")
-
-code_instance index :: eq
- (Haskell -)
-
-setup {*
- fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
- false false) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML Int int
-code_reserved OCaml Pervasives int
-
-code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.+/ ((_),/ (_))")
- (OCaml "Pervasives.( + )")
- (Haskell infixl 6 "+")
-
-code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.max/ (_/ -/ _,/ 0 : int)")
- (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
- (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
-
-code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.*/ ((_),/ (_))")
- (OCaml "Pervasives.( * )")
- (Haskell infixl 7 "*")
-
-code_const div_mod_index
- (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
- (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
- (Haskell "divMod")
-
-code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "!((_ : Int.int) = _)")
- (OCaml "!((_ : int) = _)")
- (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.<=/ ((_),/ (_))")
- (OCaml "!((_ : int) <= _)")
- (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.</ ((_),/ (_))")
- (OCaml "!((_ : int) < _)")
- (Haskell infix 4 "<")
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Numeral.thy Wed May 20 15:35:22 2009 +0200
@@ -0,0 +1,325 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Type of target language numerals *}
+
+theory Code_Numeral
+imports Nat_Numeral
+begin
+
+text {*
+ Code numerals are isomorphic to HOL @{typ nat} but
+ mapped to target-language builtin numerals.
+*}
+
+subsection {* Datatype of target language numerals *}
+
+typedef (open) code_numeral = "UNIV \<Colon> nat set"
+ morphisms nat_of of_nat by rule
+
+lemma of_nat_nat_of [simp]:
+ "of_nat (nat_of k) = k"
+ by (rule nat_of_inverse)
+
+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" by (rule is_measure_trivial)
+
+lemma code_numeral:
+ "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
+proof
+ fix n :: nat
+ assume "\<And>n\<Colon>code_numeral. PROP P n"
+ then show "PROP P (of_nat n)" .
+next
+ fix n :: code_numeral
+ 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 code_numeral_case:
+ assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
+ shows P
+ by (rule assms [of "nat_of k"]) simp
+
+lemma code_numeral_induct_raw:
+ assumes "\<And>n. P (of_nat n)"
+ shows "P k"
+proof -
+ from assms have "P (of_nat (nat_of k))" .
+ then show ?thesis by simp
+qed
+
+lemma nat_of_inject [simp]:
+ "nat_of k = nat_of l \<longleftrightarrow> k = l"
+ by (rule nat_of_inject)
+
+lemma of_nat_inject [simp]:
+ "of_nat n = of_nat m \<longleftrightarrow> n = m"
+ by (rule of_nat_inject) (rule UNIV_I)+
+
+instantiation code_numeral :: zero
+begin
+
+definition [simp, code del]:
+ "0 = of_nat 0"
+
+instance ..
+
+end
+
+definition [simp]:
+ "Suc_code_numeral k = of_nat (Suc (nat_of k))"
+
+rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
+proof -
+ fix P :: "code_numeral \<Rightarrow> bool"
+ fix k :: code_numeral
+ assume "P 0" then have init: "P (of_nat 0)" by simp
+ assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
+ then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (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
+
+declare code_numeral_case [case_names nat, cases type: code_numeral]
+declare code_numeral.induct [case_names nat, induct type: code_numeral]
+
+lemma code_numeral_decr [termination_simp]:
+ "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
+ by (cases k) simp
+
+lemma [simp, code]:
+ "code_numeral_size = nat_of"
+proof (rule ext)
+ fix k
+ have "code_numeral_size k = nat_size (nat_of k)"
+ by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+ also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+ finally show "code_numeral_size k = nat_of k" .
+qed
+
+lemma [simp, code]:
+ "size = nat_of"
+proof (rule ext)
+ fix k
+ show "size k = nat_of k"
+ by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+qed
+
+lemmas [code del] = code_numeral.recs code_numeral.cases
+
+lemma [code]:
+ "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]:
+ "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
+ by (rule HOL.eq_refl)
+
+
+subsection {* Indices as datatype of ints *}
+
+instantiation code_numeral :: number
+begin
+
+definition
+ "number_of = of_nat o nat"
+
+instance ..
+
+end
+
+lemma nat_of_number [simp]:
+ "nat_of (number_of k) = number_of k"
+ by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id)
+
+code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
+
+
+subsection {* Basic arithmetic *}
+
+instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
+begin
+
+definition [simp, code del]:
+ "(1\<Colon>code_numeral) = of_nat 1"
+
+definition [simp, code del]:
+ "n + m = of_nat (nat_of n + nat_of m)"
+
+definition [simp, code del]:
+ "n - m = of_nat (nat_of n - nat_of m)"
+
+definition [simp, code del]:
+ "n * m = of_nat (nat_of n * nat_of m)"
+
+definition [simp, code del]:
+ "n div m = of_nat (nat_of n div nat_of m)"
+
+definition [simp, code del]:
+ "n mod m = of_nat (nat_of n mod nat_of m)"
+
+definition [simp, code del]:
+ "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
+
+definition [simp, code del]:
+ "n < m \<longleftrightarrow> nat_of n < nat_of m"
+
+instance proof
+qed (auto simp add: code_numeral left_distrib div_mult_self1)
+
+end
+
+lemma zero_code_numeral_code [code inline, code]:
+ "(0\<Colon>code_numeral) = Numeral0"
+ by (simp add: number_of_code_numeral_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+ using zero_code_numeral_code ..
+
+lemma one_code_numeral_code [code inline, code]:
+ "(1\<Colon>code_numeral) = Numeral1"
+ by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
+ using one_code_numeral_code ..
+
+lemma plus_code_numeral_code [code nbe]:
+ "of_nat n + of_nat m = of_nat (n + m)"
+ by simp
+
+definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+ [simp, code del]: "subtract_code_numeral = op -"
+
+lemma subtract_code_numeral_code [code nbe]:
+ "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
+ by simp
+
+lemma minus_code_numeral_code [code]:
+ "n - m = subtract_code_numeral n m"
+ by simp
+
+lemma times_code_numeral_code [code nbe]:
+ "of_nat n * of_nat m = of_nat (n * m)"
+ by simp
+
+lemma less_eq_code_numeral_code [code nbe]:
+ "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
+ by simp
+
+lemma less_code_numeral_code [code nbe]:
+ "of_nat n < of_nat m \<longleftrightarrow> n < m"
+ by simp
+
+lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
+
+lemma of_nat_code [code]:
+ "of_nat = Nat.of_nat"
+proof
+ fix n :: nat
+ have "Nat.of_nat n = of_nat n"
+ by (induct n) simp_all
+ then show "of_nat n = Nat.of_nat n"
+ by (rule sym)
+qed
+
+lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
+ by (cases i) auto
+
+definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
+ "nat_of_aux i n = nat_of i + n"
+
+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 code_numeral_not_eq_zero)
+
+lemma nat_of_code [code]:
+ "nat_of i = nat_of_aux i 0"
+ by (simp add: nat_of_aux_def)
+
+definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
+ [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
+
+lemma [code]:
+ "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+ unfolding div_mod_code_numeral_def by auto
+
+lemma [code]:
+ "n div m = fst (div_mod_code_numeral n m)"
+ unfolding div_mod_code_numeral_def by simp
+
+lemma [code]:
+ "n mod m = snd (div_mod_code_numeral n m)"
+ unfolding div_mod_code_numeral_def by simp
+
+definition int_of :: "code_numeral \<Rightarrow> int" where
+ "int_of = Nat.of_nat o nat_of"
+
+lemma int_of_code [code]:
+ "int_of k = (if k = 0 then 0
+ else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
+ by (auto simp add: int_of_def mod_div_equality')
+
+hide (open) const of_nat nat_of int_of
+
+
+subsection {* Code generator setup *}
+
+text {* Implementation of indices by bounded integers *}
+
+code_type code_numeral
+ (SML "int")
+ (OCaml "int")
+ (Haskell "Int")
+
+code_instance code_numeral :: eq
+ (Haskell -)
+
+setup {*
+ fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+ false false) ["SML", "OCaml", "Haskell"]
+*}
+
+code_reserved SML Int int
+code_reserved OCaml Pervasives int
+
+code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.+/ ((_),/ (_))")
+ (OCaml "Pervasives.( + )")
+ (Haskell infixl 6 "+")
+
+code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.max/ (_/ -/ _,/ 0 : int)")
+ (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+ (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+
+code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.*/ ((_),/ (_))")
+ (OCaml "Pervasives.( * )")
+ (Haskell infixl 7 "*")
+
+code_const div_mod_code_numeral
+ (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+ (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+ (Haskell "divMod")
+
+code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "!((_ : Int.int) = _)")
+ (OCaml "!((_ : int) = _)")
+ (Haskell infixl 4 "==")
+
+code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "Int.<=/ ((_),/ (_))")
+ (OCaml "!((_ : int) <= _)")
+ (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "Int.</ ((_),/ (_))")
+ (OCaml "!((_ : int) < _)")
+ (Haskell infix 4 "<")
+
+end
--- a/src/HOL/Complex_Main.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Complex_Main.thy Wed May 20 15:35:22 2009 +0200
@@ -9,7 +9,6 @@
Ln
Taylor
Integration
- Quickcheck
begin
end
--- a/src/HOL/Fun.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Fun.thy Wed May 20 15:35:22 2009 +0200
@@ -100,6 +100,9 @@
lemma fcomp_id [simp]: "f o> id = f"
by (simp add: fcomp_def)
+code_const fcomp
+ (Eval infixl 1 "#>")
+
no_notation fcomp (infixl "o>" 60)
--- a/src/HOL/Imperative_HOL/Array.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Wed May 20 15:35:22 2009 +0200
@@ -6,7 +6,7 @@
header {* Monadic arrays *}
theory Array
-imports Heap_Monad Code_Index
+imports Heap_Monad
begin
subsection {* Primitives *}
@@ -115,47 +115,47 @@
subsubsection {* Logical intermediate layer *}
definition new' where
- [code del]: "new' = Array.new o Code_Index.nat_of"
+ [code del]: "new' = Array.new o Code_Numeral.nat_of"
hide (open) const new'
lemma [code]:
- "Array.new = Array.new' o Code_Index.of_nat"
+ "Array.new = Array.new' o Code_Numeral.of_nat"
by (simp add: new'_def o_def)
definition of_list' where
- [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
+ [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
hide (open) const of_list'
lemma [code]:
- "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
+ "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
by (simp add: of_list'_def)
definition make' where
- [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
+ [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
hide (open) const make'
lemma [code]:
- "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
+ "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
by (simp add: make'_def o_def)
definition length' where
- [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
+ [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
hide (open) const length'
lemma [code]:
- "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
+ "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.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 Code_Index.nat_of"
+ [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
hide (open) const nth'
lemma [code]:
- "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
+ "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
by (simp add: nth'_def)
definition upd' where
- [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
+ [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
hide (open) const upd'
lemma [code]:
- "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
+ "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- a/src/HOL/Imperative_HOL/Heap.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Wed May 20 15:35:22 2009 +0200
@@ -28,11 +28,11 @@
instance int :: heap ..
-instance message_string :: countable
- by (rule countable_classI [of "message_string_case to_nat"])
- (auto split: message_string.splits)
+instance String.literal :: countable
+ by (rule countable_classI [of "String.literal_case to_nat"])
+ (auto split: String.literal.splits)
-instance message_string :: heap ..
+instance String.literal :: heap ..
text {* Reflected types themselves are heap-representable *}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed May 20 15:35:22 2009 +0200
@@ -274,7 +274,7 @@
subsubsection {* Logical intermediate layer *}
definition
- Fail :: "message_string \<Rightarrow> exception"
+ Fail :: "String.literal \<Rightarrow> exception"
where
[code del]: "Fail s = Exn"
--- a/src/HOL/IsaMakefile Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/IsaMakefile Wed May 20 15:35:22 2009 +0200
@@ -206,21 +206,23 @@
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
ATP_Linkup.thy \
Code_Eval.thy \
- Code_Index.thy \
+ Code_Numeral.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
IntDiv.thy \
Int.thy \
- Typerep.thy \
List.thy \
Main.thy \
Map.thy \
Nat_Numeral.thy \
Presburger.thy \
+ Quickcheck.thy \
+ Random.thy \
Recdef.thy \
SetInterval.thy \
String.thy \
+ Typerep.thy \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
$(SRC)/Provers/Arith/cancel_numerals.ML \
@@ -287,10 +289,8 @@
Transcendental.thy \
GCD.thy \
Parity.thy \
- Quickcheck.thy \
Lubs.thy \
PReal.thy \
- Random.thy \
Rational.thy \
RComplete.thy \
RealDef.thy \
--- a/src/HOL/Library/Bit.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Library/Bit.thy Wed May 20 15:35:22 2009 +0200
@@ -53,10 +53,10 @@
begin
definition plus_bit_def:
- "x + y = (case x of 0 \<Rightarrow> y | 1 \<Rightarrow> (case y of 0 \<Rightarrow> 1 | 1 \<Rightarrow> 0))"
+ "x + y = bit_case y (bit_case 1 0 y) x"
definition times_bit_def:
- "x * y = (case x of 0 \<Rightarrow> 0 | 1 \<Rightarrow> y)"
+ "x * y = bit_case 0 y x"
definition uminus_bit_def [simp]:
"- x = (x :: bit)"
--- a/src/HOL/Library/Code_Integer.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy Wed May 20 15:35:22 2009 +0200
@@ -5,7 +5,7 @@
header {* Pretty integer literals for code generation *}
theory Code_Integer
-imports Main Code_Index
+imports Main
begin
text {*
@@ -91,7 +91,7 @@
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
-code_const Code_Index.int_of
+code_const Code_Numeral.int_of
(SML "IntInf.fromInt")
(OCaml "Big'_int.big'_int'_of'_int")
(Haskell "toEnum")
--- a/src/HOL/Library/Efficient_Nat.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed May 20 15:35:22 2009 +0200
@@ -5,7 +5,7 @@
header {* Implementation of natural numbers by target-language integers *}
theory Efficient_Nat
-imports Code_Index Code_Integer Main
+imports Code_Integer Main
begin
text {*
@@ -369,12 +369,12 @@
text {* Conversion from and to indices. *}
-code_const Code_Index.of_nat
+code_const Code_Numeral.of_nat
(SML "IntInf.toInt")
(OCaml "Big'_int.int'_of'_big'_int")
(Haskell "fromEnum")
-code_const Code_Index.nat_of
+code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "Big'_int.big'_int'_of'_int")
(Haskell "toEnum")
--- a/src/HOL/Main.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Main.thy Wed May 20 15:35:22 2009 +0200
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Code_Eval Map Recdef SAT
+imports Plain Quickcheck Map Recdef SAT
begin
text {*
--- a/src/HOL/Product_Type.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Product_Type.thy Wed May 20 15:35:22 2009 +0200
@@ -726,6 +726,9 @@
lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
by (simp add: expand_fun_eq scomp_apply fcomp_apply)
+code_const scomp
+ (Eval infixl 3 "#->")
+
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Quickcheck.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Quickcheck.thy Wed May 20 15:35:22 2009 +0200
@@ -3,7 +3,7 @@
header {* A simple counterexample generator *}
theory Quickcheck
-imports Main Real Random
+imports Random Code_Eval
begin
notation fcomp (infixl "o>" 60)
@@ -13,7 +13,7 @@
subsection {* The @{text random} class *}
class random = typerep +
- fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+ fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
subsection {* Quickcheck generator *}
@@ -49,7 +49,7 @@
(mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
(Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
- in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
+ in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
fun compile_generator_expr thy t =
let
@@ -84,7 +84,7 @@
instantiation itself :: (typerep) random
begin
-definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
instance ..
@@ -139,7 +139,7 @@
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
begin
-definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
instance ..
@@ -154,9 +154,9 @@
instantiation nat :: random
begin
-definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
"random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
- let n = Code_Index.nat_of k
+ let n = Code_Numeral.nat_of k
in (n, \<lambda>_. Code_Eval.term_of n)))"
instance ..
@@ -168,43 +168,13 @@
definition
"random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
- let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
+ let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
in (j, \<lambda>_. Code_Eval.term_of j)))"
instance ..
end
-definition (in term_syntax)
- valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
-
-instantiation rat :: random
-begin
-
-definition
- "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
- let j = Code_Index.int_of (denom + 1)
- in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
-
-instance ..
-
-end
-
-definition (in term_syntax)
- valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
-
-instantiation real :: random
-begin
-
-definition
- "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
-
-instance ..
-
-end
-
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Random.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Random.thy Wed May 20 15:35:22 2009 +0200
@@ -3,7 +3,7 @@
header {* A HOL random engine *}
theory Random
-imports Code_Index
+imports Code_Numeral List
begin
notation fcomp (infixl "o>" 60)
@@ -12,21 +12,21 @@
subsection {* Auxiliary functions *}
-definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
+definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"inc_shift v k = (if v = k then 1 else k + 1)"
-definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
+definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"minus_shift r k l = (if k < l then r + k - l else k - l)"
-fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
+fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
subsection {* Random seeds *}
-types seed = "index \<times> index"
+types seed = "code_numeral \<times> code_numeral"
-primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
+primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
"next (v, w) = (let
k = v div 53668;
v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
@@ -42,9 +42,6 @@
primrec seed_invariant :: "seed \<Rightarrow> bool" where
"seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
-lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
- by (cases b) simp_all
-
definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
"split_seed s = (let
(v, w) = s;
@@ -58,10 +55,10 @@
subsection {* Base selectors *}
-fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
"iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
"range k = iterate (log 2147483561 k)
(\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
o\<rightarrow> (\<lambda>v. Pair (v mod k))"
@@ -71,23 +68,23 @@
by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
- "select xs = range (Code_Index.of_nat (length xs))
- o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
+ "select xs = range (Code_Numeral.of_nat (length xs))
+ o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
lemma select:
assumes "xs \<noteq> []"
shows "fst (select xs s) \<in> set xs"
proof -
- from assms have "Code_Index.of_nat (length xs) > 0" by simp
+ from assms have "Code_Numeral.of_nat (length xs) > 0" by simp
with range have
- "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
+ "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
then have
- "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
+ "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
then show ?thesis
by (simp add: scomp_apply split_beta select_def)
qed
-primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
"pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
lemma pick_member:
@@ -98,7 +95,15 @@
"pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
by (induct xs) (auto simp add: expand_fun_eq)
-definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+lemma pick_same:
+ "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
+proof (induct xs arbitrary: l)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs) then show ?case by (cases l) simp_all
+qed
+
+definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select_weight xs = range (listsum (map fst xs))
o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
@@ -113,7 +118,28 @@
then show ?thesis by (simp add: select_weight_def scomp_def split_def)
qed
-definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+lemma select_weigth_drop_zero:
+ "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
+proof -
+ have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
+ by (induct xs) auto
+ then show ?thesis by (simp only: select_weight_def pick_drop_zero)
+qed
+
+lemma select_weigth_select:
+ assumes "xs \<noteq> []"
+ shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+proof -
+ have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
+ using assms by (intro range) simp
+ moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
+ by (induct xs) simp_all
+ ultimately show ?thesis
+ by (auto simp add: select_weight_def select_def scomp_def split_def
+ expand_fun_eq pick_same [symmetric])
+qed
+
+definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
[code del]: "select_default k x y = range k
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
@@ -127,7 +153,7 @@
else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
proof
fix s
- have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
+ have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
by (simp add: range_def scomp_Pair scomp_apply split_beta)
then show "select_default k x y s = (if k = 0
then range 1 o\<rightarrow> (\<lambda>_. Pair y)
@@ -169,7 +195,6 @@
hide (open) type seed
hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
iterate range select pick select_weight select_default
-hide (open) fact log_def
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Rational.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Rational.thy Wed May 20 15:35:22 2009 +0200
@@ -1001,6 +1001,28 @@
"Fract a b / Fract c d = Fract_norm (a * d) (b * c)"
by simp
+definition (in term_syntax)
+ valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
+ [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation rat :: random
+begin
+
+definition
+ "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+ let j = Code_Numeral.int_of (denom + 1)
+ in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
hide (open) const Fract_norm
text {* Setup for SML code generator *}
--- a/src/HOL/RealDef.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/RealDef.thy Wed May 20 15:35:22 2009 +0200
@@ -1126,6 +1126,26 @@
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
by (simp add: of_rat_divide)
+definition (in term_syntax)
+ valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
+ [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation real :: random
+begin
+
+definition
+ "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
text {* Setup for SML code generator *}
types_code
--- a/src/HOL/String.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/String.thy Wed May 20 15:35:22 2009 +0200
@@ -85,15 +85,14 @@
subsection {* Strings as dedicated datatype *}
-datatype message_string = STR string
+datatype literal = STR string
-lemmas [code del] =
- message_string.recs message_string.cases
+lemmas [code del] = literal.recs literal.cases
-lemma [code]: "size (s\<Colon>message_string) = 0"
+lemma [code]: "size (s\<Colon>literal) = 0"
by (cases s) simp_all
-lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
+lemma [code]: "literal_size (s\<Colon>literal) = 0"
by (cases s) simp_all
@@ -101,19 +100,19 @@
use "Tools/string_code.ML"
-code_type message_string
+code_type literal
(SML "string")
(OCaml "string")
(Haskell "String")
setup {*
- fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
+ fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
*}
-code_instance message_string :: eq
+code_instance literal :: eq
(Haskell -)
-code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
@@ -147,4 +146,6 @@
in Codegen.add_codegen "char_codegen" char_codegen end
*}
+hide (open) type literal
+
end
\ No newline at end of file
--- a/src/HOL/Tools/datatype_package.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed May 20 15:35:22 2009 +0200
@@ -101,7 +101,7 @@
fun put_dt_infos (dt_infos : (string * datatype_info) list) =
map_datatypes (fn {types, constrs, cases} =>
{types = fold Symtab.update dt_infos types,
- constrs = fold Symtab.update
+ constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
(maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
(#3 (the (AList.lookup op = descr index)))) dt_infos) constrs,
cases = fold Symtab.update
--- a/src/HOL/Tools/hologic.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Wed May 20 15:35:22 2009 +0200
@@ -87,7 +87,7 @@
val dest_nat: term -> int
val class_size: string
val size_const: typ -> term
- val indexT: typ
+ val code_numeralT: typ
val intT: typ
val pls_const: term
val min_const: term
@@ -116,9 +116,9 @@
val stringT: typ
val mk_string: string -> term
val dest_string: term -> string
- val message_stringT: typ
- val mk_message_string: string -> term
- val dest_message_string: term -> string
+ val literalT: typ
+ val mk_literal: string -> term
+ val dest_literal: term -> string
val mk_typerep: typ -> term
val mk_term_of: typ -> term -> term
val reflect_term: term -> term
@@ -461,9 +461,9 @@
fun size_const T = Const ("Nat.size_class.size", T --> natT);
-(* index *)
+(* code numeral *)
-val indexT = Type ("Code_Index.index", []);
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
(* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
@@ -586,15 +586,15 @@
val dest_string = implode o map (chr o dest_char) o dest_list;
-(* message_string *)
+(* literal *)
-val message_stringT = Type ("String.message_string", []);
+val literalT = Type ("String.literal", []);
-fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
+fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
$ mk_string s;
-fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
+fun dest_literal (Const ("String.literal.STR", _) $ t) =
dest_string t
- | dest_message_string t = raise TERM ("dest_message_string", [t]);
+ | dest_literal t = raise TERM ("dest_literal", [t]);
(* typerep and term *)
@@ -609,8 +609,8 @@
fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
fun reflect_term (Const (c, T)) =
- Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
- $ mk_message_string c $ mk_typerep T
+ Const ("Code_Eval.Const", literalT --> typerepT --> termT)
+ $ mk_literal c $ mk_typerep T
| reflect_term (t1 $ t2) =
Const ("Code_Eval.App", termT --> termT --> termT)
$ reflect_term t1 $ reflect_term t2
--- a/src/HOL/Tools/string_code.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Tools/string_code.ML Wed May 20 15:35:22 2009 +0200
@@ -7,7 +7,7 @@
sig
val add_literal_list_string: string -> theory -> theory
val add_literal_char: string -> theory -> theory
- val add_literal_message: string -> theory -> theory
+ val add_literal_string: string -> theory -> theory
end;
structure String_Code : STRING_CODE =
@@ -72,7 +72,7 @@
@{const_name Char} (SOME (2, (cs_nibbles, pretty)))
end;
-fun add_literal_message target =
+fun add_literal_string target =
let
fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
case List_Code.implode_list nil' cons' t
--- a/src/HOL/Typerep.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Typerep.thy Wed May 20 15:35:22 2009 +0200
@@ -6,7 +6,7 @@
imports Plain String
begin
-datatype typerep = Typerep message_string "typerep list"
+datatype typerep = Typerep String.literal "typerep list"
class typerep =
fixes typerep :: "'a itself \<Rightarrow> typerep"
@@ -45,7 +45,7 @@
val ty = Type (tyco, map TFree vs);
val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
$ Free ("T", Term.itselfT ty);
- val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
+ val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
--- a/src/HOL/ex/Quickcheck_Generators.thy Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy Wed May 20 15:35:22 2009 +0200
@@ -12,11 +12,11 @@
"collapse f = (do g \<leftarrow> f; g done)"
lemma random'_if:
- fixes random' :: "index \<Rightarrow> index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+ fixes random' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
assumes "random' 0 j = (\<lambda>s. undefined)"
- and "\<And>i. random' (Suc_index i) j = rhs2 i"
+ and "\<And>i. random' (Suc_code_numeral i) j = rhs2 i"
shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
- by (cases i rule: index.exhaust) (insert assms, simp_all)
+ by (cases i rule: code_numeral.exhaust) (insert assms, simp_all)
setup {*
let
@@ -62,7 +62,7 @@
in case mk_conss thy ty ts_rec
of SOME t_rec => mk_collapse thy (term_ty ty) $
(Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $
- @{term "i\<Colon>index"} $ t_rec $ t_atom)
+ @{term "i\<Colon>code_numeral"} $ t_rec $ t_atom)
| NONE => t_atom
end;
fun mk_random_eqs thy vs tycos =
@@ -73,12 +73,12 @@
val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
val random' = Free (random'_name,
- @{typ index} --> @{typ index} --> this_ty');
+ @{typ code_numeral} --> @{typ code_numeral} --> this_ty');
fun atom ty = if Sign.of_sort thy (ty, @{sort random})
- then ((ty, false), random ty $ @{term "j\<Colon>index"})
+ then ((ty, false), random ty $ @{term "j\<Colon>code_numeral"})
else raise TYP
("Will not generate random elements for type(s) " ^ quote (hd tycos));
- fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"});
+ fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"});
fun rtyp tyco tys = raise REC
("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
val rhss = DatatypePackage.construction_interpretation thy
@@ -87,9 +87,9 @@
|> (map o apsnd) (List.partition fst)
|> map (mk_clauses thy this_ty)
val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
- (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ Random.seed},
+ (random' $ @{term "0\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"}, Abs ("s", @{typ Random.seed},
Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))),
- (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
+ (random' $ @{term "Suc_code_numeral i"} $ @{term "j\<Colon>code_numeral"}, rhs)
]))) rhss;
in eqss end;
fun random_inst [tyco] thy =
@@ -99,8 +99,8 @@
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
- random' $ @{term "max (i\<Colon>index) 1"} $ @{term "i\<Colon>index"})
+ (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>code_numeral"},
+ random' $ @{term "max (i\<Colon>code_numeral) 1"} $ @{term "i\<Colon>code_numeral"})
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
(fn thm => Context.mapping (Code.del_eqn thm) I));
fun add_code simps lthy =
--- a/src/Pure/General/table.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/Pure/General/table.ML Wed May 20 15:35:22 2009 +0200
@@ -33,11 +33,11 @@
val max_key: 'a table -> key option
val defined: 'a table -> key -> bool
val lookup: 'a table -> key -> 'a option
- val update: (key * 'a) -> 'a table -> 'a table
- val update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*)
+ val update: key * 'a -> 'a table -> 'a table
+ val update_new: key * 'a -> 'a table -> 'a table (*exception DUP*)
val default: key * 'a -> 'a table -> 'a table
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
- val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
+ val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
'a table * 'a table -> 'a table (*exception DUP*)
@@ -48,7 +48,7 @@
val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*)
val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
val lookup_list: 'a list table -> key -> 'a list
- val cons_list: (key * 'a) -> 'a list table -> 'a list table
+ val cons_list: key * 'a -> 'a list table -> 'a list table
val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
--- a/src/Pure/Isar/class_target.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Wed May 20 15:35:22 2009 +0200
@@ -441,8 +441,8 @@
fun synchronize_inst_syntax ctxt =
let
val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
- val thy = ProofContext.theory_of ctxt;
- fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
+ val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
+ fun subst (c, ty) = case inst_tyco_of (c, ty)
of SOME tyco => (case AList.lookup (op =) params (c, tyco)
of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
| NONE => NONE)
@@ -512,9 +512,11 @@
fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
of NONE => NONE
| SOME ts' => SOME (ts', ctxt);
- fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
+ val inst_tyco_of = AxClass.inst_tyco_of consts;
+ val typ_instance = Type.typ_instance (Sign.tsig_of thy);
+ fun improve (c, ty) = case inst_tyco_of (c, ty)
of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
- of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
+ of SOME (_, ty') => if typ_instance (ty', ty)
then SOME (ty, ty') else NONE
| NONE => NONE)
| NONE => NONE;
--- a/src/Pure/axclass.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/Pure/axclass.ML Wed May 20 15:35:22 2009 +0200
@@ -26,9 +26,9 @@
val axiomatize_arity: arity -> theory -> theory
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
val instance_name: string * class -> string
+ val inst_tyco_of: Consts.T -> string * typ -> string option
val declare_overloaded: string * typ -> theory -> term * theory
val define_overloaded: binding -> string * term -> theory -> thm * theory
- val inst_tyco_of: theory -> string * typ -> string option
val unoverload: theory -> thm -> thm
val overload: theory -> thm -> thm
val unoverload_conv: theory -> conv
@@ -249,7 +249,8 @@
fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
(get_inst_params thy) [];
-fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
+fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
+val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
@@ -259,7 +260,7 @@
fun unoverload_const thy (c_ty as (c, _)) =
case class_of_param thy c
- of SOME class => (case inst_tyco_of thy c_ty
+ of SOME class => (case inst_tyco_of' thy c_ty
of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
| NONE => c)
| NONE => c;
@@ -293,7 +294,7 @@
val class = case class_of_param thy c
of SOME class => class
| NONE => error ("Not a class parameter: " ^ quote c);
- val tyco = case inst_tyco_of thy (c, T)
+ val tyco = case inst_tyco_of' thy (c, T)
of SOME tyco => tyco
| NONE => error ("Illegal type for instantiation of class parameter: "
^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
@@ -318,7 +319,7 @@
fun define_overloaded b (c, t) thy =
let
val T = Term.fastype_of t;
- val SOME tyco = inst_tyco_of thy (c, T);
+ val SOME tyco = inst_tyco_of' thy (c, T);
val (c', eq) = get_inst_param thy (c, tyco);
val prop = Logic.mk_equals (Const (c', T), t);
val b' = Thm.def_binding_optional