Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)

Copyright (c) 2002-5 CUTS and contributors.

Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)

Mapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOL

Mapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOL" (required by "mrec3_h")

Loading theory "mrec3_h"

structure Header :

sig val initialize : string list -> unit val record : string -> unit end

val it = () : unit

Proofs for datatype(s) "Prelude_Boolx"

Constructing representing sets ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the induction rule ...

Proving isomorphism properties ...

Proving freeness of constructors ...

Proving induction rule for datatypes ...

Proving case distinction theorems ...

Constructing primrec combinators ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the elimination rules ...

Proving termination and uniqueness of primrec functions ...

Proving characteristic theorems for primrec combinators ...

Proving characteristic theorems for case combinators ...

Proving equations for case splitting ...

Proving additional theorems for TFL ...

Proving equations for size function ...

Proofs for datatype(s) "Prelude_Natx"

Constructing representing sets ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the induction rule ...

Proving isomorphism properties ...

Proving freeness of constructors ...

Proving induction rule for datatypes ...

Proving case distinction theorems ...

Constructing primrec combinators ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the elimination rules ...

Proving termination and uniqueness of primrec functions ...

Proving characteristic theorems for primrec combinators ...

Proving characteristic theorems for case combinators ...

Proving equations for case splitting ...

Proving additional theorems for TFL ...

Proving equations for size function ...

Proving equations for primrec function(s) "mrec3_h.map1_Xmap2_X" ...

val it = () : unit

val it = () : unit

val it =

{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,

Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,

Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,

Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,

Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,

Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,

Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,

Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,

Main, HsHOL, mrec3_h} : Theory.theory

val it =

