isabelle: src/HOL/Nitpick_Examples/Integer_Nits.thy@8e0148e1f5f4 (annotated)

34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	1	(* Title: HOL/Nitpick_Examples/Integer_Nits.thy
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
48812 9509fc5485b2 fixed handling of "int" in the wake of its port to the quotient package blanchet parents: 48046 diff changeset	3	Copyright 2009-2012
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	4
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	5	Examples featuring Nitpick applied to natural numbers and integers.
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	6	*)
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	7
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 61076 diff changeset	8	section \<open>Examples Featuring Nitpick Applied to Natural Numbers and Integers\<close>
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	9
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	10	theory Integer_Nits
46090 f1796596ef60 tuned import blanchet parents: 45035 diff changeset	11	imports Main
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	12	begin
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	13
55893 aed17a173d16 fixed handling of 'case_prod' and other 'case' functions for interpreted types blanchet parents: 54680 diff changeset	14	nitpick_params [verbose, card = 1-5, bits = 1,2,3,4,6,
54680 93f6d33a754e reverted 86e0b402994c, which was accidentally qfinish'ed and pushed blanchet parents: 54633 diff changeset	15	sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	16
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	17	lemma "Suc x = x + 1"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	18	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	19	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	20	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	21
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	22	lemma "x < Suc x"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	23	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	24	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	25	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	26
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	27	lemma "x + y \<ge> (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	28	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	29	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	30	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	31
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	32	lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	33	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	34	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	35	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	36
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	37	lemma "x + y = y + (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	38	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	39	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	40	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	41
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	42	lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	43	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	44	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	45	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	46
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	47	lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	48	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	49	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	50	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	51
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	52	lemma "x - (0::nat) = x"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	53	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	54	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	55	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	56
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	57	lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	58	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	59	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	60	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	61
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	62	lemma "0 * y = (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	63	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	64	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	65	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	66
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	67	lemma "y * 0 = (0::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	68	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	69	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	70	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	71
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	72	lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	73	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	74	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	75	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	76
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	77	lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	78	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	79	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	80	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	81
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	82	lemma "x * y div y = (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	83	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	84	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	85	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	86
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	87	lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	88	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	89	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	90	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	91
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	92	lemma "5 * 55 < (260::nat)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	93	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	94	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	95	nitpick [binary_ints, bits = 9, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	96	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	97
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	98	lemma "nat (of_nat n) = n"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	99	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	100	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	101	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	102
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	103	lemma "x + y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	104	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	105	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	106	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	107
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	108	lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	109	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	110	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	111	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	112
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	113	lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	114	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	115	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	116	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	117
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	118	lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	119	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	120	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	121	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	122
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	123	lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	124	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	125	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	126	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	127
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	128	lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	129	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	130	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	131	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	132
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	133	lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	134	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	135	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	136	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	137
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	138	lemma "x + y = y + (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	139	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	140	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	141	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	142
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	143	lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	144	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	145	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	146	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	147
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	148	lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	149	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	150	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	151	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	152
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	153	lemma "x - (0::int) = x"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	154	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	155	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	156	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	157
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	158	lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	159	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	160	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	161	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	162
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	163	lemma "0 * y = (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	164	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	165	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	166	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	167
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	168	lemma "y * 0 = (0::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	169	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	170	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	171	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	172
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	173	lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	174	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	175	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	176	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	177
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	178	lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	179	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	180	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	181	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	182
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	183	lemma "x * y div y = (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	184	nitpick [unary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	185	nitpick [binary_ints, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	186	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	187
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	188	lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	189	nitpick [unary_ints, expect = none]
55893 aed17a173d16 fixed handling of 'case_prod' and other 'case' functions for interpreted types blanchet parents: 54680 diff changeset	190	nitpick [binary_ints, card = 1-4, bits = 1-4, expect = none]
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	191	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	192
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	193	lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	194	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	195	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	196	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	197
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	198	lemma "-5 * 55 > (-260::int)"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	199	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	200	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	201	nitpick [binary_ints, bits = 9, expect = genuine]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	202	oops
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	203
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	204	lemma "nat (of_nat n) = n"
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	205	nitpick [unary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	206	nitpick [binary_ints, expect = none]
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	207	sorry
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	208
58310 91ea607a34d8 updated news blanchet parents: 58249 diff changeset	209	datatype tree = Null \| Node nat tree tree
35695 80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	210
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	211	primrec labels where
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	212	"labels Null = {}" \|
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	213	"labels (Node x t u) = {x} \<union> labels t \<union> labels u"
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	214
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	215	lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
37477 e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster blanchet parents: 35695 diff changeset	216	nitpick [expect = potential] (* unfortunate *)
35695 80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	217	oops
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	218
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	219	lemma "labels (Node x t u) \<noteq> {}"
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	220	nitpick [expect = none]
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	221	oops
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	222
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	223	lemma "card (labels t) > 0"
37477 e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster blanchet parents: 35695 diff changeset	224	nitpick [expect = potential] (* unfortunate *)
35695 80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	225	oops
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	226
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	227	lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
37477 e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster blanchet parents: 35695 diff changeset	228	nitpick [expect = potential] (* unfortunate *)
35695 80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	229	oops
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	230
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	231	lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
39362 ee65900bfced adapt examples to latest Nitpick changes + speed them up a little bit blanchet parents: 38185 diff changeset	232	nitpick [expect = potential] (* unfortunate *)
35695 80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	233	sorry
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	234
61076 bdc1e2f0a86a eliminated \<Colon>; wenzelm parents: 58889 diff changeset	235	lemma "(\<Sum>i \<in> labels (Node x t u). f i::nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
39362 ee65900bfced adapt examples to latest Nitpick changes + speed them up a little bit blanchet parents: 38185 diff changeset	236	nitpick [expect = potential] (* unfortunate *)
35695 80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	237	oops
80b2c22f8f00 fixed soundness bug in Nitpick blanchet parents: 35078 diff changeset	238
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: diff changeset	239	end

author	wenzelm
	Fri, 12 Aug 2016 11:53:47 +0200
changeset 63670	8e0148e1f5f4
parent 63167	0909deb8059b
child 74641	6f801e1073fa
permissions	-rw-r--r--