1.1 --- a/src/HOL/Hyperreal/StarClasses.thy Thu Aug 09 15:52:42 2007 +0200
1.2 +++ b/src/HOL/Hyperreal/StarClasses.thy Thu Aug 09 15:52:45 2007 +0200
1.3 @@ -463,7 +463,7 @@
1.4 by transfer (rule refl)
1.5
1.6 instance star :: (semiring_char_0) semiring_char_0
1.7 -by (intro_classes, simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
1.8 +by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
1.9
1.10 instance star :: (ring_char_0) ring_char_0 ..
1.11
2.1 --- a/src/HOL/IntArith.thy Thu Aug 09 15:52:42 2007 +0200
2.2 +++ b/src/HOL/IntArith.thy Thu Aug 09 15:52:45 2007 +0200
2.3 @@ -196,7 +196,7 @@
2.4 "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
2.5 (is "?P = (?L & ?R)")
2.6 proof (cases "i < 0")
2.7 - case True thus ?thesis by simp
2.8 + case True thus ?thesis by auto
2.9 next
2.10 case False
2.11 have "?P = ?L"
2.12 @@ -264,11 +264,12 @@
2.13 by (rule wf_subset [OF wf_measure])
2.14 qed
2.15
2.16 - (* `set:int': dummy construction *)
2.17 -theorem int_ge_induct[case_names base step,induct set:int]:
2.18 - assumes ge: "k \<le> (i::int)" and
2.19 - base: "P(k)" and
2.20 - step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
2.21 +(* `set:int': dummy construction *)
2.22 +theorem int_ge_induct [case_names base step, induct set:int]:
2.23 + fixes i :: int
2.24 + assumes ge: "k \<le> i" and
2.25 + base: "P k" and
2.26 + step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
2.27 shows "P i"
2.28 proof -
2.29 { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
2.30 @@ -278,7 +279,7 @@
2.31 thus "P i" using base by simp
2.32 next
2.33 case (Suc n)
2.34 - hence "n = nat((i - 1) - k)" by arith
2.35 + then have "n = nat((i - 1) - k)" by arith
2.36 moreover
2.37 have ki1: "k \<le> i - 1" using Suc.prems by arith
2.38 ultimately
3.1 --- a/src/HOL/IntDiv.thy Thu Aug 09 15:52:42 2007 +0200
3.2 +++ b/src/HOL/IntDiv.thy Thu Aug 09 15:52:45 2007 +0200
3.3 @@ -1446,6 +1446,6 @@
3.4 IntDiv Integer
3.5
3.6 code_modulename Haskell
3.7 - IntDiv Divides
3.8 + IntDiv Integer
3.9
3.10 end
4.1 --- a/src/HOL/Library/Efficient_Nat.thy Thu Aug 09 15:52:42 2007 +0200
4.2 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Aug 09 15:52:45 2007 +0200
4.3 @@ -401,6 +401,7 @@
4.4
4.5 code_modulename Haskell
4.6 Nat Integer
4.7 + Divides Integer
4.8 Efficient_Nat Integer
4.9
4.10 hide const nat_of_int int'
5.1 --- a/src/HOL/Library/State_Monad.thy Thu Aug 09 15:52:42 2007 +0200
5.2 +++ b/src/HOL/Library/State_Monad.thy Thu Aug 09 15:52:45 2007 +0200
5.3 @@ -221,26 +221,22 @@
5.4 "_do f" => "CONST run f"
5.5 "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
5.6 "_fcomp f g" => "f \<guillemotright> g"
5.7 - "_let x t f" => "Let t (\<lambda>x. f)"
5.8 + "_let x t f" => "CONST Let t (\<lambda>x. f)"
5.9 "_nil f" => "f"
5.10
5.11 print_translation {*
5.12 let
5.13 - val name_mbind = @{const_syntax "mbind"};
5.14 - val name_fcomp = @{const_syntax "fcomp"};
5.15 - fun unfold_monad (t as Const (name, _) $ f $ g) =
5.16 - if name = name_mbind then let
5.17 - val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
5.18 - in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
5.19 - else if name = name_fcomp then
5.20 - Const ("_fcomp", dummyT) $ f $ unfold_monad g
5.21 - else t
5.22 - | unfold_monad (Const ("Let", _) $ f $ g) =
5.23 + fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
5.24 let
5.25 -
5.26 + val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
5.27 + in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
5.28 + | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
5.29 + Const ("_fcomp", dummyT) $ f $ unfold_monad g
5.30 + | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
5.31 + let
5.32 val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
5.33 in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
5.34 - | unfold_monad (Const ("Pair", _) $ f) =
5.35 + | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
5.36 Const ("return", dummyT) $ f
5.37 | unfold_monad f = f;
5.38 fun tr' (f::ts) =
5.39 @@ -248,6 +244,7 @@
5.40 in [(@{const_syntax "run"}, tr')] end;
5.41 *}
5.42
5.43 +
5.44 subsection {* Combinators *}
5.45
5.46 definition
5.47 @@ -258,12 +255,10 @@
5.48 list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
5.49 "list f [] = id"
5.50 | "list f (x#xs) = (do f x; list f xs done)"
5.51 -lemmas [code] = list.simps
5.52
5.53 fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
5.54 "list_yield f [] = return []"
5.55 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
5.56 -lemmas [code] = list_yield.simps
5.57
5.58 text {* combinator properties *}
5.59
5.60 @@ -304,7 +299,7 @@
5.61 *}
5.62
5.63 text {*
5.64 - For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
5.65 + For an example, see HOL/ex/Random.thy.
5.66 *}
5.67
5.68 end
6.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Thu Aug 09 15:52:42 2007 +0200
6.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Thu Aug 09 15:52:45 2007 +0200
6.3 @@ -138,7 +138,7 @@
6.4
6.5 (*The frequency of a constant is the sum of those of all instances of its type.*)
6.6 fun const_frequency ctab (c, cts) =
6.7 - let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
6.8 + let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
6.9 fun add ((cts',m), n) = if match_types cts cts' then m+n else n
6.10 in List.foldl add 0 pairs end;
6.11
7.1 --- a/src/HOL/ex/Codegenerator.thy Thu Aug 09 15:52:42 2007 +0200
7.2 +++ b/src/HOL/ex/Codegenerator.thy Thu Aug 09 15:52:45 2007 +0200
7.3 @@ -11,8 +11,5 @@
7.4 code_gen "*" in SML to CodegenTest
7.5 in OCaml file -
7.6 in Haskell file -
7.7 -code_gen in SML to CodegenTest
7.8 - in OCaml file -
7.9 - in Haskell file -
7.10
7.11 end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Thu Aug 09 15:52:45 2007 +0200
8.3 @@ -0,0 +1,57 @@
8.4 +(* Title: HOL/ex/Codegenerator_Pretty.thy
8.5 + ID: $Id$
8.6 + Author: Florian Haftmann, TU Muenchen
8.7 +*)
8.8 +
8.9 +header {* Simple examples for pretty numerals and such *}
8.10 +
8.11 +theory Codegenerator_Pretty
8.12 +imports Executable_Rat Executable_Real Efficient_Nat
8.13 +begin
8.14 +
8.15 +definition
8.16 + foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
8.17 + "foo r s t = (t + s) / t"
8.18 +
8.19 +definition
8.20 + bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
8.21 + "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
8.22 +
8.23 +definition
8.24 + "R1 = Fract 3 7"
8.25 +
8.26 +definition
8.27 + "R2 = Fract (-7) 5"
8.28 +
8.29 +definition
8.30 + "R3 = Fract 11 (-9)"
8.31 +
8.32 +definition
8.33 + "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
8.34 +
8.35 +definition
8.36 + foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
8.37 + "foo' r s t = (t + s) / t"
8.38 +
8.39 +definition
8.40 + bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
8.41 + "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
8.42 +
8.43 +definition
8.44 + "R1' = real_of_rat (Fract 3 7)"
8.45 +
8.46 +definition
8.47 + "R2' = real_of_rat (Fract (-7) 5)"
8.48 +
8.49 +definition
8.50 + "R3' = real_of_rat (Fract 11 (-9))"
8.51 +
8.52 +definition
8.53 + "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
8.54 +
8.55 +code_gen foobar foobar' in SML to Foo
8.56 + in OCaml file -
8.57 + in Haskell file -
8.58 +ML {* (Foo.foobar, Foo.foobar') *}
8.59 +
8.60 +end
9.1 --- a/src/HOL/ex/ROOT.ML Thu Aug 09 15:52:42 2007 +0200
9.2 +++ b/src/HOL/ex/ROOT.ML Thu Aug 09 15:52:45 2007 +0200
9.3 @@ -18,8 +18,8 @@
9.4
9.5 no_document time_use_thy "Executable_Rat";
9.6 no_document time_use_thy "Efficient_Nat";
9.7 -time_use_thy "Codegenerator_Rat";
9.8 no_document time_use_thy "Codegenerator";
9.9 +no_document time_use_thy "Codegenerator_Pretty";
9.10
9.11 time_use_thy "Higher_Order_Logic";
9.12 time_use_thy "Abstract_NAT";
10.1 --- a/src/Pure/Tools/codegen_thingol.ML Thu Aug 09 15:52:42 2007 +0200
10.2 +++ b/src/Pure/Tools/codegen_thingol.ML Thu Aug 09 15:52:45 2007 +0200
10.3 @@ -70,12 +70,12 @@
10.4 type code = def Graph.T;
10.5 type transact;
10.6 val empty_code: code;
10.7 - val get_def: code -> string -> def;
10.8 val merge_code: code * code -> code;
10.9 val project_code: bool (*delete empty funs*)
10.10 -> string list (*hidden*) -> string list option (*selected*)
10.11 -> code -> code;
10.12 val empty_funs: code -> string list;
10.13 + val is_cons: code -> string -> bool;
10.14 val add_eval_def: string (*bind name*) * iterm -> code -> code;
10.15
10.16 val ensure_def: (string -> string) -> (transact -> def * code) -> string
10.17 @@ -264,16 +264,14 @@
10.18
10.19 val empty_code = Graph.empty : code; (*read: "depends on"*)
10.20
10.21 -val get_def = Graph.get_node;
10.22 -
10.23 fun ensure_bot name = Graph.default_node (name, Bot);
10.24
10.25 fun add_def_incr (name, Bot) code =
10.26 - (case the_default Bot (try (get_def code) name)
10.27 + (case the_default Bot (try (Graph.get_node code) name)
10.28 of Bot => error "Attempted to add Bot to code"
10.29 | _ => code)
10.30 | add_def_incr (name, def) code =
10.31 - (case try (get_def code) name
10.32 + (case try (Graph.get_node code) name
10.33 of NONE => Graph.new_node (name, def) code
10.34 | SOME Bot => Graph.map_node name (K def) code
10.35 | SOME _ => error ("Tried to overwrite definition " ^ quote name));
10.36 @@ -285,7 +283,7 @@
10.37
10.38 fun project_code delete_empty_funs hidden raw_selected code =
10.39 let
10.40 - fun is_empty_fun name = case get_def code name
10.41 + fun is_empty_fun name = case Graph.get_node code name
10.42 of Fun ([], _) => true
10.43 | _ => false;
10.44 val names = subtract (op =) hidden (Graph.keys code);
10.45 @@ -307,6 +305,10 @@
10.46 Graph.fold (fn (name, (Fun ([], _), _)) => cons name
10.47 | _ => I) code [];
10.48
10.49 +fun is_cons code name = case Graph.get_node code name
10.50 + of Datatypecons _ => true
10.51 + | _ => false;
10.52 +
10.53 fun check_samemodule names =
10.54 fold (fn name =>
10.55 let
10.56 @@ -345,7 +347,7 @@
10.57 error "Attempted to add bare class relation"
10.58 | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
10.59 let
10.60 - val Class (_, (_, classops)) = get_def code class;
10.61 + val Class (_, (_, classops)) = Graph.get_node code class;
10.62 val _ = if length inst_classops > length classops
10.63 then error "Too many class operations given"
10.64 else ();
10.65 @@ -405,7 +407,7 @@
10.66 add_dp dep;
10.67 in
10.68 code
10.69 - |> add_def (can (get_def code) name)
10.70 + |> add_def (can (Graph.get_node code) name)
10.71 |> pair dep
10.72 end;
10.73