Quelle Nitpick.thy Sprache: Isabelle

(*  Title:      HOL/Nitpick.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2008, 2009, 2010

Nitpick: Yet another counterexample generator for Isabelle/HOL.
*)

section \<open>Nitpick: Yet Another Counterexample Generator for Isabelle/HOL\<close>

theory Nitpick
imports Record GCD
keywords
  "nitpick" :: diag and
  "nitpick_params" :: thy_decl
begin

datatype (plugins only: extraction) (dead 'a, dead 'b) fun_box = FunBox "'a \ 'b"
datatype (plugins only: extraction) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
datatype (plugins only: extraction) (dead 'a) word = Word "'a set"

typedecl bisim_iterator
typedecl unsigned_bit
typedecl signed_bit

consts
  unknown :: 'a
  is_unknown :: "'a \ bool"
  bisim :: "bisim_iterator \ 'a \ 'a \ bool"
  bisim_iterator_max :: bisim_iterator
  Quot :: "'a \ 'b"
  safe_The :: "('a \ bool) \ 'a"

text \<open>
Alternative definitions.
\<close>

lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \ \x. {x. P x} = {x}"
  apply (rule eq_reflection)
  apply (simp add: Ex1_def set_eq_iff)
  apply (rule iffI)
   apply (erule exE)
   apply (erule conjE)
   apply (rule_tac x = x in exI)
   apply (rule allI)
   apply (rename_tac y)
   apply (erule_tac x = y in allE)
  by auto

lemma rtrancl_unfold[nitpick_unfold]: "r\<^sup>* \ (r\<^sup>+)\<^sup>="
  by (simp only: rtrancl_trancl_reflcl)

lemma rtranclp_unfold[nitpick_unfold]: "rtranclp r a b \ (a = b \ tranclp r a b)"
  by (rule eq_reflection) (auto dest: rtranclpD)

lemma tranclp_unfold[nitpick_unfold]:
  "tranclp r a b \ (a, b) \ trancl {(x, y). r x y}"
  by (simp add: trancl_def)

lemma [nitpick_simp]:
  "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
  by (cases n) auto

definition prod :: "'a set \ 'b set \ ('a \ 'b) set" where
  "prod A B = {(a, b). a \ A \ b \ B}"

definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
  "refl' r \ \x. (x, x) \ r"

definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
  "wf' r \ acyclic r \ (finite r \ unknown)"

definition card' :: "'a set \<Rightarrow> nat" where
  "card' A \ if finite A then length (SOME xs. set xs = A \ distinct xs) else 0"

definition sum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
  "sum' f A \ if finite A then sum_list (map f (SOME xs. set xs = A \ distinct xs)) else 0"

inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
  "fold_graph' f z {} z" |
  "\x \ A; fold_graph' f z (A - {x}) y\ \ fold_graph' f z A (f x y)"

text \<open>
The following lemmas are not strictly necessary but they help the
\textit{specialize} optimization.
\<close>

lemma The_psimp[nitpick_psimp]: "P = (=) x \ The P = x"
  by auto

lemma Eps_psimp[nitpick_psimp]:
  "\P x; \ P y; Eps P = y\ \ Eps P = x"
  apply (cases "P (Eps P)")
   apply auto
  apply (erule contrapos_np)
  by (rule someI)

lemma case_unit_unfold[nitpick_unfold]:
  "case_unit x u \ x"
  apply (subgoal_tac "u = ()")
   apply (simp only: unit.case)
  by simp

declare unit.case[nitpick_simp del]

lemma case_nat_unfold[nitpick_unfold]:
  "case_nat x f n \ if n = 0 then x else f (n - 1)"
  apply (rule eq_reflection)
  by (cases n) auto

declare nat.case[nitpick_simp del]

lemma size_list_simp[nitpick_simp]:
  "size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
  by (cases xs) auto

text \<open>
Auxiliary definitions used to provide an alternative representation for
\<open>rat\<close> and \<open>real\<close>.
\<close>

fun nat_gcd :: "nat \ nat \ nat" where
  "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"

declare nat_gcd.simps [simp del]

definition nat_lcm :: "nat \ nat \ nat" where
  "nat_lcm x y = x * y div (nat_gcd x y)"

lemma gcd_eq_nitpick_gcd [nitpick_unfold]:
  "gcd x y = Nitpick.nat_gcd x y"
  by (induct x y rule: nat_gcd.induct)
    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)

