doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
author haftmann
Thu Jan 04 17:17:48 2007 +0100 (2007-01-04)
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 22386 4ebe883b02ff
permissions -rw-r--r--
updated manual
     1 structure ROOT = 
     2 struct
     3 
     4 structure HOL = 
     5 struct
     6 
     7 datatype boola = True | False;
     8 
     9 fun nota False = True
    10   | nota True = False;
    11 
    12 fun op_conj y True = y
    13   | op_conj x False = False
    14   | op_conj True y = y
    15   | op_conj False x = False;
    16 
    17 end; (*struct HOL*)
    18 
    19 structure Nat = 
    20 struct
    21 
    22 datatype nat = Zero_nat | Suc of nat;
    23 
    24 fun less_nat Zero_nat (Suc n) = HOL.True
    25   | less_nat n Zero_nat = HOL.False
    26   | less_nat (Suc m) (Suc n) = less_nat m n;
    27 
    28 fun less_eq_nat m n = HOL.nota (less_nat n m);
    29 
    30 end; (*struct Nat*)
    31 
    32 structure Codegen = 
    33 struct
    34 
    35 fun in_interval (k, l) n =
    36   HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    37 
    38 end; (*struct Codegen*)
    39 
    40 end; (*struct ROOT*)