equal
deleted
inserted
replaced
921 ("c*x+t",[c,t]) => |
921 ("c*x+t",[c,t]) => |
922 let |
922 let |
923 val cr = dest_frac c |
923 val cr = dest_frac c |
924 val clt = Thm.dest_fun2 ct |
924 val clt = Thm.dest_fun2 ct |
925 val cz = Thm.dest_arg ct |
925 val cz = Thm.dest_arg ct |
926 val neg = cr </ Rat.zero |
926 val neg = cr < Rat.zero |
927 val cthp = Simplifier.rewrite ctxt |
927 val cthp = Simplifier.rewrite ctxt |
928 (Thm.apply @{cterm "Trueprop"} |
928 (Thm.apply @{cterm "Trueprop"} |
929 (if neg then Thm.apply (Thm.apply clt c) cz |
929 (if neg then Thm.apply (Thm.apply clt c) cz |
930 else Thm.apply (Thm.apply clt cz) c)) |
930 else Thm.apply (Thm.apply clt cz) c)) |
931 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
931 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
944 | ("c*x",[c]) => |
944 | ("c*x",[c]) => |
945 let |
945 let |
946 val cr = dest_frac c |
946 val cr = dest_frac c |
947 val clt = Thm.dest_fun2 ct |
947 val clt = Thm.dest_fun2 ct |
948 val cz = Thm.dest_arg ct |
948 val cz = Thm.dest_arg ct |
949 val neg = cr </ Rat.zero |
949 val neg = cr < Rat.zero |
950 val cthp = Simplifier.rewrite ctxt |
950 val cthp = Simplifier.rewrite ctxt |
951 (Thm.apply @{cterm "Trueprop"} |
951 (Thm.apply @{cterm "Trueprop"} |
952 (if neg then Thm.apply (Thm.apply clt c) cz |
952 (if neg then Thm.apply (Thm.apply clt c) cz |
953 else Thm.apply (Thm.apply clt cz) c)) |
953 else Thm.apply (Thm.apply clt cz) c)) |
954 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
954 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
966 val T = Thm.typ_of_cterm x |
966 val T = Thm.typ_of_cterm x |
967 val cT = Thm.ctyp_of_cterm x |
967 val cT = Thm.ctyp_of_cterm x |
968 val cr = dest_frac c |
968 val cr = dest_frac c |
969 val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool})) |
969 val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool})) |
970 val cz = Thm.dest_arg ct |
970 val cz = Thm.dest_arg ct |
971 val neg = cr </ Rat.zero |
971 val neg = cr < Rat.zero |
972 val cthp = Simplifier.rewrite ctxt |
972 val cthp = Simplifier.rewrite ctxt |
973 (Thm.apply @{cterm "Trueprop"} |
973 (Thm.apply @{cterm "Trueprop"} |
974 (if neg then Thm.apply (Thm.apply clt c) cz |
974 (if neg then Thm.apply (Thm.apply clt c) cz |
975 else Thm.apply (Thm.apply clt cz) c)) |
975 else Thm.apply (Thm.apply clt cz) c)) |
976 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
976 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
991 val T = Thm.typ_of_cterm x |
991 val T = Thm.typ_of_cterm x |
992 val cT = Thm.ctyp_of_cterm x |
992 val cT = Thm.ctyp_of_cterm x |
993 val cr = dest_frac c |
993 val cr = dest_frac c |
994 val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool})) |
994 val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool})) |
995 val cz = Thm.dest_arg ct |
995 val cz = Thm.dest_arg ct |
996 val neg = cr </ Rat.zero |
996 val neg = cr < Rat.zero |
997 val cthp = Simplifier.rewrite ctxt |
997 val cthp = Simplifier.rewrite ctxt |
998 (Thm.apply @{cterm "Trueprop"} |
998 (Thm.apply @{cterm "Trueprop"} |
999 (if neg then Thm.apply (Thm.apply clt c) cz |
999 (if neg then Thm.apply (Thm.apply clt c) cz |
1000 else Thm.apply (Thm.apply clt cz) c)) |
1000 else Thm.apply (Thm.apply clt cz) c)) |
1001 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
1001 val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |