src/finite_maps/totoScript.sml

74 val _ = type_abbrev ("comp", Type`:'a->'a->cpn`);
76 val TotOrd = Define`TotOrd (c: 'a comp) =
115 val TO_exists = maybe_thm ("TO_exists", Term`?x:'a comp. TotOrd x`,
123 |- ?(rep :'x toto -> 'x comp). TYPE_DEFINITION (TotOrd :'x comp -> bool) rep*)
136    TO_apto_TO_ID = |- !(r :'x comp). TotOrd r <=> (apto (TO r) = r) *)
140 (* TO_11 = |- !(r :'x comp) (r' :'x comp).
145 (* onto_apto = |- !(r :'x comp). TotOrd r <=> ?(a :'x toto). r = apto a *)
149 (* TO_onto = |- !(a :'x toto). ?(r :'x comp). (a = TO r) /\ TotOrd r *)
152    wherever was previously "TotOrd (c:'a comp) ==> ... c ... . *)
171 Term`!c:'a comp. TotOrd c ==> (!x y. (c x y = EQUAL) <=> (x = y))`,
183 Term`!c:'a comp. TotOrd c ==> (!x. c x x = EQUAL)`,
197 Term`!c:'a comp. TotOrd c ==> (!x y. (c x y = GREATER) <=> (c y x = LESS))`,
279  Define`WeakLinearOrder_of_TO (c:'a comp) x y =
283  Define`StrongLinearOrder_of_TO (c:'a comp) x y =
336 val Strong_Strong_of_TO = maybe_thm ("Strong_Strong_of_TO", Term`!c:'a comp.
407 val TO_inv = Define`TO_inv (c:'a comp) x y = c y x`;
410 `!c:'a comp. TotOrd c ==> TotOrd (TO_inv c)`,
417 `!r:'a comp. TotOrd r ==> (toto_inv (TO r) = TO (TO_inv r))`,
442 Term`!c:'a comp. TO_inv (TO_inv c) = c`,
553 val lexTO = Define`(R:'a comp) lexTO (V:'b comp) = TO_of_LinearOrder (
560 Term`!R:'a comp V:'b comp. TotOrd R /\ TotOrd V ==> !x y.
572  ,Cases_on `V:'b comp (SND (x:'a#'b)) (SND (y:'a#'b))` THEN
579 val lexTO_ALT = maybe_thm ("lexTO_ALT", Term`!R:'a comp V:'b comp.
587 val TO_lexTO = maybe_thm ("TO_lexTO", Term`!R:'a comp V:'b comp.
971 val imageOrd = Define`imageOrd (f:'a->'c) (cp:'c comp) a b = cp (f a) (f b)`;
974 `!cp:'c comp. TotOrd cp ==> !f:'d->'c.