src/HOL/Nitpick.thy
author eberlm
Thu, 25 Feb 2016 16:44:53 +0100
changeset 62422 4aa35fd6c152
parent 61944 5d06ecfdb472
child 63882 018998c00003
permissions -rw-r--r--
Tuned Euclidean rings
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Nitpick.thy
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
35807
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35699
diff changeset
     3
    Copyright   2008, 2009, 2010
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     4
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     5
Nitpick: Yet another counterexample generator for Isabelle/HOL.
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     6
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     7
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     8
section \<open>Nitpick: Yet Another Counterexample Generator for Isabelle/HOL\<close>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    10
theory Nitpick
57242
25aff3b8d550 tuned dependencies
blanchet
parents: 57231
diff changeset
    11
imports Record
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55415
diff changeset
    12
keywords
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55415
diff changeset
    13
  "nitpick" :: diag and
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55415
diff changeset
    14
  "nitpick_params" :: thy_decl
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    15
begin
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    16
58350
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58335
diff changeset
    17
datatype (plugins only: extraction) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58335
diff changeset
    18
datatype (plugins only: extraction) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58335
diff changeset
    19
datatype (plugins only: extraction) (dead 'a) word = Word "'a set"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
57992
blanchet
parents: 57242
diff changeset
    21
typedecl bisim_iterator
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 33747
diff changeset
    22
typedecl unsigned_bit
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 33747
diff changeset
    23
typedecl signed_bit
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 33747
diff changeset
    24
57992
blanchet
parents: 57242
diff changeset
    25
consts
blanchet
parents: 57242
diff changeset
    26
  unknown :: 'a
blanchet
parents: 57242
diff changeset
    27
  is_unknown :: "'a \<Rightarrow> bool"
blanchet
parents: 57242
diff changeset
    28
  bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
blanchet
parents: 57242
diff changeset
    29
  bisim_iterator_max :: bisim_iterator
blanchet
parents: 57242
diff changeset
    30
  Quot :: "'a \<Rightarrow> 'b"
blanchet
parents: 57242
diff changeset
    31
  safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    32
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    33
text \<open>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    34
Alternative definitions.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    35
\<close>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    36
57992
blanchet
parents: 57242
diff changeset
    37
lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
blanchet
parents: 57242
diff changeset
    38
  apply (rule eq_reflection)
blanchet
parents: 57242
diff changeset
    39
  apply (simp add: Ex1_def set_eq_iff)
blanchet
parents: 57242
diff changeset
    40
  apply (rule iffI)
blanchet
parents: 57242
diff changeset
    41
   apply (erule exE)
blanchet
parents: 57242
diff changeset
    42
   apply (erule conjE)
blanchet
parents: 57242
diff changeset
    43
   apply (rule_tac x = x in exI)
blanchet
parents: 57242
diff changeset
    44
   apply (rule allI)
blanchet
parents: 57242
diff changeset
    45
   apply (rename_tac y)
blanchet
parents: 57242
diff changeset
    46
   apply (erule_tac x = y in allE)
blanchet
parents: 57242
diff changeset
    47
  by auto
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    48
57992
blanchet
parents: 57242
diff changeset
    49
lemma rtrancl_unfold[nitpick_unfold]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
45140
339a8b3c4791 bouned transitive closure
haftmann
parents: 44278
diff changeset
    50
  by (simp only: rtrancl_trancl_reflcl)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    51
57992
blanchet
parents: 57242
diff changeset
    52
lemma rtranclp_unfold[nitpick_unfold]: "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
blanchet
parents: 57242
diff changeset
    53
  by (rule eq_reflection) (auto dest: rtranclpD)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    54
57992
blanchet
parents: 57242
diff changeset
    55
lemma tranclp_unfold[nitpick_unfold]:
blanchet
parents: 57242
diff changeset
    56
  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
blanchet
parents: 57242
diff changeset
    57
  by (simp add: trancl_def)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    58
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 52641
diff changeset
    59
lemma [nitpick_simp]:
57992
blanchet
parents: 57242
diff changeset
    60
  "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
blanchet
parents: 57242
diff changeset
    61
  by (cases n) auto
47909
5f1afeebafbc fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents: 46950
diff changeset
    62
41046
f2e94005d283 fix special handling of set products
blanchet
parents: 39365
diff changeset
    63
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
57992
blanchet
parents: 57242
diff changeset
    64
  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
41046
f2e94005d283 fix special handling of set products
blanchet
parents: 39365
diff changeset
    65
44278
1220ecb81e8f observe distinction between sets and predicates more properly
haftmann
parents: 44016
diff changeset
    66
definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
57992
blanchet
parents: 57242
diff changeset
    67
  "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
44278
1220ecb81e8f observe distinction between sets and predicates more properly
haftmann
parents: 44016
diff changeset
    69
definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
57992
blanchet
parents: 57242
diff changeset
    70
  "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    71
44278
1220ecb81e8f observe distinction between sets and predicates more properly
haftmann
parents: 44016
diff changeset
    72
definition card' :: "'a set \<Rightarrow> nat" where
57992
blanchet
parents: 57242
diff changeset
    73
  "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    74
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
    75
definition setsum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
57992
blanchet
parents: 57242
diff changeset
    76
  "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    77
44278
1220ecb81e8f observe distinction between sets and predicates more properly
haftmann
parents: 44016
diff changeset
    78
inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
57992
blanchet
parents: 57242
diff changeset
    79
  "fold_graph' f z {} z" |
blanchet
parents: 57242
diff changeset
    80
  "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    81
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    82
text \<open>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    83
The following lemmas are not strictly necessary but they help the
47909
5f1afeebafbc fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents: 46950
diff changeset
    84
\textit{specialize} optimization.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    85
\<close>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    86
57992
blanchet
parents: 57242
diff changeset
    87
lemma The_psimp[nitpick_psimp]: "P = (op =) x \<Longrightarrow> The P = x"
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45140
diff changeset
    88
  by auto
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    89
57992
blanchet
parents: 57242
diff changeset
    90
lemma Eps_psimp[nitpick_psimp]:
blanchet
parents: 57242
diff changeset
    91
  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
blanchet
parents: 57242
diff changeset
    92
  apply (cases "P (Eps P)")
blanchet
parents: 57242
diff changeset
    93
   apply auto
blanchet
parents: 57242
diff changeset
    94
  apply (erule contrapos_np)
blanchet
parents: 57242
diff changeset
    95
  by (rule someI)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    96
57992
blanchet
parents: 57242
diff changeset
    97
lemma case_unit_unfold[nitpick_unfold]:
blanchet
parents: 57242
diff changeset
    98
  "case_unit x u \<equiv> x"
blanchet
parents: 57242
diff changeset
    99
  apply (subgoal_tac "u = ()")
blanchet
parents: 57242
diff changeset
   100
   apply (simp only: unit.case)
blanchet
parents: 57242
diff changeset
   101
  by simp
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   102
57992
blanchet
parents: 57242
diff changeset
   103
declare unit.case[nitpick_simp del]
33556
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33192
diff changeset
   104
57992
blanchet
parents: 57242
diff changeset
   105
lemma case_nat_unfold[nitpick_unfold]:
blanchet
parents: 57242
diff changeset
   106
  "case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
blanchet
parents: 57242
diff changeset
   107
  apply (rule eq_reflection)
blanchet
parents: 57242
diff changeset
   108
  by (cases n) auto
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
57992
blanchet
parents: 57242
diff changeset
   110
declare nat.case[nitpick_simp del]
33556
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33192
diff changeset
   111
57992
blanchet
parents: 57242
diff changeset
   112
lemma size_list_simp[nitpick_simp]:
blanchet
parents: 57242
diff changeset
   113
  "size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
blanchet
parents: 57242
diff changeset
   114
  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
blanchet
parents: 57242
diff changeset
   115
  by (cases xs) auto
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   116
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   117
text \<open>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   118
Auxiliary definitions used to provide an alternative representation for
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61681
diff changeset
   119
\<open>rat\<close> and \<open>real\<close>.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   120
\<close>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   122
function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
57992
blanchet
parents: 57242
diff changeset
   123
  "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
blanchet
parents: 57242
diff changeset
   124
  by auto
61944
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
   125
termination
57992
blanchet
parents: 57242
diff changeset
   126
  apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
blanchet
parents: 57242
diff changeset
   127
   apply auto
blanchet
parents: 57242
diff changeset
   128
   apply (metis mod_less_divisor xt1(9))
61944
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
   129
  apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
   130
  done
57992
blanchet
parents: 57242
diff changeset
   131
blanchet
parents: 57242
diff changeset
   132
declare nat_gcd.simps[simp del]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   133
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   134
definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
57992
blanchet
parents: 57242
diff changeset
   135
  "nat_lcm x y = x * y div (nat_gcd x y)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   136
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where
61944
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
   138
  "int_gcd x y = int (nat_gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   139
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   140
definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
61944
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
   141
  "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   142
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
definition Frac :: "int \<times> int \<Rightarrow> bool" where
57992
blanchet
parents: 57242
diff changeset
   144
  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   145
57992
blanchet
parents: 57242
diff changeset
   146
consts
blanchet
parents: 57242
diff changeset
   147
  Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
56643
41d3596d8a64 move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents: 55642
diff changeset
   148
  Rep_Frac :: "'a \<Rightarrow> int \<times> int"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   149
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   150
definition zero_frac :: 'a where
57992
blanchet
parents: 57242
diff changeset
   151
  "zero_frac \<equiv> Abs_Frac (0, 1)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   152
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   153
definition one_frac :: 'a where
57992
blanchet
parents: 57242
diff changeset
   154
  "one_frac \<equiv> Abs_Frac (1, 1)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   155
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   156
definition num :: "'a \<Rightarrow> int" where
57992
blanchet
parents: 57242
diff changeset
   157
  "num \<equiv> fst o Rep_Frac"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   158
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   159
definition denom :: "'a \<Rightarrow> int" where
57992
blanchet
parents: 57242
diff changeset
   160
  "denom \<equiv> snd o Rep_Frac"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   161
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   162
function norm_frac :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
57992
blanchet
parents: 57242
diff changeset
   163
  "norm_frac a b =
blanchet
parents: 57242
diff changeset
   164
    (if b < 0 then norm_frac (- a) (- b)
blanchet
parents: 57242
diff changeset
   165
     else if a = 0 \<or> b = 0 then (0, 1)
blanchet
parents: 57242
diff changeset
   166
     else let c = int_gcd a b in (a div c, b div c))"
blanchet
parents: 57242
diff changeset
   167
  by pat_completeness auto
blanchet
parents: 57242
diff changeset
   168
  termination by (relation "measure (\<lambda>(_, b). if b < 0 then 1 else 0)") auto
blanchet
parents: 57242
diff changeset
   169
blanchet
parents: 57242
diff changeset
   170
declare norm_frac.simps[simp del]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   171
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   172
definition frac :: "int \<Rightarrow> int \<Rightarrow> 'a" where
57992
blanchet
parents: 57242
diff changeset
   173
  "frac a b \<equiv> Abs_Frac (norm_frac a b)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   175
definition plus_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
57992
blanchet
parents: 57242
diff changeset
   176
  [nitpick_simp]: "plus_frac q r = (let d = int_lcm (denom q) (denom r) in
blanchet
parents: 57242
diff changeset
   177
    frac (num q * (d div denom q) + num r * (d div denom r)) d)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
