15 imports Main "~~/src/HOL/Library/Quotient_Product" RealDef |
15 imports Main "~~/src/HOL/Library/Quotient_Product" RealDef |
16 begin |
16 begin |
17 |
17 |
18 chapter {* 2. First Steps *} |
18 chapter {* 2. First Steps *} |
19 |
19 |
20 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1, |
20 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
21 timeout = 240] |
|
22 |
21 |
23 subsection {* 2.1. Propositional Logic *} |
22 subsection {* 2.1. Propositional Logic *} |
24 |
23 |
25 lemma "P \<longleftrightarrow> Q" |
24 lemma "P \<longleftrightarrow> Q" |
26 nitpick [expect = genuine] |
25 nitpick [expect = genuine] |
29 nitpick [expect = genuine] 2 |
28 nitpick [expect = genuine] 2 |
30 oops |
29 oops |
31 |
30 |
32 subsection {* 2.2. Type Variables *} |
31 subsection {* 2.2. Type Variables *} |
33 |
32 |
34 lemma "P x \<Longrightarrow> P (THE y. P y)" |
33 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
35 nitpick [verbose, expect = genuine] |
34 nitpick [verbose, expect = genuine] |
36 oops |
35 oops |
37 |
36 |
38 subsection {* 2.3. Constants *} |
37 subsection {* 2.3. Constants *} |
39 |
38 |
40 lemma "P x \<Longrightarrow> P (THE y. P y)" |
39 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
41 nitpick [show_consts, expect = genuine] |
40 nitpick [show_consts, expect = genuine] |
42 nitpick [dont_specialize, show_consts, expect = genuine] |
41 nitpick [dont_specialize, show_consts, expect = genuine] |
43 oops |
42 oops |
44 |
43 |
45 lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)" |
44 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
46 nitpick [expect = none] |
45 nitpick [expect = none] |
47 nitpick [card 'a = 1\<emdash>50, expect = none] |
46 nitpick [card 'a = 1\<emdash>50, expect = none] |
48 (* sledgehammer *) |
47 (* sledgehammer *) |
49 apply (metis the_equality) |
48 sledgehammer |
50 done |
49 by (metis the_equality) |
51 |
50 |
52 subsection {* 2.4. Skolemization *} |
51 subsection {* 2.4. Skolemization *} |
53 |
52 |
54 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x" |
53 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x" |
55 nitpick [expect = genuine] |
54 nitpick [expect = genuine] |
65 |
64 |
66 subsection {* 2.5. Natural Numbers and Integers *} |
65 subsection {* 2.5. Natural Numbers and Integers *} |
67 |
66 |
68 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n" |
67 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n" |
69 nitpick [expect = genuine] |
68 nitpick [expect = genuine] |
|
69 nitpick [binary_ints, bits = 16, expect = genuine] |
70 oops |
70 oops |
71 |
71 |
72 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P" |
72 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P" |
73 nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine] |
73 nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine] |
74 oops |
74 oops |
93 nitpick [show_datatypes, expect = genuine] |
93 nitpick [show_datatypes, expect = genuine] |
94 oops |
94 oops |
95 |
95 |
96 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} |
96 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} |
97 |
97 |
98 definition "three = {0\<Colon>nat, 1, 2}" |
98 typedef three = "{0\<Colon>nat, 1, 2}" |
99 typedef (open) three = three |
99 by blast |
100 unfolding three_def by blast |
|
101 |
100 |
102 definition A :: three where "A \<equiv> Abs_three 0" |
101 definition A :: three where "A \<equiv> Abs_three 0" |
103 definition B :: three where "B \<equiv> Abs_three 1" |
102 definition B :: three where "B \<equiv> Abs_three 1" |
104 definition C :: three where "C \<equiv> Abs_three 2" |
103 definition C :: three where "C \<equiv> Abs_three 2" |
105 |
104 |
106 lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x" |
105 lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X" |
107 nitpick [show_datatypes, expect = genuine] |
106 nitpick [show_datatypes, expect = genuine] |
108 oops |
107 oops |
109 |
108 |
110 fun my_int_rel where |
109 fun my_int_rel where |
111 "my_int_rel (x, y) (u, v) = (x + v = u + y)" |
110 "my_int_rel (x, y) (u, v) = (x + v = u + y)" |