--- a/src/HOL/Hyperreal/StarClasses.thy Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy Thu Aug 09 15:52:45 2007 +0200
@@ -463,7 +463,7 @@
by transfer (rule refl)
instance star :: (semiring_char_0) semiring_char_0
-by (intro_classes, simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
+by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
instance star :: (ring_char_0) ring_char_0 ..
--- a/src/HOL/IntArith.thy Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/IntArith.thy Thu Aug 09 15:52:45 2007 +0200
@@ -196,7 +196,7 @@
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L & ?R)")
proof (cases "i < 0")
- case True thus ?thesis by simp
+ case True thus ?thesis by auto
next
case False
have "?P = ?L"
@@ -264,11 +264,12 @@
by (rule wf_subset [OF wf_measure])
qed
- (* `set:int': dummy construction *)
-theorem int_ge_induct[case_names base step,induct set:int]:
- assumes ge: "k \<le> (i::int)" and
- base: "P(k)" and
- step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
+(* `set:int': dummy construction *)
+theorem int_ge_induct [case_names base step, induct set:int]:
+ fixes i :: int
+ assumes ge: "k \<le> i" and
+ base: "P k" and
+ step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
shows "P i"
proof -
{ fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
@@ -278,7 +279,7 @@
thus "P i" using base by simp
next
case (Suc n)
- hence "n = nat((i - 1) - k)" by arith
+ then have "n = nat((i - 1) - k)" by arith
moreover
have ki1: "k \<le> i - 1" using Suc.prems by arith
ultimately
--- a/src/HOL/IntDiv.thy Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/IntDiv.thy Thu Aug 09 15:52:45 2007 +0200
@@ -1446,6 +1446,6 @@
IntDiv Integer
code_modulename Haskell
- IntDiv Divides
+ IntDiv Integer
end
--- a/src/HOL/Library/Efficient_Nat.thy Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Aug 09 15:52:45 2007 +0200
@@ -401,6 +401,7 @@
code_modulename Haskell
Nat Integer
+ Divides Integer
Efficient_Nat Integer
hide const nat_of_int int'
--- a/src/HOL/Library/State_Monad.thy Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/Library/State_Monad.thy Thu Aug 09 15:52:45 2007 +0200
@@ -221,26 +221,22 @@
"_do f" => "CONST run f"
"_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
"_fcomp f g" => "f \<guillemotright> g"
- "_let x t f" => "Let t (\<lambda>x. f)"
+ "_let x t f" => "CONST Let t (\<lambda>x. f)"
"_nil f" => "f"
print_translation {*
let
- val name_mbind = @{const_syntax "mbind"};
- val name_fcomp = @{const_syntax "fcomp"};
- fun unfold_monad (t as Const (name, _) $ f $ g) =
- if name = name_mbind then let
- val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
- in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
- else if name = name_fcomp then
- Const ("_fcomp", dummyT) $ f $ unfold_monad g
- else t
- | unfold_monad (Const ("Let", _) $ f $ g) =
+ fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
let
-
+ val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
+ in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+ | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
+ Const ("_fcomp", dummyT) $ f $ unfold_monad g
+ | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
+ let
val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
- | unfold_monad (Const ("Pair", _) $ f) =
+ | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
Const ("return", dummyT) $ f
| unfold_monad f = f;
fun tr' (f::ts) =
@@ -248,6 +244,7 @@
in [(@{const_syntax "run"}, tr')] end;
*}
+
subsection {* Combinators *}
definition
@@ -258,12 +255,10 @@
list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
"list f [] = id"
| "list f (x#xs) = (do f x; list f xs done)"
-lemmas [code] = list.simps
fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
"list_yield f [] = return []"
| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
-lemmas [code] = list_yield.simps
text {* combinator properties *}
@@ -304,7 +299,7 @@
*}
text {*
- For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
+ For an example, see HOL/ex/Random.thy.
*}
end
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Thu Aug 09 15:52:45 2007 +0200
@@ -138,7 +138,7 @@
(*The frequency of a constant is the sum of those of all instances of its type.*)
fun const_frequency ctab (c, cts) =
- let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
+ let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
fun add ((cts',m), n) = if match_types cts cts' then m+n else n
in List.foldl add 0 pairs end;
--- a/src/HOL/ex/Codegenerator.thy Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy Thu Aug 09 15:52:45 2007 +0200
@@ -11,8 +11,5 @@
code_gen "*" in SML to CodegenTest
in OCaml file -
in Haskell file -
-code_gen in SML to CodegenTest
- in OCaml file -
- in Haskell file -
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Thu Aug 09 15:52:45 2007 +0200
@@ -0,0 +1,57 @@
+(* Title: HOL/ex/Codegenerator_Pretty.thy
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Simple examples for pretty numerals and such *}
+
+theory Codegenerator_Pretty
+imports Executable_Rat Executable_Real Efficient_Nat
+begin
+
+definition
+ foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
+ "foo r s t = (t + s) / t"
+
+definition
+ bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
+ "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
+
+definition
+ "R1 = Fract 3 7"
+
+definition
+ "R2 = Fract (-7) 5"
+
+definition
+ "R3 = Fract 11 (-9)"
+
+definition
+ "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
+
+definition
+ foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
+ "foo' r s t = (t + s) / t"
+
+definition
+ bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
+ "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
+
+definition
+ "R1' = real_of_rat (Fract 3 7)"
+
+definition
+ "R2' = real_of_rat (Fract (-7) 5)"
+
+definition
+ "R3' = real_of_rat (Fract 11 (-9))"
+
+definition
+ "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
+
+code_gen foobar foobar' in SML to Foo
+ in OCaml file -
+ in Haskell file -
+ML {* (Foo.foobar, Foo.foobar') *}
+
+end
--- a/src/HOL/ex/ROOT.ML Thu Aug 09 15:52:42 2007 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Aug 09 15:52:45 2007 +0200
@@ -18,8 +18,8 @@
no_document time_use_thy "Executable_Rat";
no_document time_use_thy "Efficient_Nat";
-time_use_thy "Codegenerator_Rat";
no_document time_use_thy "Codegenerator";
+no_document time_use_thy "Codegenerator_Pretty";
time_use_thy "Higher_Order_Logic";
time_use_thy "Abstract_NAT";
--- a/src/Pure/Tools/codegen_thingol.ML Thu Aug 09 15:52:42 2007 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Thu Aug 09 15:52:45 2007 +0200
@@ -70,12 +70,12 @@
type code = def Graph.T;
type transact;
val empty_code: code;
- val get_def: code -> string -> def;
val merge_code: code * code -> code;
val project_code: bool (*delete empty funs*)
-> string list (*hidden*) -> string list option (*selected*)
-> code -> code;
val empty_funs: code -> string list;
+ val is_cons: code -> string -> bool;
val add_eval_def: string (*bind name*) * iterm -> code -> code;
val ensure_def: (string -> string) -> (transact -> def * code) -> string
@@ -264,16 +264,14 @@
val empty_code = Graph.empty : code; (*read: "depends on"*)
-val get_def = Graph.get_node;
-
fun ensure_bot name = Graph.default_node (name, Bot);
fun add_def_incr (name, Bot) code =
- (case the_default Bot (try (get_def code) name)
+ (case the_default Bot (try (Graph.get_node code) name)
of Bot => error "Attempted to add Bot to code"
| _ => code)
| add_def_incr (name, def) code =
- (case try (get_def code) name
+ (case try (Graph.get_node code) name
of NONE => Graph.new_node (name, def) code
| SOME Bot => Graph.map_node name (K def) code
| SOME _ => error ("Tried to overwrite definition " ^ quote name));
@@ -285,7 +283,7 @@
fun project_code delete_empty_funs hidden raw_selected code =
let
- fun is_empty_fun name = case get_def code name
+ fun is_empty_fun name = case Graph.get_node code name
of Fun ([], _) => true
| _ => false;
val names = subtract (op =) hidden (Graph.keys code);
@@ -307,6 +305,10 @@
Graph.fold (fn (name, (Fun ([], _), _)) => cons name
| _ => I) code [];
+fun is_cons code name = case Graph.get_node code name
+ of Datatypecons _ => true
+ | _ => false;
+
fun check_samemodule names =
fold (fn name =>
let
@@ -345,7 +347,7 @@
error "Attempted to add bare class relation"
| check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
let
- val Class (_, (_, classops)) = get_def code class;
+ val Class (_, (_, classops)) = Graph.get_node code class;
val _ = if length inst_classops > length classops
then error "Too many class operations given"
else ();
@@ -405,7 +407,7 @@
add_dp dep;
in
code
- |> add_def (can (get_def code) name)
+ |> add_def (can (Graph.get_node code) name)
|> pair dep
end;