src/HOL/Nitpick_Examples/Manual_Nits.thy
author blanchet
Mon, 09 Aug 2010 13:46:25 +0200
changeset 38288 63425c4b5f57
parent 38284 9f98107ad8b4
child 39198 f967a16dfcdd
permissions -rw-r--r--
"declare" -> "declaration" (typo)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 34982
diff changeset
     3
    Copyright   2009, 2010
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     4
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     5
Examples from the Nitpick manual.
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     6
*)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     7
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     8
header {* Examples from the Nitpick Manual *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     9
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
    10
(* The "expect" arguments to Nitpick in this theory and the other example
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
    11
   theories are there so that the example can also serve as a regression test
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
    12
   suite. *)
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
    13
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    14
theory Manual_Nits
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
    15
imports Main Quotient_Product RealDef
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    16
begin
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    17
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    18
chapter {* 3. First Steps *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    19
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
    20
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    21
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    22
subsection {* 3.1. Propositional Logic *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    23
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    24
lemma "P \<longleftrightarrow> Q"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    25
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    26
apply auto
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    27
nitpick [expect = genuine] 1
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    28
nitpick [expect = genuine] 2
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    29
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    30
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    31
subsection {* 3.2. Type Variables *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    32
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    33
lemma "P x \<Longrightarrow> P (THE y. P y)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    34
nitpick [verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    35
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    36
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    37
subsection {* 3.3. Constants *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    38
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    39
lemma "P x \<Longrightarrow> P (THE y. P y)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    40
nitpick [show_consts, expect = genuine]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    41
nitpick [full_descrs, show_consts, expect = genuine]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    42
nitpick [dont_specialize, full_descrs, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    43
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    44
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    45
lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    46
nitpick [expect = none]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    47
nitpick [card 'a = 1\<midarrow>50, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    48
(* sledgehammer *)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    49
apply (metis the_equality)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    50
done
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    51
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    52
subsection {* 3.4. Skolemization *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    53
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    54
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    55
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    56
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    57
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    58
lemma "\<exists>x. \<forall>f. f x = x"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    59
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    60
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    61
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    62
lemma "refl r \<Longrightarrow> sym r"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    63
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    64
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    65
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 33197
diff changeset
    66
subsection {* 3.5. Natural Numbers and Integers *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    67
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    68
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    69
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    70
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    71
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    72
lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    73
nitpick [card nat = 100, check_potential, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    74
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    75
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    76
lemma "P Suc"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    77
nitpick [expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    78
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    79
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    80
lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    81
nitpick [card nat = 1, expect = genuine]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    82
nitpick [card nat = 2, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    83
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    84
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    85
subsection {* 3.6. Inductive Datatypes *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    86
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    87
lemma "hd (xs @ [y, y]) = hd xs"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    88
nitpick [expect = genuine]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    89
nitpick [show_consts, show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    90
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    91
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    92
lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
    93
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    94
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    95
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    96
subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    97
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    98
typedef three = "{0\<Colon>nat, 1, 2}"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    99
by blast
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   100
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   101
definition A :: three where "A \<equiv> Abs_three 0"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   102
definition B :: three where "B \<equiv> Abs_three 1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   103
definition C :: three where "C \<equiv> Abs_three 2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   104
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   105
lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   106
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   107
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   108
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   109
fun my_int_rel where
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   110
"my_int_rel (x, y) (u, v) = (x + v = u + y)"
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   111
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   112
quotient_type my_int = "nat \<times> nat" / my_int_rel
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   113
by (auto simp add: equivp_def expand_fun_eq)
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   114
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   115
definition add_raw where
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   116
"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   117
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   118
quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   119
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   120
lemma "add x y = add x x"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   121
nitpick [show_datatypes, expect = genuine]
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   122
oops
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   123
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   124
ML {*
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35711
diff changeset
   125
fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35711
diff changeset
   126
    HOLogic.mk_number T (snd (HOLogic.dest_number t1)
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35711
diff changeset
   127
                         - snd (HOLogic.dest_number t2))
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35711
diff changeset
   128
  | my_int_postproc _ _ _ _ t = t
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   129
*}
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   130
38288
63425c4b5f57 "declare" -> "declaration" (typo)
blanchet
parents: 38284
diff changeset
   131
declaration {*
38284
9f98107ad8b4 use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents: 38242
diff changeset
   132
Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
38242
f26d590dce0f adapt occurrences of renamed Nitpick functions
blanchet
parents: 38184
diff changeset
   133
*}
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   134
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   135
lemma "add x y = add x x"
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   136
nitpick [show_datatypes]
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   137
oops
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   138
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   139
record point =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   140
  Xcoord :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   141
  Ycoord :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   142
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   143
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   144
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   145
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   146
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   147
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   148
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   149
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   150
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   151
subsection {* 3.8. Inductive and Coinductive Predicates *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   152
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   153
inductive even where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   154
"even 0" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   155
"even n \<Longrightarrow> even (Suc (Suc n))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   156
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   157
lemma "\<exists>n. even n \<and> even (Suc n)"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   158
nitpick [card nat = 50, unary_ints, verbose, expect = potential]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   159
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   160
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   161
lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   162
nitpick [card nat = 50, unary_ints, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   163
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   164
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   165
inductive even' where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   166
"even' (0\<Colon>nat)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   167
"even' 2" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   168
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   169
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   170
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   171
nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   172
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   173
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   174
lemma "even' (n - 2) \<Longrightarrow> even' n"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   175
nitpick [card nat = 10, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   176
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   177
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   178
coinductive nats where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   179
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   180
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   181
lemma "nats = {0, 1, 2, 3, 4}"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   182
nitpick [card nat = 10, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   183
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   184
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   185
inductive odd where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   186
"odd 1" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   187
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   188
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   189
lemma "odd n \<Longrightarrow> odd (n - 2)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   190
nitpick [card nat = 10, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   191
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   192
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   193
subsection {* 3.9. Coinductive Datatypes *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   194
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   195
(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   196
   we cannot rely on its presence, we expediently provide our own
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   197
   axiomatization. The examples also work unchanged with Lochbihler's
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   198
   "Coinductive_List" theory. *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   199
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   200
typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   201
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   202
definition LNil where
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   203
"LNil = Abs_llist (Inl [])"
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   204
definition LCons where
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   205
"LCons y ys = Abs_llist (case Rep_llist ys of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   206
                           Inl ys' \<Rightarrow> Inl (y # ys')
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   207
                         | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   208
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   209
axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   210
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   211
lemma iterates_def [nitpick_simp]:
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   212
"iterates f a = LCons a (iterates f (f a))"
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   213
sorry
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   214
38288
63425c4b5f57 "declare" -> "declaration" (typo)
blanchet
parents: 38284
diff changeset
   215
declaration {*
38284
9f98107ad8b4 use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents: 38242
diff changeset
   216
Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   217
    (map dest_Const [@{term LNil}, @{term LCons}])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   218
*}
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   219
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   220
lemma "xs \<noteq> LCons a xs"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   221
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   222
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   223
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   224
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   225
nitpick [verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   226
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   227
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   228
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   229
nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   230
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   231
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   232
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   233
subsection {* 3.10. Boxing *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   234
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   235
datatype tm = Var nat | Lam tm | App tm tm
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   236
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   237
primrec lift where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   238
"lift (Var j) k = Var (if j < k then j else j + 1)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   239
"lift (Lam t) k = Lam (lift t (k + 1))" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   240
"lift (App t u) k = App (lift t k) (lift u k)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   241
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   242
primrec loose where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   243
"loose (Var j) k = (j \<ge> k)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   244
"loose (Lam t) k = loose t (Suc k)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   245
"loose (App t u) k = (loose t k \<or> loose u k)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   246
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   247
primrec subst\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   248
"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   249
"subst\<^isub>1 \<sigma> (Lam t) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   250
 Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   251
"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   252
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   253
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   254
nitpick [verbose, expect = genuine]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   255
nitpick [eval = "subst\<^isub>1 \<sigma> t", expect = genuine]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   256
(* nitpick [dont_box, expect = unknown] *)
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   257
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   258
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   259
primrec subst\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   260
"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   261
"subst\<^isub>2 \<sigma> (Lam t) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   262
 Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   263
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   264
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   265
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   266
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   267
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   268
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   269
subsection {* 3.11. Scope Monotonicity *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   270
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   271
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   272
nitpick [verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   273
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   274
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   275
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   276
nitpick [mono, expect = none]
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   277
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   278
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   279
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   280
subsection {* 3.12. Inductive Properties *}
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   281
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   282
inductive_set reach where
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   283
"(4\<Colon>nat) \<in> reach" |
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   284
"n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   285
"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   286
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   287
lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   288
(* nitpick *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   289
apply (induct set: reach)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   290
  apply auto
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   291
 nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   292
 apply (thin_tac "n \<in> reach")
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   293
 nitpick [expect = genuine]
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   294
oops
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   295
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   296
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   297
(* nitpick *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   298
apply (induct set: reach)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   299
  apply auto
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   300
 nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   301
 apply (thin_tac "n \<in> reach")
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   302
 nitpick [expect = genuine]
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   303
oops
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   304
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   305
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   306
by (induct set: reach) arith+
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   307
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   308
datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   309
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   310
primrec labels where
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   311
"labels (Leaf a) = {a}" |
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   312
"labels (Branch t u) = labels t \<union> labels u"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   313
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   314
primrec swap where
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   315
"swap (Leaf c) a b =
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   316
 (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   317
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   318
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35078
diff changeset
   319
lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   320
(* nitpick *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   321
proof (induct t)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   322
  case Leaf thus ?case by simp
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   323
next
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   324
  case (Branch t u) thus ?case
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   325
  (* nitpick *)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   326
  nitpick [non_std, show_all, expect = genuine]
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   327
oops
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   328
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   329
lemma "labels (swap t a b) =
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   330
       (if a \<in> labels t then
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   331
          if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   332
        else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   333
          if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35284
diff changeset
   334
(* nitpick *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   335
proof (induct t)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   336
  case Leaf thus ?case by simp
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   337
next
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   338
  case (Branch t u) thus ?case
38184
6a221fffbc8a minor changes
blanchet
parents: 37477
diff changeset
   339
  nitpick [non_std, card = 1\<midarrow>4, expect = none]
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   340
  by auto
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   341
qed
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   342
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   343
section {* 4. Case Studies *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   344
36268
65aabc2c89ae use only one thread in "Manual_Nits";
blanchet
parents: 35747
diff changeset
   345
nitpick_params [max_potential = 0]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   346
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   347
subsection {* 4.1. A Context-Free Grammar *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   348
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   349
datatype alphabet = a | b
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   350
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   351
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   352
  "[] \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   353
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   354
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   355
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   356
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   357
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   358
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   359
theorem S\<^isub>1_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   360
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   361
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   362
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   363
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   364
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   365
  "[] \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   366
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   367
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   368
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   369
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   370
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   371
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   372
theorem S\<^isub>2_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   373
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   374
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   375
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   376
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   377
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   378
  "[] \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   379
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   380
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   381
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   382
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   383
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   384
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   385
theorem S\<^isub>3_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   386
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
   387
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   388
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   389
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   390
theorem S\<^isub>3_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   391
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   392
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   393
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   394
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   395
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   396
  "[] \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   397
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   398
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   399
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   400
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   401
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   402
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   403
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   404
theorem S\<^isub>4_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   405
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
   406
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   407
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   408
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   409
theorem S\<^isub>4_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   410
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
   411
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   412
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   413
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   414
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   415
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   416
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   417
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
37477
e482320bcbfe adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents: 36268
diff changeset
   418
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   419
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   420
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   421
subsection {* 4.2. AA Trees *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   422
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34126
diff changeset
   423
datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   424
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   425
primrec data where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   426
"data \<Lambda> = undefined" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   427
"data (N x _ _ _) = x"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   428
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   429
primrec dataset where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   430
"dataset \<Lambda> = {}" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   431
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   432
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   433
primrec level where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   434
"level \<Lambda> = 0" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   435
"level (N _ k _ _) = k"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   436
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   437
primrec left where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   438
"left \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   439
"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   440
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   441
primrec right where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   442
"right \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   443
"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   444
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   445
fun wf where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   446
"wf \<Lambda> = True" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   447
"wf (N _ k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   448
 (if t = \<Lambda> then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   449
    k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   450
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   451
    wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   452
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   453
fun skew where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   454
"skew \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   455
"skew (N x k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   456
 (if t \<noteq> \<Lambda> \<and> k = level t then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   457
    N (data t) k (left t) (N x k (right t) u)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   458
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   459
    N x k t u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   460
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   461
fun split where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   462
"split \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   463
"split (N x k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   464
 (if u \<noteq> \<Lambda> \<and> k = level (right u) then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   465
    N (data u) (Suc k) (N x k t (left u)) (right u)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   466
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   467
    N x k t u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   468
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   469
theorem dataset_skew_split:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   470
"dataset (skew t) = dataset t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   471
"dataset (split t) = dataset t"
35747
c910fe606829 make tests less demanding, to prevent sporadic failures
blanchet
parents: 35718
diff changeset
   472
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   473
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   474
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   475
theorem wf_skew_split:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   476
"wf t \<Longrightarrow> skew t = t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   477
"wf t \<Longrightarrow> split t = t"
35747
c910fe606829 make tests less demanding, to prevent sporadic failures
blanchet
parents: 35718
diff changeset
   478
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   479
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   480
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   481
primrec insort\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   482
"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   483
"insort\<^isub>1 (N y k t u) x =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   484
 (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   485
                             (if x > y then insort\<^isub>1 u x else u))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   486
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   487
theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   488
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   489
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   490
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   491
theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   492
nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   493
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   494
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   495
primrec insort\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   496
"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   497
"insort\<^isub>2 (N y k t u) x =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   498
 (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   499
                       (if x > y then insort\<^isub>2 u x else u))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   500
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   501
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
35747
c910fe606829 make tests less demanding, to prevent sporadic failures
blanchet
parents: 35718
diff changeset
   502
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   503
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   504
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   505
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
35747
c910fe606829 make tests less demanding, to prevent sporadic failures
blanchet
parents: 35718
diff changeset
   506
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   507
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   508
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   509
end