1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Nov 11 21:53:58 2009 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Nov 12 09:10:07 2009 +0100
     1.3 @@ -186,9 +186,11 @@
     1.4      @{const_name "False"},
     1.5      @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
     1.6      @{const_name Nat.one_nat_inst.one_nat},
     1.7 -@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
     1.8 +@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"},
     1.9 +@{const_name "HOL.zero_class.zero"},
    1.10  @{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
    1.11  @{const_name Nat.ord_nat_inst.less_eq_nat},
    1.12 +@{const_name Nat.ord_nat_inst.less_nat},
    1.13  @{const_name number_nat_inst.number_of_nat},
    1.14    @{const_name Int.Bit0},
    1.15    @{const_name Int.Bit1},

     2.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Nov 11 21:53:58 2009 +0100
     2.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:10:07 2009 +0100
     2.3 @@ -69,6 +69,20 @@
     2.4  code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero .
     2.5  code_pred [random] zerozero .
     2.6  
     2.7 +inductive JamesBond :: "nat => int => code_numeral => bool"
     2.8 +where
     2.9 +  "JamesBond 0 0 7"
    2.10 +
    2.11 +code_pred JamesBond .
    2.12 +
    2.13 +values "{(a, b, c). JamesBond a b c}"
    2.14 +values "{(a, c, b). JamesBond a b c}"
    2.15 +values "{(b, a, c). JamesBond a b c}"
    2.16 +values "{(b, c, a). JamesBond a b c}"
    2.17 +values "{(c, a, b). JamesBond a b c}"
    2.18 +values "{(c, b, a). JamesBond a b c}"
    2.19 +
    2.20 +
    2.21  subsection {* Alternative Rules *}
    2.22  
    2.23  datatype char = C | D | E | F | G | H
    2.24 @@ -270,8 +284,9 @@
    2.25  values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
    2.26  values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
    2.27  values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
    2.28 +
    2.29  values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    2.30 -values [random] 15 "{(ys, zs). append [1::nat, 2] ys zs}"
    2.31 +values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}"
    2.32  
    2.33  value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
    2.34  value [code] "Predicate.the (append_3 ([]::int list))"
    2.35 @@ -480,7 +495,6 @@
    2.36  values [mode: [2]] 10 "{n. tranclp succ n 10}"
    2.37  values 20 "{(n, m). tranclp succ n m}"
    2.38  
    2.39 -
    2.40  subsection {* IMP *}
    2.41  
    2.42  types
    2.43 @@ -708,21 +722,82 @@
    2.44  
    2.45  (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
    2.46  
    2.47 -code_pred [inductify] concat .
    2.48 -code_pred [inductify] hd .
    2.49 -code_pred [inductify] tl .
    2.50 +code_pred (mode: [1], [2], [1, 2]) [inductify] concat .
    2.51 +thm concatP.equation
    2.52 +
    2.53 +values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
    2.54 +values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
    2.55 +
    2.56 +code_pred [inductify, depth_limited] concat .
    2.57 +thm concatP.depth_limited_equation
    2.58 +
    2.59 +values  [depth_limit = 3] 3
    2.60 +  "{xs. concatP xs ([0] :: nat list)}"
    2.61 +
    2.62 +values [depth_limit = 5] 3
    2.63 +  "{xs. concatP xs ([1] :: int list)}"
    2.64 +
    2.65 +values [depth_limit = 5] 3
    2.66 +  "{xs. concatP xs ([1] :: nat list)}"
    2.67 +
    2.68 +values [depth_limit = 5] 3
    2.69 +  "{xs. concatP xs [(1::int), 2]}"
    2.70 +
    2.71 +code_pred (mode: [1], [1, 2]) [inductify] hd .
    2.72 +thm hdP.equation
    2.73 +values "{x. hdP [1, 2, (3::int)] x}"
    2.74 +values "{(xs, x). hdP [1, 2, (3::int)] 1}"
    2.75 + 
    2.76 +code_pred (mode: [1], [1, 2]) [inductify] tl .
    2.77 +thm tlP.equation
    2.78 +values "{x. tlP [1, 2, (3::nat)] x}"
    2.79 +values "{x. tlP [1, 2, (3::int)] [3]}"
    2.80 +
    2.81  code_pred [inductify] last .
    2.82 +thm lastP.equation
    2.83 +
    2.84  code_pred [inductify] butlast .
    2.85 +thm butlastP.equation
    2.86 +
    2.87  code_pred [inductify] take .
    2.88 +thm takeP.equation
    2.89 +
    2.90  code_pred [inductify] drop .
    2.91 +thm dropP.equation
    2.92  code_pred [inductify] zip .
    2.93 +thm zipP.equation
    2.94 +
    2.95  (*code_pred [inductify] upt .*)
    2.96  code_pred [inductify] remdups .
    2.97 +thm remdupsP.equation
    2.98 +code_pred [inductify, depth_limited] remdups .
    2.99 +values [depth_limit = 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
   2.100 +
   2.101  code_pred [inductify] remove1 .
   2.102 +thm remove1P.equation
   2.103 +values "{xs. remove1P 1 xs [2, (3::int)]}"
   2.104 +
   2.105  code_pred [inductify] removeAll .
   2.106 +thm removeAllP.equation
   2.107 +code_pred [inductify, depth_limited] removeAll .
   2.108 +
   2.109 +values [depth_limit = 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
   2.110 +
   2.111  code_pred [inductify] distinct .
   2.112 +thm distinct.equation
   2.113 +
   2.114  code_pred [inductify] replicate .
   2.115 +thm replicateP.equation
   2.116 +values 5 "{(n, xs). replicateP n (0::int) xs}"
   2.117 +
   2.118  code_pred [inductify] splice .
   2.119 +thm splice.simps
   2.120 +thm spliceP.equation
   2.121 +
   2.122 +values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
   2.123 +(* TODO: correct error messages:*)
   2.124 +(* values {(xs, ys, zs). spliceP xs ... } *)
   2.125 +
   2.126  code_pred [inductify] List.rev .
   2.127  code_pred [inductify] map .
   2.128  code_pred [inductify] foldr .
   2.129 @@ -844,4 +919,8 @@
   2.130  code_pred (mode: [1], [1, 2]) beta .
   2.131  thm beta.equation
   2.132  
   2.133 +code_pred [random] typing .
   2.134 +
   2.135 +values [random] "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
   2.136 +
   2.137  end
   2.138 \ No newline at end of file