src/HOL/Codegenerator_Test/RBT_Set_Test.thy
author Christian Sternagel
Thu Aug 30 15:44:03 2012 +0900 (2012-08-30)
changeset 49093 fdc301f592c4
parent 48624 9b71daba4ec7
child 49948 744934b818c7
permissions -rw-r--r--
forgot to add lemmas
     1 (*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
     2     Author:     Ondrej Kuncar
     3 *)
     4 
     5 header {* Test of the code generator using an implementation of sets by RBT trees *}
     6 
     7 theory RBT_Set_Test
     8 imports Library "~~/src/HOL/Library/RBT_Set"
     9 begin
    10 
    11 (* 
    12    The following code equations have to be deleted because they use 
    13    lists to implement sets in the code generetor. 
    14 *)
    15 
    16 lemma [code, code del]:
    17   "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    18 
    19 lemma [code, code del]:
    20   "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    21 
    22 lemma [code, code del]:
    23   "pred_of_set = pred_of_set" ..
    24 
    25 
    26 lemma [code, code del]:
    27   "Cardinality.card' = Cardinality.card'" ..
    28 
    29 lemma [code, code del]:
    30   "Cardinality.finite' = Cardinality.finite'" ..
    31 
    32 lemma [code, code del]:
    33   "Cardinality.subset' = Cardinality.subset'" ..
    34 
    35 lemma [code, code del]:
    36   "Cardinality.eq_set = Cardinality.eq_set" ..
    37 
    38 
    39 lemma [code, code del]:
    40   "acc = acc" ..
    41 
    42 (*
    43   If the code generation ends with an exception with the following message:
    44   '"List.set" is not a constructor, on left hand side of equation: ...',
    45   the code equation in question has to be either deleted (like many others in this file) 
    46   or implemented for RBT trees.
    47 *)
    48 
    49 export_code _ checking SML OCaml? Haskell? Scala?
    50 
    51 end