src/HOL/Nitpick_Examples/Manual_Nits.thy
author blanchet
Fri, 05 Feb 2010 14:27:21 +0100
changeset 35076 cc19e2aef17e
parent 34982 7b8c366e34a2
child 35078 6fd1052fe463
permissions -rw-r--r--
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
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
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    11
imports Main Coinductive_List RealDef
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
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    16
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    21
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    22
apply auto
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    23
nitpick 1
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    24
nitpick 2
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)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    30
nitpick [verbose]
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)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    36
nitpick [show_consts]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    37
nitpick [full_descrs, show_consts]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    38
nitpick [dont_specialize, full_descrs, show_consts]
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)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    42
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    43
nitpick [card 'a = 1-50]
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    51
nitpick
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    55
nitpick
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    59
nitpick
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    65
nitpick
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    69
nitpick [card nat = 100, check_potential]
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    73
nitpick [card = 1-6]
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)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    77
nitpick [card nat = 1]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    78
nitpick [card nat = 2]
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    84
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    85
nitpick [show_consts, show_datatypes]
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    89
nitpick [show_datatypes]
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"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   102
nitpick [show_datatypes]
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
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   105
record point =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   106
  Xcoord :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   107
  Ycoord :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   108
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   109
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   110
nitpick [show_datatypes]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   111
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   112
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   113
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   114
nitpick [show_datatypes]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   115
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   116
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   117
subsection {* 3.8. Inductive and Coinductive Predicates *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   118
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   119
inductive even where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   120
"even 0" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   121
"even n \<Longrightarrow> even (Suc (Suc n))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   122
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   123
lemma "\<exists>n. even n \<and> even (Suc n)"
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 33197
diff changeset
   124
nitpick [card nat = 100, unary_ints, verbose]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   125
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   126
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   127
lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 33197
diff changeset
   128
nitpick [card nat = 100, unary_ints, verbose]
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   129
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   130
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   131
inductive even' where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   132
"even' (0\<Colon>nat)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   133
"even' 2" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   134
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   135
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   136
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 33197
diff changeset
   137
nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   138
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   139
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   140
lemma "even' (n - 2) \<Longrightarrow> even' n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   141
nitpick [card nat = 10, show_consts]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   142
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   143
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   144
coinductive nats where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   145
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
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 "nats = {0, 1, 2, 3, 4}"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   148
nitpick [card nat = 10, show_consts]
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
inductive odd where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   152
"odd 1" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   153
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   154
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   155
lemma "odd n \<Longrightarrow> odd (n - 2)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   156
nitpick [card nat = 10, show_consts]
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
subsection {* 3.9. Coinductive Datatypes *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   160
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   161
lemma "xs \<noteq> LCons a xs"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   162
nitpick
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
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   166
nitpick [verbose]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   167
nitpick [bisim_depth = -1, verbose]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   168
oops
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 "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   171
nitpick [bisim_depth = -1, show_datatypes]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   172
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   173
sorry
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
subsection {* 3.10. Boxing *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   176
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   177
datatype tm = Var nat | Lam tm | App tm tm
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
primrec lift where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   180
"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
   181
"lift (Lam t) k = Lam (lift t (k + 1))" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   182
"lift (App t u) k = App (lift t k) (lift u k)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   183
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   184
primrec loose where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   185
"loose (Var j) k = (j \<ge> k)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   186
"loose (Lam t) k = loose t (Suc k)" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   187
"loose (App t u) k = (loose t k \<or> loose u k)"
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
primrec subst\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   190
"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   191
"subst\<^isub>1 \<sigma> (Lam t) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   192
 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
   193
"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
   194
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   195
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   196
nitpick [verbose]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   197
nitpick [eval = "subst\<^isub>1 \<sigma> t"]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   198
nitpick [dont_box]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   199
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   200
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   201
primrec subst\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   202
"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   203
"subst\<^isub>2 \<sigma> (Lam t) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   204
 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
   205
"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
   206
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   207
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   208
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   209
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   210
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   211
subsection {* 3.11. Scope Monotonicity *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   212
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   213
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   214
nitpick [verbose]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   215
nitpick [card = 8, verbose]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   216
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   217
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   218
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   219
nitpick [mono]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   220
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   221
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   222
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
   223
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
   224
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
   225
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
   226
"(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
   227
"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
   228
"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
   229
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
   230
lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
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
   231
nitpick
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
   232
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
   233
  apply 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
   234
 nitpick
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
   235
 apply (thin_tac "n \<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
   236
 nitpick
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
   237
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
   238
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
   239
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
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
   240
nitpick
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
   241
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
   242
  apply 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
   243
 nitpick
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
   244
 apply (thin_tac "n \<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
   245
 nitpick
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
   246
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
   247
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
   248
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
   249
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
   250
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
   251
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
   252
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
   253
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
   254
"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
   255
"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
   256
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
   257
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
   258
"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
   259
 (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
   260
"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
   261
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
   262
lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels 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
   263
nitpick
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
   264
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
   265
  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
   266
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
   267
  case (Branch t u) thus ?case
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
   268
  nitpick
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
   269
  nitpick [non_std "'a bin_tree", show_consts]
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
   270
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
   271
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
   272
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
   273
       (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
   274
          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
   275
        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
   276
          if b \<in> labels t then (labels t - {b}) \<union> {a} else labels 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
   277
nitpick
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
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
   279
  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
   280
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
   281
  case (Branch t u) thus ?case
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
  nitpick [non_std "'a bin_tree", show_consts]
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
  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
   284
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
   285
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   286
section {* 4. Case Studies *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   287
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   288
nitpick_params [max_potential = 0, max_threads = 2]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   289
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   290
subsection {* 4.1. A Context-Free Grammar *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   291
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   292
datatype alphabet = a | b
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   293
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   294
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
   295
  "[] \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   296
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   297
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   298
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   299
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   300
| "\<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
   301
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   302
theorem S\<^isub>1_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   303
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   304
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   305
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   306
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   307
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
   308
  "[] \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   309
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   310
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   311
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   312
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   313
| "\<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
   314
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   315
theorem S\<^isub>2_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   316
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   317
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   318
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   319
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   320
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
   321
  "[] \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   322
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   323
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   324
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   325
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   326
| "\<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
   327
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   328
theorem S\<^isub>3_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   329
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   330
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   331
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   332
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   333
theorem S\<^isub>3_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   334
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   335
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   336
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   337
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   338
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
   339
  "[] \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   340
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   341
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   342
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   343
| "\<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
   344
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   345
| "\<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
   346
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   347
theorem S\<^isub>4_sound:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   348
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   349
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   350
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   351
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   352
theorem S\<^isub>4_complete:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   353
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   354
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   355
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   356
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   357
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
   358
"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
   359
"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
   360
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   361
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   362
sorry
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
subsection {* 4.2. AA Trees *}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   365
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
   366
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
   367
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   368
primrec data where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   369
"data \<Lambda> = undefined" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   370
"data (N x _ _ _) = x"
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
primrec dataset where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   373
"dataset \<Lambda> = {}" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   374
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   375
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   376
primrec level where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   377
"level \<Lambda> = 0" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   378
"level (N _ k _ _) = k"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   379
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   380
primrec left where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   381
"left \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   382
"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
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
primrec right where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   385
"right \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   386
"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   387
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   388
fun wf where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   389
"wf \<Lambda> = True" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   390
"wf (N _ k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   391
 (if t = \<Lambda> then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   392
    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
   393
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   394
    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
   395
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   396
fun skew where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   397
"skew \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   398
"skew (N x k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   399
 (if t \<noteq> \<Lambda> \<and> k = level t then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   400
    N (data t) k (left t) (N x k (right t) u)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   401
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   402
    N x k t u)"
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
fun split where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   405
"split \<Lambda> = \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   406
"split (N x k t u) =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   407
 (if u \<noteq> \<Lambda> \<and> k = level (right u) then
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   408
    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
   409
  else
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   410
    N x k t u)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   411
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   412
theorem dataset_skew_split:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   413
"dataset (skew t) = dataset t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   414
"dataset (split t) = dataset t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   415
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   416
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   417
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   418
theorem wf_skew_split:
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   419
"wf t \<Longrightarrow> skew t = t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   420
"wf t \<Longrightarrow> split t = t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   421
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   422
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   423
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   424
primrec insort\<^isub>1 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   425
"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   426
"insort\<^isub>1 (N y k t u) x =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   427
 (* (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
   428
                             (if x > y then insort\<^isub>1 u x else u))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   429
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   430
theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   431
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   432
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   433
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   434
theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   435
nitpick [eval = "insort\<^isub>1 t x"]
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   436
oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   437
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   438
primrec insort\<^isub>2 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   439
"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   440
"insort\<^isub>2 (N y k t u) x =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   441
 (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
   442
                       (if x > y then insort\<^isub>2 u x else u))"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   443
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   444
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   445
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   446
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   447
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   448
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   449
nitpick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   450
sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   451
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   452
end