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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "ex_class_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "ex_class_hc"

structure Header :

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

val it = () : unit

Proving isomorphism properties of domain ex_class_hc.Prelude_MPList ...

Proving induction properties of domain ex_class_hc.Prelude_MPList ...

Proving isomorphism properties of domain ex_class_hc.Prelude_Color ...

Proving induction properties of domain ex_class_hc.Prelude_Color ...

Proving isomorphism properties of domain ex_class_hc.Prelude_MyList ...

Proving induction properties of domain ex_class_hc.Prelude_MyList ...

### Specification of constant ex_class_hc.methodOne ::

### "'a Prelude_Color -> 'a Prelude_Color -> tr"

### is strictly less general than the declared type

### Specification of constant ex_class_hc.methodTwo ::

### "'a Prelude_Color -> tr -> 'a Prelude_Color Prelude_Color"

### is strictly less general than the declared type

### Specification of constant ex_class_hc.methodOne ::

### "'a Prelude_MyList -> 'a Prelude_MyList -> tr"

### is strictly less general than the declared type

### Specification of constant ex_class_hc.methodTwo ::

### "'a Prelude_MyList -> tr -> 'a Prelude_MyList Prelude_Color"

### is strictly less general than the declared type

### Specification of constant ex_class_hc.methodOne ::

### "('a, 'b) Prelude_MPList -> ('a, 'b) Prelude_MPList -> tr"

### is strictly less general than the declared type

### Specification of constant ex_class_hc.methodTwo ::

### "('a, 'b) Prelude_MPList -> tr -> ('a, 'b) Prelude_MPList Prelude_Color"

### is strictly less general than the declared type

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

ex_class_hc} : Theory.theory

val it =

