src/HOL/Nitpick_Examples/Manual_Nits.thy
author blanchet
Thu, 11 Mar 2010 12:22:11 +0100
changeset 35711 548d3f16404b
parent 35710 58acd48904bc
child 35712 77aa29bf14ee
permissions -rw-r--r--
added term postprocessor to Nitpick, to provide custom syntax for typedefs
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
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    10
theory Manual_Nits
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
    11
imports Main Quotient_Product RealDef
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    12
begin
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    13
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    14
chapter {* 3. First Steps *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    15
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
    16
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
33197
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
subsection {* 3.1. Propositional Logic *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    19
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    20
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
    21
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    22
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
    23
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
    24
nitpick [expect = genuine] 2
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    25
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    26
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    27
subsection {* 3.2. Type Variables *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    28
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    29
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
    30
nitpick [verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    31
oops
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
subsection {* 3.3. Constants *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    34
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    35
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
    36
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
    37
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
    38
nitpick [dont_specialize, full_descrs, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    39
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    40
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    41
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
    42
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
    43
nitpick [card 'a = 1\<midarrow>50, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    44
(* sledgehammer *)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    45
apply (metis the_equality)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    46
done
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    47
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    48
subsection {* 3.4. Skolemization *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    49
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    50
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
    51
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    52
oops
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>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
    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 "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
    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
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 33197
diff changeset
    62
subsection {* 3.5. Natural Numbers and Integers *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    63
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    64
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
    65
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    66
oops
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 "\<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
    69
nitpick [card nat = 100, check_potential, 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 "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
    73
nitpick [expect = none]
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 (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
    77
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
    78
nitpick [card nat = 2, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    79
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    80
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    81
subsection {* 3.6. Inductive Datatypes *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    82
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    83
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
    84
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
    85
nitpick [show_consts, show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    86
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    87
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    88
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
    89
nitpick [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
subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    93
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    94
typedef three = "{0\<Colon>nat, 1, 2}"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    95
by blast
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    96
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    97
definition A :: three where "A \<equiv> Abs_three 0"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    98
definition B :: three where "B \<equiv> Abs_three 1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    99
definition C :: three where "C \<equiv> Abs_three 2"
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
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
   102
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   103
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   104
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   105
fun my_int_rel where
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   106
"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
   107
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   108
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
   109
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
   110
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   111
definition add_raw where
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   112
"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
   113
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   114
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
   115
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   116
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
   117
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
   118
oops
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35185
diff changeset
   119
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   120
ML {*
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   121
(* Proof.context -> typ -> term -> term *)
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   122
fun my_int_postproc _ T (Const _ $ (Const _ $ t1 $ t2)) =
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   123
    HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2))
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   124
  | my_int_postproc _ _ t = t
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   125
*}
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   126
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   127
setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   128
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   129
lemma "add x y = add x x"
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   130
nitpick [show_datatypes]
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   131
oops
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35710
diff changeset
   132
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   133
record point =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   134
  Xcoord :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   135
  Ycoord :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   136
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   137
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
   138
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   139
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   140
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   141
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
   142
nitpick [show_datatypes, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   143
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   144
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   145
subsection {* 3.8. Inductive and Coinductive Predicates *}
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
inductive even where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   148
"even 0" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   149
"even n \<Longrightarrow> even (Suc (Suc n))"
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
lemma "\<exists>n. even n \<and> even (Suc n)"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   152
nitpick [card nat = 50, unary_ints, verbose, expect = potential]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   153
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   154
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   155
lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   156
nitpick [card nat = 50, unary_ints, verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   157
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   158
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   159
inductive even' where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   160
"even' (0\<Colon>nat)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   161
"even' 2" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   162
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   163
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   164
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
   165
nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   166
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   167
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   168
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
   169
nitpick [card nat = 10, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   170
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   171
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   172
coinductive nats where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   173
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   174
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   175
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
   176
nitpick [card nat = 10, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   177
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   178
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   179
inductive odd where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   180
"odd 1" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   181
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   182
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   183
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
   184
nitpick [card nat = 10, show_consts, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   185
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   186
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   187
subsection {* 3.9. Coinductive Datatypes *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   188
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   189
(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   190
we cannot rely on its presence, we expediently provide our own axiomatization.
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   191
The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   192
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   193
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
   194
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
   195
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
   196
"LNil = Abs_llist (Inl [])"
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   197
definition LCons where
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   198
"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
   199
                           Inl ys' \<Rightarrow> Inl (y # ys')
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   200
                         | 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
   201
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   202
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
   203
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   204
lemma iterates_def [nitpick_simp]:
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   205
"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
   206
sorry
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   207
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   208
setup {*
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   209
Nitpick.register_codatatype @{typ "'a llist"} ""
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   210
    (map dest_Const [@{term LNil}, @{term LCons}])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   211
*}
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35312
diff changeset
   212
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   213
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
   214
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   215
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   216
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   217
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
   218
nitpick [verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   219
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   220
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   221
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
   222
nitpick [bisim_depth = -1, show_datatypes, expect = quasi_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
   223
nitpick [expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   224
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   225
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   226
subsection {* 3.10. Boxing *}
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
datatype tm = Var nat | Lam tm | App tm tm
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   229
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   230
primrec lift where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   231
"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
   232
"lift (Lam t) k = Lam (lift t (k + 1))" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   233
"lift (App t u) k = App (lift t k) (lift u k)"
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
primrec loose where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   236
"loose (Var j) k = (j \<ge> k)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   237
"loose (Lam t) k = loose t (Suc k)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   238
"loose (App t u) k = (loose t k \<or> loose u k)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   239
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   240
primrec subst\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   241
"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   242
"subst\<^isub>1 \<sigma> (Lam t) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   243
 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
   244
"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
   245
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   246
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
   247
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
   248
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
   249
(* nitpick [dont_box, expect = unknown] *)
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   250
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   251
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   252
primrec subst\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   253
"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   254
"subst\<^isub>2 \<sigma> (Lam t) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   255
 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
   256
"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
   257
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   258
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
   259
nitpick [card = 1\<midarrow>5, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   260
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   261
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   262
subsection {* 3.11. Scope Monotonicity *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   263
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   264
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
   265
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
   266
nitpick [card = 8, verbose, expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   267
oops
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
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
   270
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
   271
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   272
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   273
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
   274
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
   275
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
   276
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
   277
"(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
   278
"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
   279
"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
   280
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
lemma "n \<in> reach \<Longrightarrow> 2 dvd 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
   282
nitpick [unary_ints, 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
   283
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
   284
  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
   285
 nitpick [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
   286
 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
   287
 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
   288
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
   289
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
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
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
   291
nitpick [unary_ints, 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 (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
   293
  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
   294
 nitpick [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
   295
 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
   296
 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
   297
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
   298
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
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
   300
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
   301
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
   302
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
   303
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
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
   305
"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
   306
"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
   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
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
   309
"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
   310
 (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
   311
"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
   312
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35078
diff changeset
   313
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
   314
(* 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
   315
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
   316
  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
   317
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
   318
  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
   319
  (* 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
   320
  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
   321
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
   322
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
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
   324
       (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
   325
          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
   326
        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
   327
          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
   328
(* 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
   329
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
   330
  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
   331
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
   332
  case (Branch t u) thus ?case
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   333
  nitpick [non_std, card = 1\<midarrow>5, 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
   334
  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
   335
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
   336
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   337
section {* 4. Case Studies *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   338
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   339
nitpick_params [max_potential = 0, max_threads = 2]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   340
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   341
subsection {* 4.1. A Context-Free Grammar *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   342
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   343
datatype alphabet = a | b
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   344
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   345
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
   346
  "[] \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   347
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   348
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   349
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   350
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   351
| "\<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
   352
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   353
theorem S\<^isub>1_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   354
"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
   355
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   356
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   357
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   358
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
   359
  "[] \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   360
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   361
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   362
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   363
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   364
| "\<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
   365
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   366
theorem S\<^isub>2_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   367
"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
   368
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   369
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   370
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   371
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
   372
  "[] \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   373
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   374
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   375
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   376
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   377
| "\<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
   378
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   379
theorem S\<^isub>3_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   380
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   381
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   382
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   383
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   384
theorem S\<^isub>3_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   385
"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
   386
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   387
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   388
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   389
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
   390
  "[] \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   391
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   392
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   393
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   394
| "\<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
   395
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   396
| "\<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
   397
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   398
theorem S\<^isub>4_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   399
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   400
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   401
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   402
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   403
theorem S\<^isub>4_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   404
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   405
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   406
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   407
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   408
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
   409
"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
   410
"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
   411
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   412
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   413
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   414
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   415
subsection {* 4.2. AA Trees *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   416
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
   417
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
   418
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   419
primrec data where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   420
"data \<Lambda> = undefined" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   421
"data (N x _ _ _) = x"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   422
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   423
primrec dataset where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   424
"dataset \<Lambda> = {}" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   425
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   426
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   427
primrec level where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   428
"level \<Lambda> = 0" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   429
"level (N _ k _ _) = k"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   430
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   431
primrec left where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   432
"left \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   433
"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   434
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   435
primrec right where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   436
"right \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   437
"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   438
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   439
fun wf where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   440
"wf \<Lambda> = True" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   441
"wf (N _ k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   442
 (if t = \<Lambda> then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   443
    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
   444
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   445
    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
   446
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   447
fun skew where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   448
"skew \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   449
"skew (N x k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   450
 (if t \<noteq> \<Lambda> \<and> k = level t then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   451
    N (data t) k (left t) (N x k (right t) u)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   452
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   453
    N x k t u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   454
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   455
fun split where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   456
"split \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   457
"split (N x k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   458
 (if u \<noteq> \<Lambda> \<and> k = level (right u) then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   459
    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
   460
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   461
    N x k t u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   462
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   463
theorem dataset_skew_split:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   464
"dataset (skew t) = dataset t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   465
"dataset (split t) = dataset t"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   466
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   467
sorry
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 wf_skew_split:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   470
"wf t \<Longrightarrow> skew t = t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   471
"wf t \<Longrightarrow> split t = t"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   472
nitpick [card = 1\<midarrow>6, 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
primrec insort\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   476
"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   477
"insort\<^isub>1 (N y k t u) x =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   478
 (* (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
   479
                             (if x > y then insort\<^isub>1 u x else u))"
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
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
   482
nitpick [expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   483
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   484
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   485
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
   486
nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   487
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   488
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   489
primrec insort\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   490
"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   491
"insort\<^isub>2 (N y k t u) x =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   492
 (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
   493
                       (if x > y then insort\<^isub>2 u x else u))"
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
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   496
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   497
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   498
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   499
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35671
diff changeset
   500
nitpick [card = 1\<midarrow>6, expect = none]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   501
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   502
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   503
end