[("mrec3_h.map1_def", "map1 == %x. fst (map1_Xmap2_X x)"),

("mrec3_h.map2_def", "map2 == %x. snd (map1_Xmap2_X x)"),

("mrec3_h.Prelude_Natx.Sx_def",

"Sx ?x1.0 ==

Abs_Prelude_Natx

(In1 (In0 (??.Datatype_Universe.Leaf (Inr ?x1.0))))"),

("mrec3_h.Prelude_Natx.Zx_def",

"Zx == Abs_Prelude_Natx (In0 arbitrary)"),

("mrec3_h.Prelude_Natx.SSx_def",

"SSx ?x2.0 ?x1.0 ==

Abs_Prelude_Natx

(In1

(In1

(Scons (Rep_Prelude_Natx ?x2.0)

(??.Datatype_Universe.Leaf (Inl ?x1.0)))))"),

("mrec3_h.Prelude_Boolx.Minx_def",

"Minx == Abs_Prelude_Boolx (In0 arbitrary)"),

("mrec3_h.Prelude_Boolx.Plusx_def",

"Plusx == Abs_Prelude_Boolx (In1 arbitrary)"),

("mrec3_h.type_definition_Prelude_Natx",

"EX x. x : Prelude_Natx_rep_set

==> type_definition Rep_Prelude_Natx Abs_Prelude_Natx

Prelude_Natx_rep_set"),

("mrec3_h.type_definition_Prelude_Boolx",

"EX x. x : Prelude_Boolx_rep_set

==> type_definition Rep_Prelude_Boolx Abs_Prelude_Boolx

Prelude_Boolx_rep_set"),

("mrec3_h.Prelude_Natx.Prelude_Natx_rec_def",

"Prelude_Natx_rec ?f1.0 ?f2.0 ?f3.0 ==

%x. THE y. (x, y) : Prelude_Natx_rec_set ?f1.0 ?f2.0 ?f3.0"),

("mrec3_h.Prelude_Natx.Prelude_Natx_case_def",

"Prelude_Natx_case ?f1.0 ?f2.0 ?f3.0 ==

Prelude_Natx_rec ?f1.0 ?f2.0 (%x1 x2 x3. ?f3.0 x1 x2)"),

("mrec3_h.Prelude_Natx.Prelude_Natx_size_def",

"size == Prelude_Natx_rec 0 (%x. 0) (%x xa xb. xb + Suc 0)"),

("mrec3_h.Prelude_Boolx.Prelude_Boolx_rec_def",

"Prelude_Boolx_rec ?f1.0 ?f2.0 ==

%x. THE y. (x, y) : Prelude_Boolx_rec_set ?f1.0 ?f2.0"),

("mrec3_h.Prelude_Boolx.Prelude_Boolx_case_def",

"Prelude_Boolx_case ?f1.0 ?f2.0 == Prelude_Boolx_rec ?f1.0 ?f2.0"),

("mrec3_h.Prelude_Boolx.Prelude_Boolx_size_def",

"size == Prelude_Boolx_rec 0 0"),

("mrec3_h.Prelude_Natx.Prelude_Natx_rec_set.defs_1",

"Prelude_Natx_rec_set ?f1.0 ?f2.0 ?f3.0 ==

lfp

(%S.

{x.

x = (Zx, ?f1.0) |

(EX x1. x = (Sx x1, ?f2.0 x1)) |

(EX x1 x2 y1.

x = (SSx x2 x1, ?f3.0 x2 x1 y1) & (x2, y1) : S)})"),

("mrec3_h.Prelude_Natx.Prelude_Natx_rep_set.defs_1",

"Prelude_Natx_rep_set ==

lfp

(%S.

{x.

x = In0 arbitrary |

(EX x1.

x = In1 (In0 (??.Datatype_Universe.Leaf (Inr x1)))) |

(EX x1 x2.

x =

In1

(In1

(Scons x2 (??.Datatype_Universe.Leaf (Inl x1)))) &

x2 : S)})"),

("mrec3_h.Prelude_Boolx.Prelude_Boolx_rec_set.defs_1",

"Prelude_Boolx_rec_set ?f1.0 ?f2.0 ==

lfp (%S. {x. x = (Minx, ?f1.0) | x = (Plusx, ?f2.0)})"),

("mrec3_h.Prelude_Boolx.Prelude_Boolx_rep_set.defs_1",

"Prelude_Boolx_rep_set ==

lfp (%S. {x. x = In0 arbitrary | x = In1 arbitrary})"),

("mrec3_h.map1_Xmap2_X.map1_Xmap2_X_Prelude_Natx_def",

"map1_Xmap2_X ==

Prelude_Natx_rec (%f. Sx (f 0), %w f. Zx)

(%pX1. (%f. Sx (f pX1), %w f. Sx (pX1 + 1)))

(%pX1 pX2 pX1a.

(snd pX1a pX2,

%w f. if pX2 = Minx then SSx pX1 w else fst pX1a f))")]

: (string * Thm.thm) list

Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)

Copyright (c) 2002-5 CUTS and contributors.

Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)

Mapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOL

Mapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOL" (required by "mrec_h")

Loading theory "mrec_h"

structure Header :

sig val initialize : string list -> unit val record : string -> unit end

val it = () : unit

Proofs for datatype(s) "Prelude_Natx"

Constructing representing sets ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the induction rule ...

Proving isomorphism properties ...

Proving freeness of constructors ...

Proving induction rule for datatypes ...

Proving case distinction theorems ...

Constructing primrec combinators ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the elimination rules ...

Proving termination and uniqueness of primrec functions ...

Proving characteristic theorems for primrec combinators ...

Proving characteristic theorems for case combinators ...

Proving equations for case splitting ...

Proving additional theorems for TFL ...

Proving equations for size function ...

Proving equations for primrec function(s) "mrec_h.fun1_Xfun2_X" ...

val it = () : unit

val it = () : unit

val it =

{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,

Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,

Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,

Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,

Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,

Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,

Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,

Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,

Main, HsHOL, mrec_h} : Theory.theory

val it =

[("mrec_h.fun1_def", "fun1 == %x. fst (fun1_Xfun2_X x)"),

("mrec_h.fun2_def", "fun2 == %x. snd (fun1_Xfun2_X x)"),

("mrec_h.Prelude_Natx.Sx_def",

"Sx ?x2.0 ?x1.0 ==

Abs_Prelude_Natx

(In1

(Scons (??.Datatype_Universe.Leaf ?x2.0)

(Rep_Prelude_Natx ?x1.0)))"),

("mrec_h.Prelude_Natx.Zx_def",

"Zx == Abs_Prelude_Natx (In0 arbitrary)"),

("mrec_h.type_definition_Prelude_Natx",

"EX x. x : Prelude_Natx_rep_set

==> type_definition Rep_Prelude_Natx Abs_Prelude_Natx

Prelude_Natx_rep_set"),

("mrec_h.Prelude_Natx.Prelude_Natx_rec_def",

"Prelude_Natx_rec ?f1.0 ?f2.0 ==

%x. THE y. (x, y) : Prelude_Natx_rec_set ?f1.0 ?f2.0"),

("mrec_h.Prelude_Natx.Prelude_Natx_case_def",

"Prelude_Natx_case ?f1.0 ?f2.0 ==

Prelude_Natx_rec ?f1.0 (%x1 x2 x3. ?f2.0 x1 x2)"),

("mrec_h.Prelude_Natx.Prelude_Natx_size_def",

"size == Prelude_Natx_rec 0 (%x xa xb. xb + Suc 0)"),

("mrec_h.Prelude_Natx.Prelude_Natx_rec_set.defs_1",

"Prelude_Natx_rec_set ?f1.0 ?f2.0 ==

lfp

(%S.

{x.

x = (Zx, ?f1.0) |

(EX x1 x2 y1.

x = (Sx x2 x1, ?f2.0 x2 x1 y1) & (x1, y1) : S)})"),

("mrec_h.Prelude_Natx.Prelude_Natx_rep_set.defs_1",

"Prelude_Natx_rep_set ==

lfp

(%S.

{x.

x = In0 arbitrary |

(EX x1 x2.

x = In1 (Scons (??.Datatype_Universe.Leaf x2) x1) &

x1 : S)})"),

("mrec_h.fun1_Xfun2_X.fun1_Xfun2_X_Prelude_Natx_def",

"fun1_Xfun2_X ==

Prelude_Natx_rec ((Zx, 0), 0)

(%pX1 pX2 pX2a.

((Sx pX1 (fst (fst pX2a)), pX1 * snd pX2a),

snd (fst pX2a) + pX1))")] : (string * Thm.thm) list

Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)

Copyright (c) 2002-5 CUTS and contributors.

Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)

Mapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOL

Mapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOL" (required by "wcard_h")

Loading theory "wcard_h"

structure Header :

sig val initialize : string list -> unit val record : string -> unit end

val it = () : unit

Proofs for datatype(s) "Prelude_Boolx"

Constructing representing sets ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the induction rule ...

Proving isomorphism properties ...

Proving freeness of constructors ...

Proving induction rule for datatypes ...

Proving case distinction theorems ...

Constructing primrec combinators ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the elimination rules ...

Proving termination and uniqueness of primrec functions ...

Proving characteristic theorems for primrec combinators ...

Proving characteristic theorems for case combinators ...

Proving equations for case splitting ...

Proving additional theorems for TFL ...

Proving equations for size function ...

Proofs for datatype(s) "Prelude_Natx"

Constructing representing sets ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the induction rule ...

Proving isomorphism properties ...

Proving freeness of constructors ...

Proving induction rule for datatypes ...

Proving case distinction theorems ...

Constructing primrec combinators ...

Proving monotonicity ...

Proving the introduction rules ...

Proving the elimination rules ...

Proving termination and uniqueness of primrec functions ...

Proving characteristic theorems for primrec combinators ...

Proving characteristic theorems for case combinators ...

Proving equations for case splitting ...

Proving additional theorems for TFL ...

Proving equations for size function ...

val it = () : unit

val it = () : unit

val it =

{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,

Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,

Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,

Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,

Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,

Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,

Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,

Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,

Main, HsHOL, wcard_h} : Theory.theory

val it =

[("wcard_h.map1_def",

"map1 ==

%x f.

case x of Zx => Sx (f 0) | Sx pX1 => Sx (f pX1)

| SSx pX2 pX1 => x"),

("wcard_h.Prelude_Natx.Sx_def",

"Sx ?x1.0 ==

Abs_Prelude_Natx

(In1 (In0 (??.Datatype_Universe.Leaf (Inr ?x1.0))))"),

("wcard_h.Prelude_Natx.Zx_def",

"Zx == Abs_Prelude_Natx (In0 arbitrary)"),

("wcard_h.Prelude_Natx.SSx_def",

"SSx ?x2.0 ?x1.0 ==

Abs_Prelude_Natx

(In1

(In1

(Scons (Rep_Prelude_Natx ?x2.0)

(??.Datatype_Universe.Leaf (Inl ?x1.0)))))"),

("wcard_h.Prelude_Boolx.Minx_def",

"Minx == Abs_Prelude_Boolx (In0 arbitrary)"),

("wcard_h.Prelude_Boolx.Plusx_def",

"Plusx == Abs_Prelude_Boolx (In1 arbitrary)"),

("wcard_h.type_definition_Prelude_Natx",

"EX x. x : Prelude_Natx_rep_set

==> type_definition Rep_Prelude_Natx Abs_Prelude_Natx

Prelude_Natx_rep_set"),

("wcard_h.type_definition_Prelude_Boolx",

"EX x. x : Prelude_Boolx_rep_set

==> type_definition Rep_Prelude_Boolx Abs_Prelude_Boolx

Prelude_Boolx_rep_set"),

("wcard_h.Prelude_Natx.Prelude_Natx_rec_def",

"Prelude_Natx_rec ?f1.0 ?f2.0 ?f3.0 ==

%x. THE y. (x, y) : Prelude_Natx_rec_set ?f1.0 ?f2.0 ?f3.0"),

("wcard_h.Prelude_Natx.Prelude_Natx_case_def",

"Prelude_Natx_case ?f1.0 ?f2.0 ?f3.0 ==

Prelude_Natx_rec ?f1.0 ?f2.0 (%x1 x2 x3. ?f3.0 x1 x2)"),

("wcard_h.Prelude_Natx.Prelude_Natx_size_def",

"size == Prelude_Natx_rec 0 (%x. 0) (%x xa xb. xb + Suc 0)"),

("wcard_h.Prelude_Boolx.Prelude_Boolx_rec_def",

"Prelude_Boolx_rec ?f1.0 ?f2.0 ==

%x. THE y. (x, y) : Prelude_Boolx_rec_set ?f1.0 ?f2.0"),

("wcard_h.Prelude_Boolx.Prelude_Boolx_case_def",

"Prelude_Boolx_case ?f1.0 ?f2.0 == Prelude_Boolx_rec ?f1.0 ?f2.0"),

("wcard_h.Prelude_Boolx.Prelude_Boolx_size_def",

"size == Prelude_Boolx_rec 0 0"),

("wcard_h.Prelude_Natx.Prelude_Natx_rec_set.defs_1",

"Prelude_Natx_rec_set ?f1.0 ?f2.0 ?f3.0 ==

lfp

(%S.

{x.

x = (Zx, ?f1.0) |

(EX x1. x = (Sx x1, ?f2.0 x1)) |

(EX x1 x2 y1.

x = (SSx x2 x1, ?f3.0 x2 x1 y1) & (x2, y1) : S)})"),

("wcard_h.Prelude_Natx.Prelude_Natx_rep_set.defs_1",

"Prelude_Natx_rep_set ==

lfp

(%S.

{x.

x = In0 arbitrary |

(EX x1.

x = In1 (In0 (??.Datatype_Universe.Leaf (Inr x1)))) |

(EX x1 x2.

x =

In1

(In1

(Scons x2 (??.Datatype_Universe.Leaf (Inl x1)))) &

x2 : S)})"),

("wcard_h.Prelude_Boolx.Prelude_Boolx_rec_set.defs_1",

"Prelude_Boolx_rec_set ?f1.0 ?f2.0 ==

lfp (%S. {x. x = (Minx, ?f1.0) | x = (Plusx, ?f2.0)})"),

("wcard_h.Prelude_Boolx.Prelude_Boolx_rep_set.defs_1",

"Prelude_Boolx_rep_set ==

lfp (%S. {x. x = In0 arbitrary | x = In1 arbitrary})")]

: (string * Thm.thm) list