lemma lcm_eq_nitpick_lcm [nitpick_unfold]:
  "lcm x y = Nitpick.nat_lcm x y"
  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)

definition Frac :: "int \ int \ bool" where
  "Frac \ \(a, b). b > 0 \ coprime a b"

consts
  Abs_Frac :: "int \ int \ 'a"
  Rep_Frac :: "'a \ int \ int"

definition zero_frac :: 'a where
  "zero_frac \ Abs_Frac (0, 1)"

definition one_frac :: 'a where
  "one_frac \ Abs_Frac (1, 1)"

definition num :: "'a \ int" where
  "num \ fst \ Rep_Frac"

definition denom :: "'a \ int" where
  "denom \ snd \ Rep_Frac"

function norm_frac :: "int \ int \ int \ int" where
  "norm_frac a b =
    (if b < 0 then norm_frac (- a) (- b)
     else if a = 0 \<or> b = 0 then (0, 1)
     else let c = gcd a b in (a div c, b div c))"
  by pat_completeness auto
  termination by (relation "measure (\(_, b). if b < 0 then 1 else 0)") auto

declare norm_frac.simps[simp del]

definition frac :: "int \ int \ 'a" where
  "frac a b \ Abs_Frac (norm_frac a b)"

definition plus_frac :: "'a \ 'a \ 'a" where
  [nitpick_simp]: "plus_frac q r = (let d = lcm (denom q) (denom r) in
    frac (num q * (d div denom q) + num r * (d div denom r)) d)"

definition times_frac :: "'a \ 'a \ 'a" where
  [nitpick_simp]: "times_frac q r = frac (num q * num r) (denom q * denom r)"

definition uminus_frac :: "'a \ 'a" where
  "uminus_frac q \ Abs_Frac (- num q, denom q)"

definition number_of_frac :: "int \ 'a" where
  "number_of_frac n \ Abs_Frac (n, 1)"

definition inverse_frac :: "'a \ 'a" where
  "inverse_frac q \ frac (denom q) (num q)"

definition less_frac :: "'a \ 'a \ bool" where
  [nitpick_simp]: "less_frac q r \ num (plus_frac q (uminus_frac r)) < 0"

definition less_eq_frac :: "'a \ 'a \ bool" where
  [nitpick_simp]: "less_eq_frac q r \ num (plus_frac q (uminus_frac r)) \ 0"

definition of_frac :: "'a \ 'b::{inverse,ring_1}" where
  "of_frac q \ of_int (num q) / of_int (denom q)"

axiomatization wf_wfrec :: "('a \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b"

definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
  [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"

definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
  "wfrec' R F x \ if wf R then wf_wfrec' R F x else THE y. wfrec_rel R (\f x. F (cut f R x) x) x y"

ML_file \<open>Tools/Nitpick/kodkod.ML\<close>
ML_file \<open>Tools/Nitpick/kodkod_sat.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_util.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_hol.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_mono.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_preproc.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_scope.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_peephole.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_rep.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_nut.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_kodkod.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_model.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_commands.ML\<close>
ML_file \<open>Tools/Nitpick/nitpick_tests.ML\<close>

setup \<open>
  Nitpick_HOL.register_ersatz_global
    [(\<^const_name>\<open>card\<close>, \<^const_name>\<open>card'\<close>),
     (\<^const_name>\<open>sum\<close>, \<^const_name>\<open>sum'\<close>),
     (\<^const_name>\<open>fold_graph\<close>, \<^const_name>\<open>fold_graph'\<close>),
     (\<^const_abbrev>\<open>wf\<close>, \<^const_name>\<open>wf'\<close>),
     (\<^const_name>\<open>wf_wfrec\<close>, \<^const_name>\<open>wf_wfrec'\<close>),
     (\<^const_name>\<open>wfrec\<close>, \<^const_name>\<open>wfrec'\<close>)]
\<close>

hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod
  refl' wf' card' sum' fold_graph' nat_gcd nat_lcm Frac Abs_Frac Rep_Frac
  zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac
  inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec'

hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word

hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
  card'_def sum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
  size_list_simp nat_lcm_def Frac_def zero_frac_def one_frac_def
  num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
  number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
  wfrec'_def

end

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.