definition times_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
57992
blanchet
parents: 57242
diff changeset
   180
  [nitpick_simp]: "times_frac q r = frac (num q * num r) (denom q * denom r)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   181
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   182
definition uminus_frac :: "'a \<Rightarrow> 'a" where
57992
blanchet
parents: 57242
diff changeset
   183
  "uminus_frac q \<equiv> Abs_Frac (- num q, denom q)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   184
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   185
definition number_of_frac :: "int \<Rightarrow> 'a" where
57992
blanchet
parents: 57242
diff changeset
   186
  "number_of_frac n \<equiv> Abs_Frac (n, 1)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   187
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   188
definition inverse_frac :: "'a \<Rightarrow> 'a" where
57992
blanchet
parents: 57242
diff changeset
   189
  "inverse_frac q \<equiv> frac (denom q) (num q)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   190
37397
18000f9d783e adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents: 37213
diff changeset
   191
definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
57992
blanchet
parents: 57242
diff changeset
   192
  [nitpick_simp]: "less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
37397
18000f9d783e adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents: 37213
diff changeset
   193
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   194
definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
57992
blanchet
parents: 57242
diff changeset
   195
  [nitpick_simp]: "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   196
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   197
definition of_frac :: "'a \<Rightarrow> 'b::{inverse,ring_1}" where
57992
blanchet
parents: 57242
diff changeset
   198
  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   199
