adaptions to improvements
authorhaftmann
Mon Aug 14 13:46:17 2006 +0200 (2006-08-14)
changeset 2038358f65fc90cf4
parent 20382 39964c8dcd54
child 20384 049d955cf716
adaptions to improvements
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/ex/Classpackage.thy	Mon Aug 14 13:46:16 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Mon Aug 14 13:46:17 2006 +0200
     1.3 @@ -211,18 +211,12 @@
     1.4    with cancel show ?thesis ..
     1.5  qed
     1.6  
     1.7 -interpretation group < monoid
     1.8 +instance group < monoid
     1.9  proof -
    1.10 -  fix x :: "'a"
    1.11 +  fix x
    1.12    from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
    1.13  qed
    1.14  
    1.15 -instance group < monoid
    1.16 -proof
    1.17 -  fix x :: "'a\<Colon>group"
    1.18 -  from group.neutr show "x \<otimes> \<one> = x" .
    1.19 -qed
    1.20 -
    1.21  lemma (in group) all_inv [intro]:
    1.22    "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
    1.23    unfolding units_def
    1.24 @@ -305,12 +299,17 @@
    1.25  by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
    1.26  
    1.27  definition
    1.28 -  "x = ((2\<Colon>nat) \<otimes> \<one> \<otimes> 3, (2\<Colon>int) \<otimes> \<one> \<otimes> \<div> 3, [1\<Colon>nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
    1.29 -  "y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
    1.30 +  "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
    1.31 +  "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
    1.32 +
    1.33 +definition
    1.34 +  "x1 = X (1::nat) 2 3"
    1.35 +  "x2 = X (1::int) 2 3"
    1.36 +  "y2 = Y (1::int) 2 3"
    1.37  
    1.38  code_generate "op \<otimes>" \<one> inv
    1.39 -code_generate (ml, haskell) x
    1.40 -code_generate (ml, haskell) y
    1.41 +code_generate (ml, haskell) X Y
    1.42 +code_generate (ml, haskell) x1 x2 y2
    1.43  
    1.44  code_serialize ml (-)
    1.45  
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Aug 14 13:46:16 2006 +0200
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Aug 14 13:46:17 2006 +0200
     2.3 @@ -85,24 +85,24 @@
     2.4    h :: nat
     2.5    "h = g"
     2.6  
     2.7 -code_alias
     2.8 -  "Codegenerator.f" "Mymod.f"
     2.9 -  "Codegenerator.g" "Mymod.A.f"
    2.10 -  "Codegenerator.h" "Mymod.A.B.f"
    2.11 +code_constname
    2.12 +  f "Mymod.f"
    2.13 +  g "Mymod.A.f"
    2.14 +  h "Mymod.A.B.f"
    2.15  
    2.16  code_generate (ml, haskell)
    2.17    n one "0::int" "0::nat" "1::int" "1::nat"
    2.18  code_generate (ml, haskell)
    2.19    fac
    2.20 -code_generate (ml, haskell)
    2.21 +code_generate
    2.22    xor
    2.23 -code_generate (ml, haskell)
    2.24 +code_generate
    2.25    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.26    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.27    "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.28    "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
    2.29    "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
    2.30 -code_generate (ml, haskell)
    2.31 +code_generate
    2.32    Pair fst snd Let split swap swapp appl
    2.33  code_generate (ml, haskell)
    2.34    k
    2.35 @@ -114,13 +114,13 @@
    2.36    fac
    2.37    "op div :: int \<Rightarrow> int \<Rightarrow> int"
    2.38    "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    2.39 -code_generate (ml, haskell)
    2.40 +code_generate
    2.41    Inl Inr
    2.42 -code_generate (ml, haskell)
    2.43 +code_generate
    2.44    None Some
    2.45 -code_generate (ml, haskell)
    2.46 +code_generate
    2.47    hd tl "op @" ps qs
    2.48 -code_generate (ml, haskell)
    2.49 +code_generate
    2.50    mut1 mut2
    2.51  code_generate (ml, haskell)
    2.52    "op @" filter concat foldl foldr hd tl
    2.53 @@ -143,7 +143,7 @@
    2.54    rotate1
    2.55    rotate
    2.56    splice
    2.57 -code_generate (ml, haskell)
    2.58 +code_generate
    2.59    foo1 foo3
    2.60  code_generate (ml, haskell)
    2.61    "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    2.62 @@ -153,9 +153,10 @@
    2.63    "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    2.64    "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
    2.65    "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.66 +  "op = :: point \<Rightarrow> point \<Rightarrow> bool"
    2.67    "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    2.68    "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    2.69 -code_generate (ml, haskell)
    2.70 +code_generate
    2.71    f g h
    2.72  
    2.73  code_serialize ml (-)