tuned
authorhaftmann
Thu Aug 09 15:52:45 2007 +0200 (2007-08-09)
changeset 241957d1a16c77f7c
parent 24194 96013f81faef
child 24196 f1dbfd7e3223
tuned
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IntArith.thy
src/HOL/IntDiv.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/State_Monad.thy
src/HOL/Tools/ATP/reduce_axiomsN.ML
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Codegenerator_Pretty.thy
src/HOL/ex/ROOT.ML
src/Pure/Tools/codegen_thingol.ML
     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