[("ex_class_hc.myEqual_def",

"myEqual ==

LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi"),

("ex_class_hc.Joker_class.intro",

"OFCLASS(?'a, pcpo_class) ==> OFCLASS(?'a, Joker_class)"),

("ex_class_hc.Prelude_Color.reach", "fix$Prelude_Color_copy$?x = ?x"),

("ex_class_hc.Prelude_MPList.reach",

"fix$Prelude_MPList_copy$?x = ?x"),

("ex_class_hc.Prelude_MyList.reach",

"fix$Prelude_MyList_copy$?x = ?x"),

("ex_class_hc.Prelude_Color.Red_def",

"Red == LAM a. Prelude_Color_abs$(sinl$a)"),

("ex_class_hc.Prelude_Color.abs_iso",

"Prelude_Color_rep$(Prelude_Color_abs$?x) = ?x"),

("ex_class_hc.Prelude_Color.rep_iso",

"Prelude_Color_abs$(Prelude_Color_rep$?x) = ?x"),

("ex_class_hc.Prelude_Color.Blue_def",

"Blue == LAM a. Prelude_Color_abs$(sinr$a)"),

("ex_class_hc.Prelude_Color.copy_def",

"Prelude_Color_copy ==

LAM f.

Prelude_Color_abs oo

Prelude_Color_when$(LAM a. sinl$a)$(LAM a. sinr$a)"),

("ex_class_hc.Prelude_Color.take_def",

"Prelude_Color_take == %n. iterate n Prelude_Color_copy UU"),

("ex_class_hc.Prelude_Color.when_def",

"Prelude_Color_when ==

LAM f1 f2 x. sscase$f1$f2$(Prelude_Color_rep$x)"),

("ex_class_hc.Prelude_MPList.abs_iso",

"Prelude_MPList_rep$(Prelude_MPList_abs$?x) = ?x"),

("ex_class_hc.Prelude_MPList.rep_iso",

"Prelude_MPList_abs$(Prelude_MPList_rep$?x) = ?x"),

("ex_class_hc.Prelude_MyList.abs_iso",

"Prelude_MyList_rep$(Prelude_MyList_abs$?x) = ?x"),

("ex_class_hc.Prelude_MyList.rep_iso",

"Prelude_MyList_abs$(Prelude_MyList_rep$?x) = ?x"),

("ex_class_hc.Prelude_Color.Red_1_def",

"Red_1 == Prelude_Color_when$(LAM a. a)$UU"),

("ex_class_hc.Prelude_Color.bisim_def",

"Prelude_Color_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

(EX a. a ~= UU & x = Red$a & x' = Red$a) |

(EX a. a ~= UU & x = Blue$a & x' = Blue$a)"),

("ex_class_hc.Prelude_MPList.copy_def",

"Prelude_MPList_copy ==

LAM f.

Prelude_MPList_abs oo

Prelude_MPList_when$(sinl$ONE)$(LAM a b P'.

sinr$(:a, b, f$P':))"),

("ex_class_hc.Prelude_MPList.take_def",

"Prelude_MPList_take == %n. iterate n Prelude_MPList_copy UU"),

("ex_class_hc.Prelude_MPList.when_def",

"Prelude_MPList_when ==

LAM f1 f2 x.

sscase$(LAM dummy.

f1)$(ssplit$(LAM a.

ssplit$(f2$a)))$(Prelude_MPList_rep$x)"),

("ex_class_hc.Prelude_MyList.copy_def",

"Prelude_MyList_copy ==

LAM f.

Prelude_MyList_abs oo

Prelude_MyList_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),

("ex_class_hc.Prelude_MyList.take_def",

"Prelude_MyList_take == %n. iterate n Prelude_MyList_copy UU"),

("ex_class_hc.Prelude_MyList.when_def",

"Prelude_MyList_when ==

LAM f1 f2 x.

sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_MyList_rep$x)"),

("ex_class_hc.Prelude_Color.Blue_1_def",

"Blue_1 == Prelude_Color_when$UU$(LAM a. a)"),

("ex_class_hc.Prelude_Color.finite_def",

"Prelude_Color_finite == %x. EX n. Prelude_Color_take n$x = x"),

("ex_class_hc.Prelude_Color.is_Red_def",

"is_Red == Prelude_Color_when$(LAM a. TT)$(LAM a. FF)"),

("ex_class_hc.Prelude_MPList.MPNil_def",

"MPNil == Prelude_MPList_abs$(sinl$ONE)"),

("ex_class_hc.Prelude_MPList.bisim_def",

"Prelude_MPList_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = MPNil & x' = MPNil |

(EX a b P' P''.

a ~= UU &

b ~= UU &

P' ~= UU &

P'' ~= UU &

R P' P'' & x = MPCons$a$b$P' & x' = MPCons$a$b$P'')"),

("ex_class_hc.Prelude_MyList.MyNil_def",

"MyNil == Prelude_MyList_abs$(sinl$ONE)"),

("ex_class_hc.Prelude_MyList.bisim_def",

"Prelude_MyList_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = MyNil & x' = MyNil |

(EX a P' P''.

a ~= UU &

P' ~= UU &

P'' ~= UU &

R P' P'' & x = MyCons$a$P' & x' = MyCons$a$P'')"),

("ex_class_hc.Prelude_Color.is_Blue_def",

"is_Blue == Prelude_Color_when$(LAM a. FF)$(LAM a. TT)"),

("ex_class_hc.Prelude_MPList.MPCons_def",

"MPCons == LAM a b P'. Prelude_MPList_abs$(sinr$(:a, b, P':))"),

("ex_class_hc.Prelude_MPList.finite_def",

"Prelude_MPList_finite == %x. EX n. Prelude_MPList_take n$x = x"),

("ex_class_hc.Prelude_MyList.MyCons_def",

"MyCons == LAM a P'. Prelude_MyList_abs$(sinr$(:a, P':))"),

("ex_class_hc.Prelude_MyList.finite_def",

"Prelude_MyList_finite == %x. EX n. Prelude_MyList_take n$x = x"),

("ex_class_hc.Prelude_Color.match_Red_def",

"match_Red == Prelude_Color_when$(LAM a. return$a)$(LAM a. fail)"),

("ex_class_hc.Prelude_Color_methodOne_def", "methodOne == myEqual"),

("ex_class_hc.Prelude_Color_methodTwo_def",

"methodTwo == default__methodTwo"),

("ex_class_hc.Prelude_MPList.MPCons_1_def",

"MPCons_1 == Prelude_MPList_when$UU$(LAM a b P'. a)"),

("ex_class_hc.Prelude_MPList.MPCons_2_def",

"MPCons_2 == Prelude_MPList_when$UU$(LAM a b P'. b)"),

("ex_class_hc.Prelude_MPList.MPCons_3_def",

"MPCons_3 == Prelude_MPList_when$UU$(LAM a b P'. P')"),

("ex_class_hc.Prelude_MPList.is_MPNil_def",

"is_MPNil == Prelude_MPList_when$TT$(LAM a b P'. FF)"),

("ex_class_hc.Prelude_MyList.MyCons_1_def",

"MyCons_1 == Prelude_MyList_when$UU$(LAM a P'. a)"),

("ex_class_hc.Prelude_MyList.MyCons_2_def",

"MyCons_2 == Prelude_MyList_when$UU$(LAM a P'. P')"),

("ex_class_hc.Prelude_MyList.is_MyNil_def",

"is_MyNil == Prelude_MyList_when$TT$(LAM a P'. FF)"),

("ex_class_hc.Prelude_Color.match_Blue_def",

"match_Blue == Prelude_Color_when$(LAM a. fail)$(LAM a. return$a)"),

("ex_class_hc.Prelude_MPList.is_MPCons_def",

"is_MPCons == Prelude_MPList_when$FF$(LAM a b P'. TT)"),

("ex_class_hc.Prelude_MPList_methodOne_def",

"methodOne == default__methodOne"),

("ex_class_hc.Prelude_MPList_methodTwo_def",

"methodTwo == default__methodTwo"),

("ex_class_hc.Prelude_MyList.is_MyCons_def",

"is_MyCons == Prelude_MyList_when$FF$(LAM a P'. TT)"),

("ex_class_hc.Prelude_MyList_methodOne_def", "methodOne == myEqual"),

("ex_class_hc.Prelude_MyList_methodTwo_def",

"methodTwo ==

LAM x y.

If (LAM x y. Def (x = y))$y$TT then Red$x else Blue$x fi"),

("ex_class_hc.Prelude_MPList.match_MPNil_def",

"match_MPNil ==

Prelude_MPList_when$(return$())$(LAM a b P'. fail)"),

("ex_class_hc.Prelude_MyList.match_MyNil_def",

"match_MyNil == Prelude_MyList_when$(return$())$(LAM a P'. fail)"),

("ex_class_hc.Prelude_MPList.match_MPCons_def",

"match_MPCons ==

Prelude_MPList_when$fail$(LAM a b P'. return$<a, b, P'>)"),

("ex_class_hc.Prelude_MyList.match_MyCons_def",

"match_MyCons ==

Prelude_MyList_when$fail$(LAM a P'. return$<a, P'>)")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "ex_fibon_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "ex_fibon_hc"

structure Header :

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

val it = () : unit

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

ex_fibon_hc} : Theory.theory

val it =

[("ex_fibon_hc.fibon_def",

"fibon ==

FIX fibon.

run$(return$(LAM n.

If (LAM x y. Def (x = y))$n$(Def 0)

then Def 1

else If (LAM x y. Def (x = y))$n$(Def 1)

then Def 1

else fliftbin

op +$(fibon$(fliftbin

op -$n$(Def

1)))$(fibon$(fliftbin

op -$n$(Def 2))) fi fi))")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "ex_let_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "ex_let_hc"

structure Header :

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

val it = () : unit

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

ex_let_hc} : Theory.theory

val it =

[("ex_let_hc.foon_def",

"foon ==

LAM a b c.

let testName1 >>= myEqual$a$b

in Let (myEqual$b$c) (Rep_CFun (trand$testName1))"),

("ex_let_hc.myEqual_def",

"myEqual ==

LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "ex_list_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "ex_list_hc"

structure Header :

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

val it = () : unit

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

ex_list_hc} : Theory.theory

val it =

[("ex_list_hc.myMap_def",

"myMap ==

FIX myMap.

run$(return$(LAM x f.

case x of lNil => lNil

| lCons$pX1$pX2 => lCons$(f$pX1)$(myMap$pX2$f)))"),

("ex_list_hc.funOne_def",

"funOne ==

LAM x y.

If (LAM x y. Def (x = y))$x$(lCons$(lHd$x)$(lTl$y))

then TT else FF fi")] : (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "ex_mutrec_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "ex_mutrec_hc"

structure Header :

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

val it = () : unit

Proving isomorphism properties of domain ex_mutrec_hc.Prelude_MyList ...

Proving induction properties of domain ex_mutrec_hc.Prelude_MyList ...

Proving isomorphism properties of domain ex_mutrec_hc.Prelude_Form ...

Proving induction properties of domain ex_mutrec_hc.Prelude_Form ...

Proving isomorphism properties of domain ex_mutrec_hc.Prelude_CList ...

Proving isomorphism properties of domain ex_mutrec_hc.Prelude_LColor ...

Proving induction properties of domain ex_mutrec_hc.Prelude_CList_Prelude_LColor ...

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

ex_mutrec_hc} : Theory.theory

val it =

[("ex_mutrec_hc.fibon_def",

"fibon ==

FIX fibon.

run$(return$(LAM n.

If (LAM x y. Def (x = y))$n$(Def 0)

then Def 1

else If (LAM x y. Def (x = y))$n$(Def 1)

then Def 1

else fliftbin

op +$(fibon$(fliftbin

op -$n$(Def

1)))$(fibon$(fliftbin

op -$n$(Def 2))) fi fi))"),

("ex_mutrec_hc.myEqual_def",

"myEqual ==

LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi"),

("ex_mutrec_hc.hasColor_def",

"hasColor ==

LAM x y.

If myEqual$x$y

then Red$((LAM z. Square$x$z)$x)

else Blue$(Rectangle$x$y) fi"),

("ex_mutrec_hc.mRecFun1_def",

"mRecFun1 ==

cfst$(FIX <mRecFun1, mRecFun2>.

<run$(return$(LAM n.

If (LAM x y. Def (x = y))$n$(Def 0)

then Def 0

else If (LAM x y. Def (x = y))$n$(Def 1)

then Def 2

else fliftbin

op +$(mRecFun1$(fliftbin

op -$n$(Def

1)))$(mRecFun2$(fliftbin

op -$n$(Def 2))) fi fi)),

run$(return$(LAM n.

If (LAM x y. Def (x = y))$n$(Def 0)

then Def 0

else If (LAM x y. Def (x = y))$n$(Def 1)

then Def 0

else fliftbin

op +$(mRecFun1$(fliftbin

op -$n$(Def

1)))$(mRecFun2$(fliftbin

op -$n$(Def 1))) fi fi))>)"),

("ex_mutrec_hc.mRecFun2_def",

"mRecFun2 ==

csnd$(FIX <mRecFun1, mRecFun2>.

<run$(return$(LAM n.

If (LAM x y. Def (x = y))$n$(Def 0)

then Def 0

else If (LAM x y. Def (x = y))$n$(Def 1)

then Def 2

else fliftbin

op +$(mRecFun1$(fliftbin

op -$n$(Def

1)))$(mRecFun2$(fliftbin

op -$n$(Def 2))) fi fi)),

run$(return$(LAM n.

If (LAM x y. Def (x = y))$n$(Def 0)

then Def 0

else If (LAM x y. Def (x = y))$n$(Def 1)

then Def 0

else fliftbin

op +$(mRecFun1$(fliftbin

op -$n$(Def

1)))$(mRecFun2$(fliftbin

op -$n$(Def 1))) fi fi))>)"),

("ex_mutrec_hc.Prelude_Form.reach", "fix$Prelude_Form_copy$?x = ?x"),

("ex_mutrec_hc.Prelude_CList.reach",

"cfst$(fix$Prelude_CList_Prelude_LColor_copy)$?x1.0 = ?x1.0"),

("ex_mutrec_hc.Prelude_Form.abs_iso",

"Prelude_Form_rep$(Prelude_Form_abs$?x) = ?x"),

("ex_mutrec_hc.Prelude_Form.rep_iso",

"Prelude_Form_abs$(Prelude_Form_rep$?x) = ?x"),

("ex_mutrec_hc.Prelude_LColor.reach",

"csnd$(fix$Prelude_CList_Prelude_LColor_copy)$?x2.0 = ?x2.0"),

("ex_mutrec_hc.Prelude_MyList.reach",

"fix$Prelude_MyList_copy$?x = ?x"),

("ex_mutrec_hc.Prelude_CList.abs_iso",

"Prelude_CList_rep$(Prelude_CList_abs$?x) = ?x"),

("ex_mutrec_hc.Prelude_CList.rep_iso",

"Prelude_CList_abs$(Prelude_CList_rep$?x) = ?x"),

("ex_mutrec_hc.Prelude_Form.copy_def",

"Prelude_Form_copy ==

LAM f.

Prelude_Form_abs oo

Prelude_Form_when$(LAM a b.

sinl$(:a, b:))$(LAM a b. sinr$(:a, b:))"),

("ex_mutrec_hc.Prelude_Form.take_def",

"Prelude_Form_take == %n. iterate n Prelude_Form_copy UU"),

("ex_mutrec_hc.Prelude_Form.when_def",

"Prelude_Form_when ==

LAM f1 f2 x.

sscase$(ssplit$f1)$(ssplit$f2)$(Prelude_Form_rep$x)"),

("ex_mutrec_hc.Prelude_CList.copy_def",

"Prelude_CList_copy ==

LAM f.

Prelude_CList_abs oo

Prelude_CList_when$(sinl$ONE)$(LAM P'1 P'2.

sinr$(:P'1, cfst$f$P'2:))"),

("ex_mutrec_hc.Prelude_CList.take_def",

"Prelude_CList_take ==

%n. cfst$(iterate n Prelude_CList_Prelude_LColor_copy UU)"),

("ex_mutrec_hc.Prelude_CList.when_def",

"Prelude_CList_when ==

LAM f1 f2 x.

sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_CList_rep$x)"),

("ex_mutrec_hc.Prelude_Form.bisim_def",

"Prelude_Form_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

(EX a b.

a ~= UU & b ~= UU & x = Square$a$b & x' = Square$a$b) |

(EX a b.

a ~= UU &

b ~= UU & x = Rectangle$a$b & x' = Rectangle$a$b)"),

("ex_mutrec_hc.Prelude_LColor.Red_def",

"Red == LAM a. Prelude_LColor_abs$(sinr$(sinl$a))"),

("ex_mutrec_hc.Prelude_LColor.abs_iso",

"Prelude_LColor_rep$(Prelude_LColor_abs$?x) = ?x"),

("ex_mutrec_hc.Prelude_LColor.rep_iso",

"Prelude_LColor_abs$(Prelude_LColor_rep$?x) = ?x"),

("ex_mutrec_hc.Prelude_MyList.abs_iso",

"Prelude_MyList_rep$(Prelude_MyList_abs$?x) = ?x"),

("ex_mutrec_hc.Prelude_MyList.rep_iso",

"Prelude_MyList_abs$(Prelude_MyList_rep$?x) = ?x"),

("ex_mutrec_hc.Prelude_CList.CCons_def",

"CCons == LAM P'1 P'2. Prelude_CList_abs$(sinr$(:P'1, P'2:))"),

("ex_mutrec_hc.Prelude_CList.Trans_def",

"Trans == Prelude_CList_abs$(sinl$ONE)"),

("ex_mutrec_hc.Prelude_Form.Square_def",

"Square == LAM a b. Prelude_Form_abs$(sinl$(:a, b:))"),

("ex_mutrec_hc.Prelude_Form.finite_def",

"Prelude_Form_finite == %x. EX n. Prelude_Form_take n$x = x"),

("ex_mutrec_hc.Prelude_LColor.Blue_def",

"Blue == LAM a. Prelude_LColor_abs$(sinl$a)"),

("ex_mutrec_hc.Prelude_LColor.copy_def",

"Prelude_LColor_copy ==

LAM f.

Prelude_LColor_abs oo

Prelude_LColor_when$(LAM a.

sinl$a)$(LAM a. sinr$(sinl$a))$(LAM P'. sinr$(sinr$P'))"),

("ex_mutrec_hc.Prelude_LColor.take_def",

"Prelude_LColor_take ==

%n. csnd$(iterate n Prelude_CList_Prelude_LColor_copy UU)"),

("ex_mutrec_hc.Prelude_LColor.when_def",

"Prelude_LColor_when ==

LAM f1 f2 f3 x.

sscase$f1$(sscase$f2$f3)$(Prelude_LColor_rep$x)"),

("ex_mutrec_hc.Prelude_MyList.copy_def",

"Prelude_MyList_copy ==

LAM f.

Prelude_MyList_abs oo

Prelude_MyList_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),

("ex_mutrec_hc.Prelude_MyList.take_def",

"Prelude_MyList_take == %n. iterate n Prelude_MyList_copy UU"),

("ex_mutrec_hc.Prelude_MyList.when_def",

"Prelude_MyList_when ==

LAM f1 f2 x.

sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_MyList_rep$x)"),

("ex_mutrec_hc.Prelude_CList.finite_def",

"Prelude_CList_finite == %x1. EX n. Prelude_CList_take n$x1 = x1"),

("ex_mutrec_hc.Prelude_LColor.Multi_def",

"Multi == LAM P'. Prelude_LColor_abs$(sinr$(sinr$P'))"),

("ex_mutrec_hc.Prelude_LColor.Red_1_def",

"Red_1 == Prelude_LColor_when$UU$(LAM a. a)$UU"),

("ex_mutrec_hc.Prelude_MyList.MyNil_def",

"MyNil == Prelude_MyList_abs$(sinl$ONE)"),

("ex_mutrec_hc.Prelude_MyList.bisim_def",

"Prelude_MyList_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = MyNil & x' = MyNil |

(EX a P' P''.

a ~= UU &

P' ~= UU &

P'' ~= UU &

R P' P'' & x = MyCons$a$P' & x' = MyCons$a$P'')"),

("ex_mutrec_hc.Prelude_CList.CCons_1_def",

"CCons_1 == Prelude_CList_when$UU$(LAM P'1 P'2. P'1)"),

("ex_mutrec_hc.Prelude_CList.CCons_2_def",

"CCons_2 == Prelude_CList_when$UU$(LAM P'1 P'2. P'2)"),

("ex_mutrec_hc.Prelude_Form.Square_1_def",

"Square_1 == Prelude_Form_when$(LAM a b. a)$UU"),

("ex_mutrec_hc.Prelude_Form.Square_2_def",

"Square_2 == Prelude_Form_when$(LAM a b. b)$UU"),

("ex_mutrec_hc.Prelude_LColor.Blue_1_def",

"Blue_1 == Prelude_LColor_when$(LAM a. a)$UU$UU"),

("ex_mutrec_hc.Prelude_LColor.finite_def",

"Prelude_LColor_finite ==

%x2. EX n. Prelude_LColor_take n$x2 = x2"),

("ex_mutrec_hc.Prelude_LColor.is_Red_def",

"is_Red ==

Prelude_LColor_when$(LAM a. FF)$(LAM a. TT)$(LAM P'. FF)"),

("ex_mutrec_hc.Prelude_MyList.MyCons_def",

"MyCons == LAM a P'. Prelude_MyList_abs$(sinr$(:a, P':))"),

("ex_mutrec_hc.Prelude_MyList.finite_def",

"Prelude_MyList_finite == %x. EX n. Prelude_MyList_take n$x = x"),

("ex_mutrec_hc.Prelude_CList.is_CCons_def",

"is_CCons == Prelude_CList_when$FF$(LAM P'1 P'2. TT)"),

("ex_mutrec_hc.Prelude_CList.is_Trans_def",

"is_Trans == Prelude_CList_when$TT$(LAM P'1 P'2. FF)"),

("ex_mutrec_hc.Prelude_Form.Rectangle_def",

"Rectangle == LAM a b. Prelude_Form_abs$(sinr$(:a, b:))"),

("ex_mutrec_hc.Prelude_Form.is_Square_def",

"is_Square == Prelude_Form_when$(LAM a b. TT)$(LAM a b. FF)"),

("ex_mutrec_hc.Prelude_LColor.Multi_1_def",

"Multi_1 == Prelude_LColor_when$UU$UU$(LAM P'. P')"),

("ex_mutrec_hc.Prelude_LColor.is_Blue_def",

"is_Blue ==

Prelude_LColor_when$(LAM a. TT)$(LAM a. FF)$(LAM P'. FF)"),

("ex_mutrec_hc.Prelude_LColor.is_Multi_def",

"is_Multi ==

Prelude_LColor_when$(LAM a. FF)$(LAM a. FF)$(LAM P'. TT)"),

("ex_mutrec_hc.Prelude_MyList.MyCons_1_def",

"MyCons_1 == Prelude_MyList_when$UU$(LAM a P'. a)"),

("ex_mutrec_hc.Prelude_MyList.MyCons_2_def",

"MyCons_2 == Prelude_MyList_when$UU$(LAM a P'. P')"),

("ex_mutrec_hc.Prelude_MyList.is_MyNil_def",

"is_MyNil == Prelude_MyList_when$TT$(LAM a P'. FF)"),

("ex_mutrec_hc.Prelude_Form.Rectangle_1_def",

"Rectangle_1 == Prelude_Form_when$UU$(LAM a b. a)"),

("ex_mutrec_hc.Prelude_Form.Rectangle_2_def",

"Rectangle_2 == Prelude_Form_when$UU$(LAM a b. b)"),

("ex_mutrec_hc.Prelude_LColor.match_Red_def",

"match_Red ==

Prelude_LColor_when$(LAM a.

fail)$(LAM a. return$a)$(LAM P'. fail)"),

("ex_mutrec_hc.Prelude_MyList.is_MyCons_def",

"is_MyCons == Prelude_MyList_when$FF$(LAM a P'. TT)"),

("ex_mutrec_hc.Prelude_CList.match_CCons_def",

"match_CCons ==

Prelude_CList_when$fail$(LAM P'1 P'2. return$<P'1, P'2>)"),

("ex_mutrec_hc.Prelude_CList.match_Trans_def",

"match_Trans ==

Prelude_CList_when$(return$())$(LAM P'1 P'2. fail)"),

("ex_mutrec_hc.Prelude_Form.is_Rectangle_def",

"is_Rectangle == Prelude_Form_when$(LAM a b. FF)$(LAM a b. TT)"),

("ex_mutrec_hc.Prelude_Form.match_Square_def",

"match_Square ==

Prelude_Form_when$(LAM a b. return$<a, b>)$(LAM a b. fail)"),

("ex_mutrec_hc.Prelude_LColor.match_Blue_def",

"match_Blue ==

Prelude_LColor_when$(LAM a.

return$a)$(LAM a. fail)$(LAM P'. fail)"),

("ex_mutrec_hc.Prelude_LColor.match_Multi_def",

"match_Multi ==

Prelude_LColor_when$(LAM a.

fail)$(LAM a. fail)$(LAM P'. return$P')"),

("ex_mutrec_hc.Prelude_MyList.match_MyNil_def",

"match_MyNil == Prelude_MyList_when$(return$())$(LAM a P'. fail)"),

("ex_mutrec_hc.Prelude_MyList.match_MyCons_def",

"match_MyCons ==

Prelude_MyList_when$fail$(LAM a P'. return$<a, P'>)"),

("ex_mutrec_hc.Prelude_Form.match_Rectangle_def",

"match_Rectangle ==

Prelude_Form_when$(LAM a b. fail)$(LAM a b. return$<a, b>)"),

("ex_mutrec_hc.Prelude_CList_Prelude_LColor.copy_def",

"Prelude_CList_Prelude_LColor_copy ==

LAM f. <Prelude_CList_copy$f, Prelude_LColor_copy$f>"),

("ex_mutrec_hc.Prelude_CList_Prelude_LColor.bisim_def",

"Prelude_CList_Prelude_LColor_bisim ==

%R.

(ALL x1 x1'.

fst R x1 x1' -->

x1 = UU & x1' = UU |

x1 = Trans & x1' = Trans |

(EX P'1 P'2 P'2'.

P'1 ~= UU &

P'2 ~= UU &

P'2' ~= UU &

fst R P'2 P'2' &

x1 = CCons$P'1$P'2 & x1' = CCons$P'1$P'2')) &

(ALL x2 x2'.

snd R x2 x2' -->

x2 = UU & x2' = UU |

(EX a. a ~= UU & x2 = Blue$a & x2' = Blue$a) |

(EX a. a ~= UU & x2 = Red$a & x2' = Red$a) |

(EX P'. P' ~= UU & x2 = Multi$P' & x2' = Multi$P'))")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "incmpl_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "incmpl_hc"

structure Header :

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

val it = () : unit

Proving isomorphism properties of domain incmpl_hc.Prelude_Boolx ...

Proving induction properties of domain incmpl_hc.Prelude_Boolx ...

Proving isomorphism properties of domain incmpl_hc.Prelude_Natx ...

Proving induction properties of domain incmpl_hc.Prelude_Natx ...

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

incmpl_hc} : Theory.theory

val it =

[("incmpl_hc.map1_def",

"map1 ==

LAM x f.

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

| SSx$pX2$pX1 => UU"),

("incmpl_hc.Prelude_Natx.reach", "fix$Prelude_Natx_copy$?x = ?x"),

("incmpl_hc.Prelude_Boolx.reach", "fix$Prelude_Boolx_copy$?x = ?x"),

("incmpl_hc.Prelude_Natx.Sx_def",

"Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),

("incmpl_hc.Prelude_Natx.Zx_def", "Zx == Prelude_Natx_abs$(sinl$ONE)"),

("incmpl_hc.Prelude_Natx.SSx_def",

"SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),

("incmpl_hc.Prelude_Natx.abs_iso",

"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),

("incmpl_hc.Prelude_Natx.rep_iso",

"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),

("incmpl_hc.Prelude_Boolx.abs_iso",

"Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),

("incmpl_hc.Prelude_Boolx.rep_iso",

"Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),

("incmpl_hc.Prelude_Natx.Sx_1_def",

"Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),

("incmpl_hc.Prelude_Natx.copy_def",

"Prelude_Natx_copy ==

LAM f.

Prelude_Natx_abs oo

Prelude_Natx_when$(sinl$ONE)$(LAM a.

sinr$(sinl$a))$(LAM P'1 P'2.

sinr$(sinr$(:f$P'1, P'2:)))"),

("incmpl_hc.Prelude_Natx.take_def",

"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),

("incmpl_hc.Prelude_Natx.when_def",

"Prelude_Natx_when ==

LAM f1 f2 f3 x.

sscase$(LAM dummy.

f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),

("incmpl_hc.Prelude_Boolx.Minx_def",

"Minx == Prelude_Boolx_abs$(sinl$ONE)"),

("incmpl_hc.Prelude_Boolx.copy_def",

"Prelude_Boolx_copy ==

LAM f.

Prelude_Boolx_abs oo

Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),

("incmpl_hc.Prelude_Boolx.take_def",

"Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),

("incmpl_hc.Prelude_Boolx.when_def",

"Prelude_Boolx_when ==

LAM f1 f2 x.

case Prelude_Boolx_rep$x of sinl$dummy => f1

| sinr$dummy => f2"),

("incmpl_hc.Prelude_Natx.SSx_1_def",

"SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),

("incmpl_hc.Prelude_Natx.SSx_2_def",

"SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),

("incmpl_hc.Prelude_Natx.bisim_def",

"Prelude_Natx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Zx & x' = Zx |

(EX a. a ~= UU & x = Sx$a & x' = Sx$a) |

(EX P'2 P'1 P'1'.

P'2 ~= UU &

P'1 ~= UU &

P'1' ~= UU &

R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),

("incmpl_hc.Prelude_Natx.is_Sx_def",

"is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),

("incmpl_hc.Prelude_Natx.is_Zx_def",

"is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),

("incmpl_hc.Prelude_Boolx.Plusx_def",

"Plusx == Prelude_Boolx_abs$(sinr$ONE)"),

("incmpl_hc.Prelude_Boolx.bisim_def",

"Prelude_Boolx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Minx & x' = Minx | x = Plusx & x' = Plusx"),

("incmpl_hc.Prelude_Natx.finite_def",

"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),

("incmpl_hc.Prelude_Natx.is_SSx_def",

"is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),

("incmpl_hc.Prelude_Boolx.finite_def",

"Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),

("incmpl_hc.Prelude_Boolx.is_Minx_def",

"is_Minx == Prelude_Boolx_when$TT$FF"),

("incmpl_hc.Prelude_Natx.match_Sx_def",

"match_Sx ==

Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),

("incmpl_hc.Prelude_Natx.match_Zx_def",

"match_Zx ==

Prelude_Natx_when$(return$())$(LAM a.

fail)$(LAM P'1 P'2. fail)"),

("incmpl_hc.Prelude_Boolx.is_Plusx_def",

"is_Plusx == Prelude_Boolx_when$FF$TT"),

("incmpl_hc.Prelude_Natx.match_SSx_def",

"match_SSx ==

Prelude_Natx_when$fail$(LAM a.

fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),

("incmpl_hc.Prelude_Boolx.match_Minx_def",

"match_Minx == Prelude_Boolx_when$(return$())$fail"),

("incmpl_hc.Prelude_Boolx.match_Plusx_def",

"match_Plusx == Prelude_Boolx_when$fail$(return$())")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "mrec3_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "mrec3_hc"

structure Header :

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

val it = () : unit

Proving isomorphism properties of domain mrec3_hc.Prelude_Boolx ...

Proving induction properties of domain mrec3_hc.Prelude_Boolx ...

Proving isomorphism properties of domain mrec3_hc.Prelude_Natx ...

Proving induction properties of domain mrec3_hc.Prelude_Natx ...

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

mrec3_hc} : Theory.theory

val it =

[("mrec3_hc.map1_def",

"map1 ==

cfst$(FIX <map1, map2>.

<run$(return$(LAM x f.

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

| SSx$pX1$pX2 => map2$pX1$pX2$f)),

run$(return$(LAM x w f.

case x of Zx => Zx

| Sx$pX1 => Sx$(fliftbin op +$pX1$(Def 1))

| SSx$pX1$pX2 =>

If (LAM x y. Def (x = y))$pX2$Minx

then SSx$pX1$w else map1$pX1$f fi))>)"),

("mrec3_hc.map2_def",

"map2 ==

csnd$(FIX <map1, map2>.

<run$(return$(LAM x f.

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

| SSx$pX1$pX2 => map2$pX1$pX2$f)),

run$(return$(LAM x w f.

case x of Zx => Zx

| Sx$pX1 => Sx$(fliftbin op +$pX1$(Def 1))

| SSx$pX1$pX2 =>

If (LAM x y. Def (x = y))$pX2$Minx

then SSx$pX1$w else map1$pX1$f fi))>)"),

("mrec3_hc.Prelude_Natx.reach", "fix$Prelude_Natx_copy$?x = ?x"),

("mrec3_hc.Prelude_Boolx.reach", "fix$Prelude_Boolx_copy$?x = ?x"),

("mrec3_hc.Prelude_Natx.Sx_def",

"Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),

("mrec3_hc.Prelude_Natx.Zx_def", "Zx == Prelude_Natx_abs$(sinl$ONE)"),

("mrec3_hc.Prelude_Natx.SSx_def",

"SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),

("mrec3_hc.Prelude_Natx.abs_iso",

"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),

("mrec3_hc.Prelude_Natx.rep_iso",

"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),

("mrec3_hc.Prelude_Boolx.abs_iso",

"Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),

("mrec3_hc.Prelude_Boolx.rep_iso",

"Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),

("mrec3_hc.Prelude_Natx.Sx_1_def",

"Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),

("mrec3_hc.Prelude_Natx.copy_def",

"Prelude_Natx_copy ==

LAM f.

Prelude_Natx_abs oo

Prelude_Natx_when$(sinl$ONE)$(LAM a.

sinr$(sinl$a))$(LAM P'1 P'2.

sinr$(sinr$(:f$P'1, P'2:)))"),

("mrec3_hc.Prelude_Natx.take_def",

"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),

("mrec3_hc.Prelude_Natx.when_def",

"Prelude_Natx_when ==

LAM f1 f2 f3 x.

sscase$(LAM dummy.

f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),

("mrec3_hc.Prelude_Boolx.Minx_def",

"Minx == Prelude_Boolx_abs$(sinl$ONE)"),

("mrec3_hc.Prelude_Boolx.copy_def",

"Prelude_Boolx_copy ==

LAM f.

Prelude_Boolx_abs oo

Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),

("mrec3_hc.Prelude_Boolx.take_def",

"Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),

("mrec3_hc.Prelude_Boolx.when_def",

"Prelude_Boolx_when ==

LAM f1 f2 x.

case Prelude_Boolx_rep$x of sinl$dummy => f1

| sinr$dummy => f2"),

("mrec3_hc.Prelude_Natx.SSx_1_def",

"SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),

("mrec3_hc.Prelude_Natx.SSx_2_def",

"SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),

("mrec3_hc.Prelude_Natx.bisim_def",

"Prelude_Natx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Zx & x' = Zx |

(EX a. a ~= UU & x = Sx$a & x' = Sx$a) |

(EX P'2 P'1 P'1'.

P'2 ~= UU &

P'1 ~= UU &

P'1' ~= UU &

R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),

("mrec3_hc.Prelude_Natx.is_Sx_def",

"is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),

("mrec3_hc.Prelude_Natx.is_Zx_def",

"is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),

("mrec3_hc.Prelude_Boolx.Plusx_def",

"Plusx == Prelude_Boolx_abs$(sinr$ONE)"),

("mrec3_hc.Prelude_Boolx.bisim_def",

"Prelude_Boolx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Minx & x' = Minx | x = Plusx & x' = Plusx"),

("mrec3_hc.Prelude_Natx.finite_def",

"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),

("mrec3_hc.Prelude_Natx.is_SSx_def",

"is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),

("mrec3_hc.Prelude_Boolx.finite_def",

"Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),

("mrec3_hc.Prelude_Boolx.is_Minx_def",

"is_Minx == Prelude_Boolx_when$TT$FF"),

("mrec3_hc.Prelude_Natx.match_Sx_def",

"match_Sx ==

Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),

("mrec3_hc.Prelude_Natx.match_Zx_def",

"match_Zx ==

Prelude_Natx_when$(return$())$(LAM a.

fail)$(LAM P'1 P'2. fail)"),

("mrec3_hc.Prelude_Boolx.is_Plusx_def",

"is_Plusx == Prelude_Boolx_when$FF$TT"),

("mrec3_hc.Prelude_Natx.match_SSx_def",

"match_SSx ==

Prelude_Natx_when$fail$(LAM a.

fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),

("mrec3_hc.Prelude_Boolx.match_Minx_def",

"match_Minx == Prelude_Boolx_when$(return$())$fail"),

("mrec3_hc.Prelude_Boolx.match_Plusx_def",

"match_Plusx == Prelude_Boolx_when$fail$(return$())")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "mrec_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "mrec_hc"

structure Header :

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

val it = () : unit

Proving isomorphism properties of domain mrec_hc.Prelude_Natx ...

Proving induction properties of domain mrec_hc.Prelude_Natx ...

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

mrec_hc} : Theory.theory

val it =

[("mrec_hc.fun1_def",

"fun1 ==

cfst$(FIX <fun1, fun2>.

<run$(return$(LAM x.

case x of Zx => <Zx, Def 0>

| Sx$pX1$pX2 =>

<Sx$pX1$(cfst$(fun1$pX2)),

fliftbin op *$pX1$(fun2$pX2)>)),

run$(return$(LAM x.

case x of Zx => Def 0

| Sx$pX1$pX2 =>

fliftbin op +$(csnd$(fun1$pX2))$pX1))>)"),

("mrec_hc.fun2_def",

"fun2 ==

csnd$(FIX <fun1, fun2>.

<run$(return$(LAM x.

case x of Zx => <Zx, Def 0>

| Sx$pX1$pX2 =>

<Sx$pX1$(cfst$(fun1$pX2)),

fliftbin op *$pX1$(fun2$pX2)>)),

run$(return$(LAM x.

case x of Zx => Def 0

| Sx$pX1$pX2 =>

fliftbin op +$(csnd$(fun1$pX2))$pX1))>)"),

("mrec_hc.Prelude_Natx.reach", "fix$Prelude_Natx_copy$?x = ?x"),

("mrec_hc.Prelude_Natx.Sx_def",

"Sx == LAM a P'. Prelude_Natx_abs$(sinr$(:a, P':))"),

("mrec_hc.Prelude_Natx.Zx_def", "Zx == Prelude_Natx_abs$(sinl$ONE)"),

("mrec_hc.Prelude_Natx.abs_iso",

"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),

("mrec_hc.Prelude_Natx.rep_iso",

"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),

("mrec_hc.Prelude_Natx.Sx_1_def",

"Sx_1 == Prelude_Natx_when$UU$(LAM a P'. a)"),

("mrec_hc.Prelude_Natx.Sx_2_def",

"Sx_2 == Prelude_Natx_when$UU$(LAM a P'. P')"),

("mrec_hc.Prelude_Natx.copy_def",

"Prelude_Natx_copy ==

LAM f.

Prelude_Natx_abs oo

Prelude_Natx_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),

("mrec_hc.Prelude_Natx.take_def",

"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),

("mrec_hc.Prelude_Natx.when_def",

"Prelude_Natx_when ==

LAM f1 f2 x.

sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_Natx_rep$x)"),

("mrec_hc.Prelude_Natx.bisim_def",

"Prelude_Natx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Zx & x' = Zx |

(EX a P' P''.

a ~= UU &

P' ~= UU &

P'' ~= UU & R P' P'' & x = Sx$a$P' & x' = Sx$a$P'')"),

("mrec_hc.Prelude_Natx.is_Sx_def",

"is_Sx == Prelude_Natx_when$FF$(LAM a P'. TT)"),

("mrec_hc.Prelude_Natx.is_Zx_def",

"is_Zx == Prelude_Natx_when$TT$(LAM a P'. FF)"),

("mrec_hc.Prelude_Natx.finite_def",

"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),

("mrec_hc.Prelude_Natx.match_Sx_def",

"match_Sx == Prelude_Natx_when$fail$(LAM a P'. return$<a, P'>)"),

("mrec_hc.Prelude_Natx.match_Zx_def",

"match_Zx == Prelude_Natx_when$(return$())$(LAM a P'. fail)")]

: (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/HOLCF

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

Poly/ML 4.2.0 Release

> val it = () : unit

Loading theory "HsHOLCF" (required by "wcard_hc")

constants

fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"

Proving isomorphism properties of domain HsHOLCF.llist ...

Proving induction properties of domain HsHOLCF.llist ...

Loading theory "wcard_hc"

structure Header :

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

val it = () : unit

Proving isomorphism properties of domain wcard_hc.Prelude_Boolx ...

Proving induction properties of domain wcard_hc.Prelude_Boolx ...

Proving isomorphism properties of domain wcard_hc.Prelude_Natx ...

Proving induction properties of domain wcard_hc.Prelude_Natx ...

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, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,

Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,

wcard_hc} : Theory.theory

val it =

[("wcard_hc.map1_def",

"map1 ==

LAM x f.

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

| SSx$pX2$pX1 => x"),

("wcard_hc.Prelude_Natx.reach", "fix$Prelude_Natx_copy$?x = ?x"),

("wcard_hc.Prelude_Boolx.reach", "fix$Prelude_Boolx_copy$?x = ?x"),

("wcard_hc.Prelude_Natx.Sx_def",

"Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),

("wcard_hc.Prelude_Natx.Zx_def", "Zx == Prelude_Natx_abs$(sinl$ONE)"),

("wcard_hc.Prelude_Natx.SSx_def",

"SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),

("wcard_hc.Prelude_Natx.abs_iso",

"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),

("wcard_hc.Prelude_Natx.rep_iso",

"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),

("wcard_hc.Prelude_Boolx.abs_iso",

"Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),

("wcard_hc.Prelude_Boolx.rep_iso",

"Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),

("wcard_hc.Prelude_Natx.Sx_1_def",

"Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),

("wcard_hc.Prelude_Natx.copy_def",

"Prelude_Natx_copy ==

LAM f.

Prelude_Natx_abs oo

Prelude_Natx_when$(sinl$ONE)$(LAM a.

sinr$(sinl$a))$(LAM P'1 P'2.

sinr$(sinr$(:f$P'1, P'2:)))"),

("wcard_hc.Prelude_Natx.take_def",

"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),

("wcard_hc.Prelude_Natx.when_def",

"Prelude_Natx_when ==

LAM f1 f2 f3 x.

sscase$(LAM dummy.

f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),

("wcard_hc.Prelude_Boolx.Minx_def",

"Minx == Prelude_Boolx_abs$(sinl$ONE)"),

("wcard_hc.Prelude_Boolx.copy_def",

"Prelude_Boolx_copy ==

LAM f.

Prelude_Boolx_abs oo

Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),

("wcard_hc.Prelude_Boolx.take_def",

"Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),

("wcard_hc.Prelude_Boolx.when_def",

"Prelude_Boolx_when ==

LAM f1 f2 x.

case Prelude_Boolx_rep$x of sinl$dummy => f1

| sinr$dummy => f2"),

("wcard_hc.Prelude_Natx.SSx_1_def",

"SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),

("wcard_hc.Prelude_Natx.SSx_2_def",

"SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),

("wcard_hc.Prelude_Natx.bisim_def",

"Prelude_Natx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Zx & x' = Zx |

(EX a. a ~= UU & x = Sx$a & x' = Sx$a) |

(EX P'2 P'1 P'1'.

P'2 ~= UU &

P'1 ~= UU &

P'1' ~= UU &

R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),

("wcard_hc.Prelude_Natx.is_Sx_def",

"is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),

("wcard_hc.Prelude_Natx.is_Zx_def",

"is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),

("wcard_hc.Prelude_Boolx.Plusx_def",

"Plusx == Prelude_Boolx_abs$(sinr$ONE)"),

("wcard_hc.Prelude_Boolx.bisim_def",

"Prelude_Boolx_bisim ==

%R.

ALL x x'.

R x x' -->

x = UU & x' = UU |

x = Minx & x' = Minx | x = Plusx & x' = Plusx"),

("wcard_hc.Prelude_Natx.finite_def",

"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),

("wcard_hc.Prelude_Natx.is_SSx_def",

"is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),

("wcard_hc.Prelude_Boolx.finite_def",

"Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),

("wcard_hc.Prelude_Boolx.is_Minx_def",

"is_Minx == Prelude_Boolx_when$TT$FF"),

("wcard_hc.Prelude_Natx.match_Sx_def",

"match_Sx ==

Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),

("wcard_hc.Prelude_Natx.match_Zx_def",

"match_Zx ==

Prelude_Natx_when$(return$())$(LAM a.

fail)$(LAM P'1 P'2. fail)"),

("wcard_hc.Prelude_Boolx.is_Plusx_def",

"is_Plusx == Prelude_Boolx_when$FF$TT"),

("wcard_hc.Prelude_Natx.match_SSx_def",

"match_SSx ==

Prelude_Natx_when$fail$(LAM a.

fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),

("wcard_hc.Prelude_Boolx.match_Minx_def",

"match_Minx == Prelude_Boolx_when$(return$())$fail"),

("wcard_hc.Prelude_Boolx.match_Plusx_def",

"match_Plusx == Prelude_Boolx_when$fail$(return$())")]

: (string * Thm.thm) list