log revision 449dec898e52d1ce9b809df70cf26cd567ae8518
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettCopyright (c) 2002-5 CUTS and contributors.
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuPoly/ML 4.2.0 Release
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach> val it = () : unit
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettLoading theory "HsHOLCF" (required by "ex_class_hc")
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachconstants
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachProving isomorphism properties of domain HsHOLCF.llist ...
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettProving induction properties of domain HsHOLCF.llist ...
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettLoading theory "ex_class_hc"
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maederstructure Header :
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach sig val initialize : string list -> unit val record : string -> unit end
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachval it = () : unit
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachProving isomorphism properties of domain ex_class_hc.Prelude_MPList ...
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachProving induction properties of domain ex_class_hc.Prelude_MPList ...
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachProving isomorphism properties of domain ex_class_hc.Prelude_Color ...
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederProving induction properties of domain ex_class_hc.Prelude_Color ...
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettProving isomorphism properties of domain ex_class_hc.Prelude_MyList ...
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederProving induction properties of domain ex_class_hc.Prelude_MyList ...
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett### Specification of constant ex_class_hc.methodOne ::
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach### "'a Prelude_Color -> 'a Prelude_Color -> tr"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder### is strictly less general than the declared type
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder### Specification of constant ex_class_hc.methodTwo ::
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett### "'a Prelude_Color -> tr -> 'a Prelude_Color Prelude_Color"
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach### is strictly less general than the declared type
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach### Specification of constant ex_class_hc.methodOne ::
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder### "'a Prelude_MyList -> 'a Prelude_MyList -> tr"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly### is strictly less general than the declared type
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach### Specification of constant ex_class_hc.methodTwo ::
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder### "'a Prelude_MyList -> tr -> 'a Prelude_MyList Prelude_Color"
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett### is strictly less general than the declared type
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett### Specification of constant ex_class_hc.methodOne ::
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett### "('a, 'b) Prelude_MPList -> ('a, 'b) Prelude_MPList -> tr"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly### is strictly less general than the declared type
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder### Specification of constant ex_class_hc.methodTwo ::
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett### "('a, 'b) Prelude_MPList -> tr -> ('a, 'b) Prelude_MPList Prelude_Color"
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder### is strictly less general than the declared type
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett ex_class_hc} : Theory.theory
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederval it =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly [("ex_class_hc.myEqual_def",
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "myEqual ==
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi"),
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder ("ex_class_hc.Joker_class.intro",
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder "OFCLASS(?'a, pcpo_class) ==> OFCLASS(?'a, Joker_class)"),
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder ("ex_class_hc.Prelude_Color.reach", "fix$Prelude_Color_copy$?x = ?x"),
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder ("ex_class_hc.Prelude_MPList.reach",
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "fix$Prelude_MPList_copy$?x = ?x"),
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ("ex_class_hc.Prelude_MyList.reach",
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "fix$Prelude_MyList_copy$?x = ?x"),
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ("ex_class_hc.Prelude_Color.Red_def",
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Red == LAM a. Prelude_Color_abs$(sinl$a)"),
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ("ex_class_hc.Prelude_Color.abs_iso",
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder "Prelude_Color_rep$(Prelude_Color_abs$?x) = ?x"),
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder ("ex_class_hc.Prelude_Color.rep_iso",
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder "Prelude_Color_abs$(Prelude_Color_rep$?x) = ?x"),
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder ("ex_class_hc.Prelude_Color.Blue_def",
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder "Blue == LAM a. Prelude_Color_abs$(sinr$a)"),
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder ("ex_class_hc.Prelude_Color.copy_def",
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett "Prelude_Color_copy ==
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett LAM f.
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Prelude_Color_abs oo
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Prelude_Color_when$(LAM a. sinl$a)$(LAM a. sinr$a)"),
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett ("ex_class_hc.Prelude_Color.take_def",
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett "Prelude_Color_take == %n. iterate n Prelude_Color_copy UU"),
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett ("ex_class_hc.Prelude_Color.when_def",
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett "Prelude_Color_when ==
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett LAM f1 f2 x. sscase$f1$f2$(Prelude_Color_rep$x)"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("ex_class_hc.Prelude_MPList.abs_iso",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "Prelude_MPList_rep$(Prelude_MPList_abs$?x) = ?x"),
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett ("ex_class_hc.Prelude_MPList.rep_iso",
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett "Prelude_MPList_abs$(Prelude_MPList_rep$?x) = ?x"),
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett ("ex_class_hc.Prelude_MyList.abs_iso",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_MyList_rep$(Prelude_MyList_abs$?x) = ?x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.rep_iso",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_MyList_abs$(Prelude_MyList_rep$?x) = ?x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color.Red_1_def",
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett "Red_1 == Prelude_Color_when$(LAM a. a)$UU"),
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett ("ex_class_hc.Prelude_Color.bisim_def",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "Prelude_Color_bisim ==
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett %R.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ALL x x'.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly R x x' -->
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett x = UU & x' = UU |
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett (EX a. a ~= UU & x = Red$a & x' = Red$a) |
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett (EX a. a ~= UU & x = Blue$a & x' = Blue$a)"),
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett ("ex_class_hc.Prelude_MPList.copy_def",
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett "Prelude_MPList_copy ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM f.
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Prelude_MPList_abs oo
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Prelude_MPList_when$(sinl$ONE)$(LAM a b P'.
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett sinr$(:a, b, f$P':))"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("ex_class_hc.Prelude_MPList.take_def",
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett "Prelude_MPList_take == %n. iterate n Prelude_MPList_copy UU"),
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett ("ex_class_hc.Prelude_MPList.when_def",
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett "Prelude_MPList_when ==
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett LAM f1 f2 x.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sscase$(LAM dummy.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder f1)$(ssplit$(LAM a.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ssplit$(f2$a)))$(Prelude_MPList_rep$x)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_class_hc.Prelude_MyList.copy_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_MyList_copy ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM f.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_MyList_abs oo
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_MyList_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_class_hc.Prelude_MyList.take_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_MyList_take == %n. iterate n Prelude_MyList_copy UU"),
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ("ex_class_hc.Prelude_MyList.when_def",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "Prelude_MyList_when ==
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach LAM f1 f2 x.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_MyList_rep$x)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color.Blue_1_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Blue_1 == Prelude_Color_when$UU$(LAM a. a)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color.finite_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_Color_finite == %x. EX n. Prelude_Color_take n$x = x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color.is_Red_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "is_Red == Prelude_Color_when$(LAM a. TT)$(LAM a. FF)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.MPNil_def",
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett "MPNil == Prelude_MPList_abs$(sinl$ONE)"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("ex_class_hc.Prelude_MPList.bisim_def",
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett "Prelude_MPList_bisim ==
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett %R.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ALL x x'.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett R x x' -->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly x = UU & x' = UU |
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett x = MPNil & x' = MPNil |
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett (EX a b P' P''.
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett a ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly b ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly P' ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly P'' ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly R P' P'' & x = MPCons$a$b$P' & x' = MPCons$a$b$P'')"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.MyNil_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MyNil == Prelude_MyList_abs$(sinl$ONE)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.bisim_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_MyList_bisim ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly %R.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ALL x x'.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly R x x' -->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly x = UU & x' = UU |
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly x = MyNil & x' = MyNil |
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (EX a P' P''.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly a ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly P' ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly P'' ~= UU &
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly R P' P'' & x = MyCons$a$P' & x' = MyCons$a$P'')"),
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder ("ex_class_hc.Prelude_Color.is_Blue_def",
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder "is_Blue == Prelude_Color_when$(LAM a. FF)$(LAM a. TT)"),
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ("ex_class_hc.Prelude_MPList.MPCons_def",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "MPCons == LAM a b P'. Prelude_MPList_abs$(sinr$(:a, b, P':))"),
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ("ex_class_hc.Prelude_MPList.finite_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_MPList_finite == %x. EX n. Prelude_MPList_take n$x = x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.MyCons_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MyCons == LAM a P'. Prelude_MyList_abs$(sinr$(:a, P':))"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.finite_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_MyList_finite == %x. EX n. Prelude_MyList_take n$x = x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color.match_Red_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "match_Red == Prelude_Color_when$(LAM a. return$a)$(LAM a. fail)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color_methodOne_def", "methodOne == myEqual"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color_methodTwo_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "methodTwo == default__methodTwo"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.MPCons_1_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MPCons_1 == Prelude_MPList_when$UU$(LAM a b P'. a)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.MPCons_2_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MPCons_2 == Prelude_MPList_when$UU$(LAM a b P'. b)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.MPCons_3_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MPCons_3 == Prelude_MPList_when$UU$(LAM a b P'. P')"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.is_MPNil_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "is_MPNil == Prelude_MPList_when$TT$(LAM a b P'. FF)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.MyCons_1_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MyCons_1 == Prelude_MyList_when$UU$(LAM a P'. a)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.MyCons_2_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "MyCons_2 == Prelude_MyList_when$UU$(LAM a P'. P')"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.is_MyNil_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "is_MyNil == Prelude_MyList_when$TT$(LAM a P'. FF)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_Color.match_Blue_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "match_Blue == Prelude_Color_when$(LAM a. fail)$(LAM a. return$a)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.is_MPCons_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "is_MPCons == Prelude_MPList_when$FF$(LAM a b P'. TT)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList_methodOne_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "methodOne == default__methodOne"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList_methodTwo_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "methodTwo == default__methodTwo"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.is_MyCons_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "is_MyCons == Prelude_MyList_when$FF$(LAM a P'. TT)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList_methodOne_def", "methodOne == myEqual"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList_methodTwo_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "methodTwo ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly LAM x y.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly If (LAM x y. Def (x = y))$y$TT then Red$x else Blue$x fi"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.match_MPNil_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "match_MPNil ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Prelude_MPList_when$(return$())$(LAM a b P'. fail)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MyList.match_MyNil_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "match_MyNil == Prelude_MyList_when$(return$())$(LAM a P'. fail)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_class_hc.Prelude_MPList.match_MPCons_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "match_MPCons ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Prelude_MPList_when$fail$(LAM a b P'. return$<a, b, P'>)"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("ex_class_hc.Prelude_MyList.match_MyCons_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "match_MyCons ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Prelude_MyList_when$fail$(LAM a P'. return$<a, P'>)")]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly: (string * Thm.thm) list
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyCopyright (c) 2002-5 CUTS and contributors.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyPoly/ML 4.2.0 Release
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly> val it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyLoading theory "HsHOLCF" (required by "ex_fibon_hc")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyconstants
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyProving isomorphism properties of domain HsHOLCF.llist ...
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyProving induction properties of domain HsHOLCF.llist ...
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyLoading theory "ex_fibon_hc"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillystructure Header :
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sig val initialize : string list -> unit val record : string -> unit end
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ex_fibon_hc} : Theory.theory
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [("ex_fibon_hc.fibon_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "fibon ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly FIX fibon.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly run$(return$(LAM n.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly If (LAM x y. Def (x = y))$n$(Def 0)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then Def 1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else If (LAM x y. Def (x = y))$n$(Def 1)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then Def 1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op +$(fibon$(fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op -$n$(Def
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly 1)))$(fibon$(fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op -$n$(Def 2))) fi fi))")]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly: (string * Thm.thm) list
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyCopyright (c) 2002-5 CUTS and contributors.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettPoly/ML 4.2.0 Release
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett> val it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyLoading theory "HsHOLCF" (required by "ex_let_hc")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyconstants
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyProving isomorphism properties of domain HsHOLCF.llist ...
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyProving induction properties of domain HsHOLCF.llist ...
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyLoading theory "ex_let_hc"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillystructure Header :
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sig val initialize : string list -> unit val record : string -> unit end
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it = () : unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyval it =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett ex_let_hc} : Theory.theory
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyval it =
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett [("ex_let_hc.foon_def",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "foon ==
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett LAM a b c.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let testName1 >>= myEqual$a$b
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly in Let (myEqual$b$c) (Rep_CFun (trand$testName1))"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("ex_let_hc.myEqual_def",
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "myEqual ==
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi")]
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly: (string * Thm.thm) list
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright (c) 2002-5 CUTS and contributors.
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyPoly/ML 4.2.0 Release
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly> val it = () : unit
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettLoading theory "HsHOLCF" (required by "ex_list_hc")
842ae753ab848a8508c4832ab64296b929167a97Christian Maederconstants
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyProving isomorphism properties of domain HsHOLCF.llist ...
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettProving induction properties of domain HsHOLCF.llist ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederLoading theory "ex_list_hc"
842ae753ab848a8508c4832ab64296b929167a97Christian Maederstructure Header :
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sig val initialize : string list -> unit val record : string -> unit end
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettval it = () : unit
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it = () : unit
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it = () : unit
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyval it =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ex_list_hc} : Theory.theory
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reillyval it =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly [("ex_list_hc.myMap_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "myMap ==
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly FIX myMap.
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly run$(return$(LAM x f.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly case x of lNil => lNil
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett | lCons$pX1$pX2 => lCons$(f$pX1)$(myMap$pX2$f)))"),
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ("ex_list_hc.funOne_def",
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "funOne ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM x y.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly If (LAM x y. Def (x = y))$x$(lCons$(lHd$x)$(lTl$y))
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly then TT else FF fi")] : (string * Thm.thm) list
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettCopyright (c) 2002-5 CUTS and contributors.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
842ae753ab848a8508c4832ab64296b929167a97Christian MaederMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyPoly/ML 4.2.0 Release
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly> val it = () : unit
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLoading theory "HsHOLCF" (required by "ex_mutrec_hc")
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettconstants
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyProving isomorphism properties of domain HsHOLCF.llist ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving induction properties of domain HsHOLCF.llist ...
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLoading theory "ex_mutrec_hc"
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillystructure Header :
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sig val initialize : string list -> unit val record : string -> unit end
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettval it = () : unit
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyProving isomorphism properties of domain ex_mutrec_hc.Prelude_MyList ...
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyProving induction properties of domain ex_mutrec_hc.Prelude_MyList ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving isomorphism properties of domain ex_mutrec_hc.Prelude_Form ...
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyProving induction properties of domain ex_mutrec_hc.Prelude_Form ...
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyProving isomorphism properties of domain ex_mutrec_hc.Prelude_CList ...
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyProving isomorphism properties of domain ex_mutrec_hc.Prelude_LColor ...
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettProving induction properties of domain ex_mutrec_hc.Prelude_CList_Prelude_LColor ...
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyval it = () : unit
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyval it = () : unit
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ex_mutrec_hc} : Theory.theory
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyval it =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly [("ex_mutrec_hc.fibon_def",
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett "fibon ==
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly FIX fibon.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly run$(return$(LAM n.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly If (LAM x y. Def (x = y))$n$(Def 0)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly then Def 1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly else If (LAM x y. Def (x = y))$n$(Def 1)
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett then Def 1
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett else fliftbin
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder op +$(fibon$(fliftbin
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly op -$n$(Def
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly 1)))$(fibon$(fliftbin
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly op -$n$(Def 2))) fi fi))"),
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("ex_mutrec_hc.myEqual_def",
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett "myEqual ==
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.hasColor_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "hasColor ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM x y.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly If myEqual$x$y
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett then Red$((LAM z. Square$x$z)$x)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly else Blue$(Rectangle$x$y) fi"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.mRecFun1_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "mRecFun1 ==
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cfst$(FIX <mRecFun1, mRecFun2>.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <run$(return$(LAM n.
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly If (LAM x y. Def (x = y))$n$(Def 0)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly then Def 0
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett else If (LAM x y. Def (x = y))$n$(Def 1)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly then Def 2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly else fliftbin
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly op +$(mRecFun1$(fliftbin
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett op -$n$(Def
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly 1)))$(mRecFun2$(fliftbin
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly op -$n$(Def 2))) fi fi)),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly run$(return$(LAM n.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly If (LAM x y. Def (x = y))$n$(Def 0)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly then Def 0
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly else If (LAM x y. Def (x = y))$n$(Def 1)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly then Def 0
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett else fliftbin
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder op +$(mRecFun1$(fliftbin
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett op -$n$(Def
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder 1)))$(mRecFun2$(fliftbin
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly op -$n$(Def 1))) fi fi))>)"),
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("ex_mutrec_hc.mRecFun2_def",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "mRecFun2 ==
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly csnd$(FIX <mRecFun1, mRecFun2>.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <run$(return$(LAM n.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly If (LAM x y. Def (x = y))$n$(Def 0)
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett then Def 0
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly else If (LAM x y. Def (x = y))$n$(Def 1)
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly then Def 2
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly else fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op +$(mRecFun1$(fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op -$n$(Def
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly 1)))$(mRecFun2$(fliftbin
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett op -$n$(Def 2))) fi fi)),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly run$(return$(LAM n.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly If (LAM x y. Def (x = y))$n$(Def 0)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then Def 0
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else If (LAM x y. Def (x = y))$n$(Def 1)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then Def 0
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op +$(mRecFun1$(fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op -$n$(Def
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly 1)))$(mRecFun2$(fliftbin
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly op -$n$(Def 1))) fi fi))>)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.reach", "fix$Prelude_Form_copy$?x = ?x"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_CList.reach",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "cfst$(fix$Prelude_CList_Prelude_LColor_copy)$?x1.0 = ?x1.0"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.abs_iso",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_Form_rep$(Prelude_Form_abs$?x) = ?x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.rep_iso",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_Form_abs$(Prelude_Form_rep$?x) = ?x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_LColor.reach",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "csnd$(fix$Prelude_CList_Prelude_LColor_copy)$?x2.0 = ?x2.0"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_MyList.reach",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "fix$Prelude_MyList_copy$?x = ?x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_CList.abs_iso",
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly "Prelude_CList_rep$(Prelude_CList_abs$?x) = ?x"),
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.rep_iso",
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly "Prelude_CList_abs$(Prelude_CList_rep$?x) = ?x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.copy_def",
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett "Prelude_Form_copy ==
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly LAM f.
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly Prelude_Form_abs oo
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_Form_when$(LAM a b.
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett sinl$(:a, b:))$(LAM a b. sinr$(:a, b:))"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("ex_mutrec_hc.Prelude_Form.take_def",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "Prelude_Form_take == %n. iterate n Prelude_Form_copy UU"),
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.when_def",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "Prelude_Form_when ==
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett LAM f1 f2 x.
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett sscase$(ssplit$f1)$(ssplit$f2)$(Prelude_Form_rep$x)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_CList.copy_def",
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett "Prelude_CList_copy ==
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly LAM f.
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly Prelude_CList_abs oo
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly Prelude_CList_when$(sinl$ONE)$(LAM P'1 P'2.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sinr$(:P'1, cfst$f$P'2:))"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_CList.take_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_CList_take ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder %n. cfst$(iterate n Prelude_CList_Prelude_LColor_copy UU)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_CList.when_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_CList_when ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM f1 f2 x.
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_CList_rep$x)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_Form.bisim_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_Form_bisim ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder %R.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ALL x x'.
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett R x x' -->
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett x = UU & x' = UU |
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (EX a b.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly a ~= UU & b ~= UU & x = Square$a$b & x' = Square$a$b) |
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (EX a b.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly a ~= UU &
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly b ~= UU & x = Rectangle$a$b & x' = Rectangle$a$b)"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.Red_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Red == LAM a. Prelude_LColor_abs$(sinr$(sinl$a))"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.abs_iso",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_LColor_rep$(Prelude_LColor_abs$?x) = ?x"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_LColor.rep_iso",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_LColor_abs$(Prelude_LColor_rep$?x) = ?x"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.abs_iso",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_MyList_rep$(Prelude_MyList_abs$?x) = ?x"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.rep_iso",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_MyList_abs$(Prelude_MyList_rep$?x) = ?x"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.CCons_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "CCons == LAM P'1 P'2. Prelude_CList_abs$(sinr$(:P'1, P'2:))"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.Trans_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Trans == Prelude_CList_abs$(sinl$ONE)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.Square_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Square == LAM a b. Prelude_Form_abs$(sinl$(:a, b:))"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.finite_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_Form_finite == %x. EX n. Prelude_Form_take n$x = x"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_LColor.Blue_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Blue == LAM a. Prelude_LColor_abs$(sinl$a)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_LColor.copy_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_LColor_copy ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly LAM f.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Prelude_LColor_abs oo
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Prelude_LColor_when$(LAM a.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sinl$a)$(LAM a. sinr$(sinl$a))$(LAM P'. sinr$(sinr$P'))"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_LColor.take_def",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Prelude_LColor_take ==
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly %n. csnd$(iterate n Prelude_CList_Prelude_LColor_copy UU)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ex_mutrec_hc.Prelude_LColor.when_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_LColor_when ==
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly LAM f1 f2 f3 x.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sscase$f1$(sscase$f2$f3)$(Prelude_LColor_rep$x)"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.copy_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_MyList_copy ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM f.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_MyList_abs oo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Prelude_MyList_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.take_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_MyList_take == %n. iterate n Prelude_MyList_copy UU"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_MyList.when_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_MyList_when ==
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett LAM f1 f2 x.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_MyList_rep$x)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_CList.finite_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_CList_finite == %x1. EX n. Prelude_CList_take n$x1 = x1"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_LColor.Multi_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Multi == LAM P'. Prelude_LColor_abs$(sinr$(sinr$P'))"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.Red_1_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Red_1 == Prelude_LColor_when$UU$(LAM a. a)$UU"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.MyNil_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "MyNil == Prelude_MyList_abs$(sinl$ONE)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ex_mutrec_hc.Prelude_MyList.bisim_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_MyList_bisim ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder %R.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ALL x x'.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder R x x' -->
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett x = UU & x' = UU |
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett x = MyNil & x' = MyNil |
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett (EX a P' P''.
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly a ~= UU &
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly P' ~= UU &
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly P'' ~= UU &
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly R P' P'' & x = MyCons$a$P' & x' = MyCons$a$P'')"),
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.CCons_1_def",
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly "CCons_1 == Prelude_CList_when$UU$(LAM P'1 P'2. P'1)"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_CList.CCons_2_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "CCons_2 == Prelude_CList_when$UU$(LAM P'1 P'2. P'2)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.Square_1_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Square_1 == Prelude_Form_when$(LAM a b. a)$UU"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.Square_2_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Square_2 == Prelude_Form_when$(LAM a b. b)$UU"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.Blue_1_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Blue_1 == Prelude_LColor_when$(LAM a. a)$UU$UU"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.finite_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Prelude_LColor_finite ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly %x2. EX n. Prelude_LColor_take n$x2 = x2"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.is_Red_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "is_Red ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Prelude_LColor_when$(LAM a. FF)$(LAM a. TT)$(LAM P'. FF)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.MyCons_def",
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly "MyCons == LAM a P'. Prelude_MyList_abs$(sinr$(:a, P':))"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.finite_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Prelude_MyList_finite == %x. EX n. Prelude_MyList_take n$x = x"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.is_CCons_def",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "is_CCons == Prelude_CList_when$FF$(LAM P'1 P'2. TT)"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_CList.is_Trans_def",
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly "is_Trans == Prelude_CList_when$TT$(LAM P'1 P'2. FF)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.Rectangle_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Rectangle == LAM a b. Prelude_Form_abs$(sinr$(:a, b:))"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.is_Square_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "is_Square == Prelude_Form_when$(LAM a b. TT)$(LAM a b. FF)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.Multi_1_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Multi_1 == Prelude_LColor_when$UU$UU$(LAM P'. P')"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.is_Blue_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "is_Blue ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Prelude_LColor_when$(LAM a. TT)$(LAM a. FF)$(LAM P'. FF)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.is_Multi_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "is_Multi ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Prelude_LColor_when$(LAM a. FF)$(LAM a. FF)$(LAM P'. TT)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.MyCons_1_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "MyCons_1 == Prelude_MyList_when$UU$(LAM a P'. a)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.MyCons_2_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "MyCons_2 == Prelude_MyList_when$UU$(LAM a P'. P')"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_MyList.is_MyNil_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "is_MyNil == Prelude_MyList_when$TT$(LAM a P'. FF)"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.Rectangle_1_def",
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly "Rectangle_1 == Prelude_Form_when$UU$(LAM a b. a)"),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.Rectangle_2_def",
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly "Rectangle_2 == Prelude_Form_when$UU$(LAM a b. b)"),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.match_Red_def",
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly "match_Red ==
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett Prelude_LColor_when$(LAM a.
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly fail)$(LAM a. return$a)$(LAM P'. fail)"),
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett ("ex_mutrec_hc.Prelude_MyList.is_MyCons_def",
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett "is_MyCons == Prelude_MyList_when$FF$(LAM a P'. TT)"),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.match_CCons_def",
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly "match_CCons ==
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly Prelude_CList_when$fail$(LAM P'1 P'2. return$<P'1, P'2>)"),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly ("ex_mutrec_hc.Prelude_CList.match_Trans_def",
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly "match_Trans ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_CList_when$(return$())$(LAM P'1 P'2. fail)"),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.is_Rectangle_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "is_Rectangle == Prelude_Form_when$(LAM a b. FF)$(LAM a b. TT)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_Form.match_Square_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "match_Square ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Prelude_Form_when$(LAM a b. return$<a, b>)$(LAM a b. fail)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.match_Blue_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "match_Blue ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Prelude_LColor_when$(LAM a.
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly return$a)$(LAM a. fail)$(LAM P'. fail)"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_LColor.match_Multi_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "match_Multi ==
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Prelude_LColor_when$(LAM a.
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly fail)$(LAM a. fail)$(LAM P'. return$P')"),
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ("ex_mutrec_hc.Prelude_MyList.match_MyNil_def",
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "match_MyNil == Prelude_MyList_when$(return$())$(LAM a P'. fail)"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_MyList.match_MyCons_def",
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly "match_MyCons ==
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Prelude_MyList_when$fail$(LAM a P'. return$<a, P'>)"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_Form.match_Rectangle_def",
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett "match_Rectangle ==
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Prelude_Form_when$(LAM a b. fail)$(LAM a b. return$<a, b>)"),
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ("ex_mutrec_hc.Prelude_CList_Prelude_LColor.copy_def",
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett "Prelude_CList_Prelude_LColor_copy ==
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett LAM f. <Prelude_CList_copy$f, Prelude_LColor_copy$f>"),
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett ("ex_mutrec_hc.Prelude_CList_Prelude_LColor.bisim_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_CList_Prelude_LColor_bisim ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder %R.
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett (ALL x1 x1'.
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly fst R x1 x1' -->
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly x1 = UU & x1' = UU |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder x1 = Trans & x1' = Trans |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (EX P'1 P'2 P'2'.
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett P'1 ~= UU &
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett P'2 ~= UU &
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder P'2' ~= UU &
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder fst R P'2 P'2' &
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder x1 = CCons$P'1$P'2 & x1' = CCons$P'1$P'2')) &
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (ALL x2 x2'.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder snd R x2 x2' -->
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder x2 = UU & x2' = UU |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (EX a. a ~= UU & x2 = Blue$a & x2' = Blue$a) |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (EX a. a ~= UU & x2 = Red$a & x2' = Red$a) |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (EX P'. P' ~= UU & x2 = Multi$P' & x2' = Multi$P'))")]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder: (string * Thm.thm) list
842ae753ab848a8508c4832ab64296b929167a97Christian MaederPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
842ae753ab848a8508c4832ab64296b929167a97Christian MaederCopyright (c) 2002-5 CUTS and contributors.
842ae753ab848a8508c4832ab64296b929167a97Christian MaederRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
842ae753ab848a8508c4832ab64296b929167a97Christian MaederMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
842ae753ab848a8508c4832ab64296b929167a97Christian MaederMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
842ae753ab848a8508c4832ab64296b929167a97Christian MaederPoly/ML 4.2.0 Release
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder> val it = () : unit
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyLoading theory "HsHOLCF" (required by "incmpl_hc")
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reillyconstants
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyProving isomorphism properties of domain HsHOLCF.llist ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving induction properties of domain HsHOLCF.llist ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederLoading theory "incmpl_hc"
842ae753ab848a8508c4832ab64296b929167a97Christian Maederstructure Header :
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sig val initialize : string list -> unit val record : string -> unit end
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it = () : unit
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving isomorphism properties of domain incmpl_hc.Prelude_Boolx ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving induction properties of domain incmpl_hc.Prelude_Boolx ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving isomorphism properties of domain incmpl_hc.Prelude_Natx ...
842ae753ab848a8508c4832ab64296b929167a97Christian MaederProving induction properties of domain incmpl_hc.Prelude_Natx ...
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it = () : unit
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it = () : unit
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly incmpl_hc} : Theory.theory
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillyval it =
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett [("incmpl_hc.map1_def",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "map1 ==
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly LAM x f.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | SSx$pX2$pX1 => UU"),
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett ("incmpl_hc.Prelude_Natx.reach", "fix$Prelude_Natx_copy$?x = ?x"),
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett ("incmpl_hc.Prelude_Boolx.reach", "fix$Prelude_Boolx_copy$?x = ?x"),
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett ("incmpl_hc.Prelude_Natx.Sx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.Zx_def", "Zx == Prelude_Natx_abs$(sinl$ONE)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.SSx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.abs_iso",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.rep_iso",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Boolx.abs_iso",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("incmpl_hc.Prelude_Boolx.rep_iso",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("incmpl_hc.Prelude_Natx.Sx_1_def",
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.copy_def",
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett "Prelude_Natx_copy ==
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett LAM f.
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Prelude_Natx_abs oo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Prelude_Natx_when$(sinl$ONE)$(LAM a.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sinr$(sinl$a))$(LAM P'1 P'2.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sinr$(sinr$(:f$P'1, P'2:)))"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("incmpl_hc.Prelude_Natx.take_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.when_def",
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly "Prelude_Natx_when ==
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly LAM f1 f2 f3 x.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sscase$(LAM dummy.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("incmpl_hc.Prelude_Boolx.Minx_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Minx == Prelude_Boolx_abs$(sinl$ONE)"),
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly ("incmpl_hc.Prelude_Boolx.copy_def",
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly "Prelude_Boolx_copy ==
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly LAM f.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Prelude_Boolx_abs oo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Boolx.take_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("incmpl_hc.Prelude_Boolx.when_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_Boolx_when ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM f1 f2 x.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case Prelude_Boolx_rep$x of sinl$dummy => f1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly | sinr$dummy => f2"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("incmpl_hc.Prelude_Natx.SSx_1_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.SSx_2_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("incmpl_hc.Prelude_Natx.bisim_def",
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Prelude_Natx_bisim ==
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly %R.
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly ALL x x'.
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly R x x' -->
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly x = UU & x' = UU |
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly x = Zx & x' = Zx |
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (EX a. a ~= UU & x = Sx$a & x' = Sx$a) |
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (EX P'2 P'1 P'1'.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett P'2 ~= UU &
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett P'1 ~= UU &
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett P'1' ~= UU &
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("incmpl_hc.Prelude_Natx.is_Sx_def",
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett "is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.is_Zx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Boolx.Plusx_def",
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett "Plusx == Prelude_Boolx_abs$(sinr$ONE)"),
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ("incmpl_hc.Prelude_Boolx.bisim_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_Boolx_bisim ==
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett %R.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ALL x x'.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett R x x' -->
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett x = UU & x' = UU |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder x = Minx & x' = Minx | x = Plusx & x' = Plusx"),
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ("incmpl_hc.Prelude_Natx.finite_def",
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett "Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Natx.is_SSx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Boolx.finite_def",
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett "Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ("incmpl_hc.Prelude_Boolx.is_Minx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "is_Minx == Prelude_Boolx_when$TT$FF"),
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ("incmpl_hc.Prelude_Natx.match_Sx_def",
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "match_Sx ==
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett ("incmpl_hc.Prelude_Natx.match_Zx_def",
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett "match_Zx ==
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Prelude_Natx_when$(return$())$(LAM a.
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett fail)$(LAM P'1 P'2. fail)"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("incmpl_hc.Prelude_Boolx.is_Plusx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "is_Plusx == Prelude_Boolx_when$FF$TT"),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("incmpl_hc.Prelude_Natx.match_SSx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "match_SSx ==
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Prelude_Natx_when$fail$(LAM a.
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("incmpl_hc.Prelude_Boolx.match_Minx_def",
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett "match_Minx == Prelude_Boolx_when$(return$())$fail"),
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett ("incmpl_hc.Prelude_Boolx.match_Plusx_def",
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett "match_Plusx == Prelude_Boolx_when$fail$(return$())")]
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett: (string * Thm.thm) list
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettPoly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettCopyright (c) 2002-5 CUTS and contributors.
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettRunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettMapping /local/mirror/linux-bkb/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOLCF
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettMapping /home/linux-bkb/Isabelle/polyml-4.1.4/x86-linux/ML_dbase
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettPoly/ML 4.2.0 Release
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett> val it = () : unit
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettLoading theory "HsHOLCF" (required by "mrec3_hc")
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettconstants
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettProving isomorphism properties of domain HsHOLCF.llist ...
c909c215242232fe78ce335e677e6f22264a0ee9Christian MaederProving induction properties of domain HsHOLCF.llist ...
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettLoading theory "mrec3_hc"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettstructure Header :
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder sig val initialize : string list -> unit val record : string -> unit end
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederval it = () : unit
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederProving isomorphism properties of domain mrec3_hc.Prelude_Boolx ...
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederProving induction properties of domain mrec3_hc.Prelude_Boolx ...
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettProving isomorphism properties of domain mrec3_hc.Prelude_Natx ...
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettProving induction properties of domain mrec3_hc.Prelude_Natx ...
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettval it = () : unit
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettval it = () : unit
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederval it =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mrec3_hc} : Theory.theory
842ae753ab848a8508c4832ab64296b929167a97Christian Maederval it =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [("mrec3_hc.map1_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "map1 ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder cfst$(FIX <map1, map2>.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <run$(return$(LAM x f.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder | SSx$pX1$pX2 => map2$pX1$pX2$f)),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder run$(return$(LAM x w f.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case x of Zx => Zx
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett | Sx$pX1 => Sx$(fliftbin op +$pX1$(Def 1))
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett | SSx$pX1$pX2 =>
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett If (LAM x y. Def (x = y))$pX2$Minx
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett then SSx$pX1$w else map1$pX1$f fi))>)"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.map2_def",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "map2 ==
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett csnd$(FIX <map1, map2>.
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett <run$(return$(LAM x f.
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett | SSx$pX1$pX2 => map2$pX1$pX2$f)),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly run$(return$(LAM x w f.
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett case x of Zx => Zx
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett | Sx$pX1 => Sx$(fliftbin op +$pX1$(Def 1))
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett | SSx$pX1$pX2 =>
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett If (LAM x y. Def (x = y))$pX2$Minx
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett then SSx$pX1$w else map1$pX1$f fi))>)"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Natx.reach", "fix$Prelude_Natx_copy$?x = ?x"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Boolx.reach", "fix$Prelude_Boolx_copy$?x = ?x"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Natx.Sx_def",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Natx.Zx_def", "Zx == Prelude_Natx_abs$(sinl$ONE)"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Natx.SSx_def",
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder "SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder ("mrec3_hc.Prelude_Natx.abs_iso",
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder "Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ("mrec3_hc.Prelude_Natx.rep_iso",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Boolx.abs_iso",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Boolx.rep_iso",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Natx.Sx_1_def",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("mrec3_hc.Prelude_Natx.copy_def",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Prelude_Natx_copy ==
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett LAM f.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_Natx_abs oo
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Prelude_Natx_when$(sinl$ONE)$(LAM a.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sinr$(sinl$a))$(LAM P'1 P'2.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sinr$(sinr$(:f$P'1, P'2:)))"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Natx.take_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("mrec3_hc.Prelude_Natx.when_def",
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett "Prelude_Natx_when ==
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder LAM f1 f2 f3 x.
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett sscase$(LAM dummy.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ("mrec3_hc.Prelude_Boolx.Minx_def",
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Minx == Prelude_Boolx_abs$(sinl$ONE)"),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("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