adjusted to new fun''
authorhaftmann
Mon Nov 13 15:55:38 2006 +0100 (2006-11-13)
changeset 213413844037a8e2d
parent 21340 51d9bf0b821f
child 21342 223a3de1222b
adjusted to new fun''
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 13 15:45:34 2006 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 13 15:55:38 2006 +0100
     1.3 @@ -546,7 +546,6 @@
     1.4  fun
     1.5    in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
     1.6    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
     1.7 -termination by (auto_term "{}")
     1.8  (*<*)
     1.9  declare in_interval.simps [code func]
    1.10  (*>*)
    1.11 @@ -718,7 +717,6 @@
    1.12        then collect_duplicates xs ys zs
    1.13        else collect_duplicates xs (z#ys) zs
    1.14      else collect_duplicates (z#xs) (z#ys) zs)"
    1.15 -termination by (auto_term "measure (length o snd o snd)")
    1.16  (*<*)
    1.17  lemmas [code func] = collect_duplicates.simps
    1.18  (*>*)
    1.19 @@ -809,7 +807,6 @@
    1.20    lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
    1.21    "lookup [] l = None"
    1.22    "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
    1.23 -termination by (auto_term "measure (length o fst)")
    1.24  (*<*)
    1.25  lemmas [code func] = lookup.simps
    1.26  (*>*)
    1.27 @@ -1115,7 +1112,6 @@
    1.28    dummy_option :: "'a list \<Rightarrow> 'a option" where
    1.29    "dummy_option (x#xs) = Some x"
    1.30    "dummy_option [] = arbitrary"
    1.31 -termination by (auto_term "{}")
    1.32  (*<*)
    1.33  declare dummy_option.simps [code func]
    1.34  (*>*)
    1.35 @@ -1184,7 +1180,7 @@
    1.36  
    1.37  text %mlref {*
    1.38    \begin{mldecls}
    1.39 -  @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"}
    1.40 +  @{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"}
    1.41    \end{mldecls}
    1.42  
    1.43    \begin{description}
    1.44 @@ -1201,7 +1197,7 @@
    1.45    \begin{mldecls}
    1.46    @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
    1.47    @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
    1.48 -  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\
    1.49 +  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
    1.50    @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
    1.51    @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
    1.52    @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list)
    1.53 @@ -1209,7 +1205,7 @@
    1.54    @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list)
    1.55      -> theory -> theory"} \\
    1.56    @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
    1.57 -    * CodegenData.lthms) -> theory -> theory"} \\
    1.58 +    * thm list Susp.T) -> theory -> theory"} \\
    1.59    @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
    1.60    @{index_ML CodegenData.get_datatype: "theory -> string
    1.61      -> ((string * sort) list * (string * typ list) list) option"} \\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Mon Nov 13 15:55:38 2006 +0100
     2.3 @@ -0,0 +1,32 @@
     2.4 +structure ROOT = 
     2.5 +struct
     2.6 +
     2.7 +structure HOL = 
     2.8 +struct
     2.9 +
    2.10 +fun nota false = true
    2.11 +  | nota true = false;
    2.12 +
    2.13 +end; (*struct HOL*)
    2.14 +
    2.15 +structure Nat = 
    2.16 +struct
    2.17 +
    2.18 +datatype nat = Zero_nat | Suc of nat;
    2.19 +
    2.20 +fun less_nat Zero_nat (Suc n) = true
    2.21 +  | less_nat n Zero_nat = false
    2.22 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    2.23 +
    2.24 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    2.25 +
    2.26 +end; (*struct Nat*)
    2.27 +
    2.28 +structure Codegen = 
    2.29 +struct
    2.30 +
    2.31 +fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    2.32 +
    2.33 +end; (*struct Codegen*)
    2.34 +
    2.35 +end; (*struct ROOT*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Mon Nov 13 15:55:38 2006 +0100
     3.3 @@ -0,0 +1,40 @@
     3.4 +structure ROOT = 
     3.5 +struct
     3.6 +
     3.7 +structure HOL = 
     3.8 +struct
     3.9 +
    3.10 +datatype boola = True | False;
    3.11 +
    3.12 +fun nota False = True
    3.13 +  | nota True = False;
    3.14 +
    3.15 +fun op_conj y True = y
    3.16 +  | op_conj x False = False
    3.17 +  | op_conj True y = y
    3.18 +  | op_conj False x = False;
    3.19 +
    3.20 +end; (*struct HOL*)
    3.21 +
    3.22 +structure Nat = 
    3.23 +struct
    3.24 +
    3.25 +datatype nat = Zero_nat | Suc of nat;
    3.26 +
    3.27 +fun less_nat Zero_nat (Suc n) = HOL.True
    3.28 +  | less_nat n Zero_nat = HOL.False
    3.29 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    3.30 +
    3.31 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    3.32 +
    3.33 +end; (*struct Nat*)
    3.34 +
    3.35 +structure Codegen = 
    3.36 +struct
    3.37 +
    3.38 +fun in_interval (k, l) n =
    3.39 +  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    3.40 +
    3.41 +end; (*struct Codegen*)
    3.42 +
    3.43 +end; (*struct ROOT*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Mon Nov 13 15:55:38 2006 +0100
     4.3 @@ -0,0 +1,33 @@
     4.4 +structure ROOT = 
     4.5 +struct
     4.6 +
     4.7 +structure HOL = 
     4.8 +struct
     4.9 +
    4.10 +fun nota false = true
    4.11 +  | nota true = false;
    4.12 +
    4.13 +end; (*struct HOL*)
    4.14 +
    4.15 +structure Nat = 
    4.16 +struct
    4.17 +
    4.18 +datatype nat = Zero_nat | Suc of nat;
    4.19 +
    4.20 +fun less_nat Zero_nat (Suc n) = true
    4.21 +  | less_nat n Zero_nat = false
    4.22 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    4.23 +
    4.24 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    4.25 +
    4.26 +end; (*struct Nat*)
    4.27 +
    4.28 +structure Codegen = 
    4.29 +struct
    4.30 +
    4.31 +fun in_interval (k, l) n =
    4.32 +  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    4.33 +
    4.34 +end; (*struct Codegen*)
    4.35 +
    4.36 +end; (*struct ROOT*)