blanchet@33192: (* Title: HOL/Nitpick.thy blanchet@33192: Author: Jasmin Blanchette, TU Muenchen blanchet@35807: Copyright 2008, 2009, 2010 blanchet@33192: blanchet@33192: Nitpick: Yet another counterexample generator for Isabelle/HOL. blanchet@33192: *) blanchet@33192: blanchet@33192: header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} blanchet@33192: blanchet@33192: theory Nitpick haftmann@38393: imports Map Quotient SAT Record blanchet@33192: uses ("Tools/Nitpick/kodkod.ML") blanchet@33192: ("Tools/Nitpick/kodkod_sat.ML") blanchet@33192: ("Tools/Nitpick/nitpick_util.ML") blanchet@33192: ("Tools/Nitpick/nitpick_hol.ML") blanchet@35070: ("Tools/Nitpick/nitpick_preproc.ML") blanchet@33192: ("Tools/Nitpick/nitpick_mono.ML") blanchet@33192: ("Tools/Nitpick/nitpick_scope.ML") blanchet@33192: ("Tools/Nitpick/nitpick_peephole.ML") blanchet@33192: ("Tools/Nitpick/nitpick_rep.ML") blanchet@33192: ("Tools/Nitpick/nitpick_nut.ML") blanchet@33192: ("Tools/Nitpick/nitpick_kodkod.ML") blanchet@33192: ("Tools/Nitpick/nitpick_model.ML") blanchet@33192: ("Tools/Nitpick/nitpick.ML") blanchet@33192: ("Tools/Nitpick/nitpick_isar.ML") blanchet@33192: ("Tools/Nitpick/nitpick_tests.ML") blanchet@33192: begin blanchet@33192: blanchet@33192: typedecl bisim_iterator blanchet@33192: blanchet@33192: axiomatization unknown :: 'a blanchet@34938: and is_unknown :: "'a \ bool" blanchet@33192: and undefined_fast_The :: 'a blanchet@33192: and undefined_fast_Eps :: 'a blanchet@33192: and bisim :: "bisim_iterator \ 'a \ 'a \ bool" blanchet@33192: and bisim_iterator_max :: bisim_iterator blanchet@34938: and Quot :: "'a \ 'b" blanchet@35671: and safe_The :: "('a \ bool) \ 'a" blanchet@35671: and safe_Eps :: "('a \ bool) \ 'a" blanchet@33192: blanchet@35665: datatype ('a, 'b) fin_fun = FinFun "('a \ 'b)" blanchet@35665: datatype ('a, 'b) fun_box = FunBox "('a \ 'b)" blanchet@33192: datatype ('a, 'b) pair_box = PairBox 'a 'b blanchet@34124: blanchet@34124: typedecl unsigned_bit blanchet@34124: typedecl signed_bit blanchet@34124: blanchet@34124: datatype 'a word = Word "('a set)" blanchet@33192: blanchet@33192: text {* blanchet@33192: Alternative definitions. blanchet@33192: *} blanchet@33192: blanchet@36918: lemma If_def [nitpick_def, no_atp]: blanchet@33192: "(if P then Q else R) \ (P \ Q) \ (\ P \ R)" blanchet@33192: by (rule eq_reflection) (rule if_bool_eq_conj) blanchet@33192: blanchet@36918: lemma Ex1_def [nitpick_def, no_atp]: blanchet@33192: "Ex1 P \ \x. P = {x}" blanchet@33192: apply (rule eq_reflection) nipkow@39198: apply (simp add: Ex1_def set_ext_iff) blanchet@33192: apply (rule iffI) blanchet@33192: apply (erule exE) blanchet@33192: apply (erule conjE) blanchet@33192: apply (rule_tac x = x in exI) blanchet@33192: apply (rule allI) blanchet@33192: apply (rename_tac y) blanchet@33192: apply (erule_tac x = y in allE) blanchet@33192: by (auto simp: mem_def) blanchet@33192: blanchet@36918: lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \ (r\<^sup>+)\<^sup>=" blanchet@33192: by simp blanchet@33192: blanchet@36918: lemma rtranclp_def [nitpick_def, no_atp]: blanchet@33192: "rtranclp r a b \ (a = b \ tranclp r a b)" blanchet@33192: by (rule eq_reflection) (auto dest: rtranclpD) blanchet@33192: blanchet@36918: lemma tranclp_def [nitpick_def, no_atp]: blanchet@33192: "tranclp r a b \ trancl (split r) (a, b)" blanchet@33192: by (simp add: trancl_def Collect_def mem_def) blanchet@33192: blanchet@33192: definition refl' :: "('a \ 'a \ bool) \ bool" where blanchet@33192: "refl' r \ \x. (x, x) \ r" blanchet@33192: blanchet@33192: definition wf' :: "('a \ 'a \ bool) \ bool" where blanchet@33192: "wf' r \ acyclic r \ (finite r \ unknown)" blanchet@33192: blanchet@33192: axiomatization wf_wfrec :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" blanchet@33192: blanchet@33192: definition wf_wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where blanchet@33192: [nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x" blanchet@33192: blanchet@33192: definition wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where blanchet@33192: "wfrec' R F x \ if wf R then wf_wfrec' R F x blanchet@33192: else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y" blanchet@33192: blanchet@33192: definition card' :: "('a \ bool) \ nat" where blanchet@35699: "card' A \ if finite A then length (safe_Eps (\xs. set xs = A \ distinct xs)) else 0" blanchet@33192: blanchet@33192: definition setsum' :: "('a \ 'b\comm_monoid_add) \ ('a \ bool) \ 'b" where blanchet@35699: "setsum' f A \ if finite A then listsum (map f (safe_Eps (\xs. set xs = A \ distinct xs))) else 0" blanchet@33192: blanchet@33192: inductive fold_graph' :: "('a \ 'b \ 'b) \ 'b \ ('a \ bool) \ 'b \ bool" where blanchet@33192: "fold_graph' f z {} z" | blanchet@33192: "\x \ A; fold_graph' f z (A - {x}) y\ \ fold_graph' f z A (f x y)" blanchet@33192: blanchet@33192: text {* blanchet@33192: The following lemmas are not strictly necessary but they help the blanchet@33192: \textit{special\_level} optimization. blanchet@33192: *} blanchet@33192: blanchet@36918: lemma The_psimp [nitpick_psimp, no_atp]: blanchet@33192: "P = {x} \ The P = x" blanchet@33192: by (subgoal_tac "{x} = (\y. y = x)") (auto simp: mem_def) blanchet@33192: blanchet@36918: lemma Eps_psimp [nitpick_psimp, no_atp]: blanchet@33192: "\P x; \ P y; Eps P = y\ \ Eps P = x" blanchet@33192: apply (case_tac "P (Eps P)") blanchet@33192: apply auto blanchet@33192: apply (erule contrapos_np) blanchet@33192: by (rule someI) blanchet@33192: blanchet@36918: lemma unit_case_def [nitpick_def, no_atp]: blanchet@33192: "unit_case x u \ x" blanchet@33192: apply (subgoal_tac "u = ()") blanchet@33192: apply (simp only: unit.cases) blanchet@33192: by simp blanchet@33192: blanchet@33556: declare unit.cases [nitpick_simp del] blanchet@33556: blanchet@36918: lemma nat_case_def [nitpick_def, no_atp]: blanchet@33192: "nat_case x f n \ if n = 0 then x else f (n - 1)" blanchet@33192: apply (rule eq_reflection) blanchet@33192: by (case_tac n) auto blanchet@33192: blanchet@33556: declare nat.cases [nitpick_simp del] blanchet@33556: blanchet@36918: lemma list_size_simp [nitpick_simp, no_atp]: blanchet@33192: "list_size f xs = (if xs = [] then 0 blanchet@33192: else Suc (f (hd xs) + list_size f (tl xs)))" blanchet@33192: "size xs = (if xs = [] then 0 else Suc (size (tl xs)))" blanchet@33192: by (case_tac xs) auto blanchet@33192: blanchet@33192: text {* blanchet@33192: Auxiliary definitions used to provide an alternative representation for blanchet@33192: @{text rat} and @{text real}. blanchet@33192: *} blanchet@33192: blanchet@33192: function nat_gcd :: "nat \ nat \ nat" where blanchet@33192: [simp del]: "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" blanchet@33192: by auto blanchet@33192: termination blanchet@33192: apply (relation "measure (\(x, y). x + y + (if y > x then 1 else 0))") blanchet@33192: apply auto blanchet@33192: apply (metis mod_less_divisor xt1(9)) blanchet@33192: by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10)) blanchet@33192: blanchet@33192: definition nat_lcm :: "nat \ nat \ nat" where blanchet@33192: "nat_lcm x y = x * y div (nat_gcd x y)" blanchet@33192: blanchet@33192: definition int_gcd :: "int \ int \ int" where blanchet@33192: "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))" blanchet@33192: blanchet@33192: definition int_lcm :: "int \ int \ int" where blanchet@33192: "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))" blanchet@33192: blanchet@33192: definition Frac :: "int \ int \ bool" where blanchet@33192: "Frac \ \(a, b). b > 0 \ int_gcd a b = 1" blanchet@33192: blanchet@33192: axiomatization Abs_Frac :: "int \ int \ 'a" blanchet@33192: and Rep_Frac :: "'a \ int \ int" blanchet@33192: blanchet@33192: definition zero_frac :: 'a where blanchet@33192: "zero_frac \ Abs_Frac (0, 1)" blanchet@33192: blanchet@33192: definition one_frac :: 'a where blanchet@33192: "one_frac \ Abs_Frac (1, 1)" blanchet@33192: blanchet@33192: definition num :: "'a \ int" where blanchet@33192: "num \ fst o Rep_Frac" blanchet@33192: blanchet@33192: definition denom :: "'a \ int" where blanchet@33192: "denom \ snd o Rep_Frac" blanchet@33192: blanchet@33192: function norm_frac :: "int \ int \ int \ int" where blanchet@33192: [simp del]: "norm_frac a b = (if b < 0 then norm_frac (- a) (- b) blanchet@33192: else if a = 0 \ b = 0 then (0, 1) blanchet@33192: else let c = int_gcd a b in (a div c, b div c))" blanchet@33192: by pat_completeness auto blanchet@33192: termination by (relation "measure (\(_, b). if b < 0 then 1 else 0)") auto blanchet@33192: blanchet@33192: definition frac :: "int \ int \ 'a" where blanchet@33192: "frac a b \ Abs_Frac (norm_frac a b)" blanchet@33192: blanchet@33192: definition plus_frac :: "'a \ 'a \ 'a" where blanchet@33192: [nitpick_simp]: blanchet@33192: "plus_frac q r = (let d = int_lcm (denom q) (denom r) in blanchet@33192: frac (num q * (d div denom q) + num r * (d div denom r)) d)" blanchet@33192: blanchet@33192: definition times_frac :: "'a \ 'a \ 'a" where blanchet@33192: [nitpick_simp]: blanchet@33192: "times_frac q r = frac (num q * num r) (denom q * denom r)" blanchet@33192: blanchet@33192: definition uminus_frac :: "'a \ 'a" where blanchet@33192: "uminus_frac q \ Abs_Frac (- num q, denom q)" blanchet@33192: blanchet@33192: definition number_of_frac :: "int \ 'a" where blanchet@33192: "number_of_frac n \ Abs_Frac (n, 1)" blanchet@33192: blanchet@33192: definition inverse_frac :: "'a \ 'a" where blanchet@33192: "inverse_frac q \ frac (denom q) (num q)" blanchet@33192: blanchet@37397: definition less_frac :: "'a \ 'a \ bool" where blanchet@37397: [nitpick_simp]: blanchet@37397: "less_frac q r \ num (plus_frac q (uminus_frac r)) < 0" blanchet@37397: blanchet@33192: definition less_eq_frac :: "'a \ 'a \ bool" where blanchet@33192: [nitpick_simp]: blanchet@33192: "less_eq_frac q r \ num (plus_frac q (uminus_frac r)) \ 0" blanchet@33192: blanchet@33192: definition of_frac :: "'a \ 'b\{inverse,ring_1}" where blanchet@33192: "of_frac q \ of_int (num q) / of_int (denom q)" blanchet@33192: blanchet@33192: use "Tools/Nitpick/kodkod.ML" blanchet@33192: use "Tools/Nitpick/kodkod_sat.ML" blanchet@33192: use "Tools/Nitpick/nitpick_util.ML" blanchet@33192: use "Tools/Nitpick/nitpick_hol.ML" blanchet@35665: use "Tools/Nitpick/nitpick_mono.ML" blanchet@35070: use "Tools/Nitpick/nitpick_preproc.ML" blanchet@33192: use "Tools/Nitpick/nitpick_scope.ML" blanchet@33192: use "Tools/Nitpick/nitpick_peephole.ML" blanchet@33192: use "Tools/Nitpick/nitpick_rep.ML" blanchet@33192: use "Tools/Nitpick/nitpick_nut.ML" blanchet@33192: use "Tools/Nitpick/nitpick_kodkod.ML" blanchet@33192: use "Tools/Nitpick/nitpick_model.ML" blanchet@33192: use "Tools/Nitpick/nitpick.ML" blanchet@33192: use "Tools/Nitpick/nitpick_isar.ML" blanchet@33192: use "Tools/Nitpick/nitpick_tests.ML" blanchet@33192: blanchet@33561: setup {* Nitpick_Isar.setup *} blanchet@33561: wenzelm@36176: hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim blanchet@35671: bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl' blanchet@35671: wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm blanchet@35671: int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom blanchet@35671: norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac blanchet@37397: less_frac less_eq_frac of_frac wenzelm@36176: hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit blanchet@35665: word blanchet@37704: hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def blanchet@37704: wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def blanchet@37704: The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def blanchet@37704: nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def blanchet@37704: num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def blanchet@37704: uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def blanchet@37704: less_eq_frac_def of_frac_def blanchet@33192: blanchet@33192: end