55017
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   200
axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   201
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   202
definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
57992
blanchet
parents: 57242
diff changeset
   203
  [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
55017
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   204
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   205
definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
57992
blanchet
parents: 57242
diff changeset
   206
  "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x else THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y"
55017
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   207
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   208
ML_file "Tools/Nitpick/kodkod.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   209
ML_file "Tools/Nitpick/kodkod_sat.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   210
ML_file "Tools/Nitpick/nitpick_util.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   211
ML_file "Tools/Nitpick/nitpick_hol.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   212
ML_file "Tools/Nitpick/nitpick_mono.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   213
ML_file "Tools/Nitpick/nitpick_preproc.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   214
ML_file "Tools/Nitpick/nitpick_scope.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   215
ML_file "Tools/Nitpick/nitpick_peephole.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   216
ML_file "Tools/Nitpick/nitpick_rep.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   217
ML_file "Tools/Nitpick/nitpick_nut.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   218
ML_file "Tools/Nitpick/nitpick_kodkod.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   219
ML_file "Tools/Nitpick/nitpick_model.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   220
ML_file "Tools/Nitpick/nitpick.ML"
55199
ba93ef2c0d27 tuned ML file name
blanchet
parents: 55082
diff changeset
   221
ML_file "Tools/Nitpick/nitpick_commands.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47988
diff changeset
   222
ML_file "Tools/Nitpick/nitpick_tests.ML"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   224
setup \<open>
44016
51184010c609 replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents: 44013
diff changeset
   225
  Nitpick_HOL.register_ersatz_global
51184010c609 replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents: 44013
diff changeset
   226
    [(@{const_name card}, @{const_name card'}),
51184010c609 replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents: 44013
diff changeset
   227
     (@{const_name setsum}, @{const_name setsum'}),
51184010c609 replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents: 44013
diff changeset
   228
     (@{const_name fold_graph}, @{const_name fold_graph'}),
55017
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   229
     (@{const_name wf}, @{const_name wf'}),
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   230
     (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
2df6ad1dbd66 adapted to move of Wfrec
blanchet
parents: 54555
diff changeset
   231
     (@{const_name wfrec}, @{const_name wfrec'})]
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   232
\<close>
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 33556
diff changeset
   233
57992
blanchet
parents: 57242
diff changeset
   234
hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod
blanchet
parents: 57242
diff changeset
   235
  refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
blanchet
parents: 57242
diff changeset
   236
  zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac
blanchet
parents: 57242
diff changeset
   237
  inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec'
blanchet
parents: 57242
diff changeset
   238
46324
e4bccf5ec61e added problem importer
blanchet
parents: 46319
diff changeset
   239
hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
57992
blanchet
parents: 57242
diff changeset
   240
blanchet
parents: 57242
diff changeset
   241
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
61681
ca53150406c9 option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents: 61121
diff changeset
   242
  card'_def setsum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
61121
efe8b18306b7 do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents: 61076
diff changeset
   243
  size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
efe8b18306b7 do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents: 61076
diff changeset
   244
  num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
57992
blanchet
parents: 57242
diff changeset
   245
  number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
blanchet
parents: 57242
diff changeset
   246
  wfrec'_def
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   247
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   248
end