Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Nitpick_Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 21 kB

Quelle Core_Nits.thy Sprache: Isabelle

(*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

Examples featuring Nitpick's functional core.
*)

section \<open>Examples Featuring Nitpick's Functional Core\<close>

theory Core_Nits
imports Main
begin

nitpick_params [verbose, card = 1-6, unary_ints, max_potential = 0,
                sat_solver = MiniSat, max_threads = 1, timeout = 240]

subsection \<open>Curry in a Hurry\<close>

lemma "(\f x y. (curry o case_prod) f x y) = (\f x y. (\x. x) f x y)"
nitpick [card = 1-12, expect = none]
by auto

lemma "(\f p. (case_prod o curry) f p) = (\f p. (\x. x) f p)"
nitpick [card = 1-12, expect = none]
by auto

lemma "case_prod (curry f) = f"
nitpick [card = 1-12, expect = none]
by auto

lemma "curry (case_prod f) = f"
nitpick [card = 1-12, expect = none]
by auto

lemma "case_prod (\x y. f (x, y)) = f"
nitpick [card = 1-12, expect = none]
by auto

subsection \<open>Representations\<close>

lemma "\f. f = (\x. x) \ f y = y"
nitpick [expect = none]
by auto

lemma "(\g. \x. g (f x) = x) \ (\y. \x. y = f x)"
nitpick [card 'a = 25, card 'b = 24, expect = genuine]
nitpick [card = 1-10, mono, expect = none]
oops

lemma "\f. f = (\x. x) \ f y \ y"
nitpick [card = 1, expect = genuine]
oops

lemma "P (\x. x)"
nitpick [card = 1, expect = genuine]
oops

lemma "{(a::'a\'a, b::'b)}\ = {(b, a)}"
nitpick [card = 1-12, expect = none]
by auto

lemma "fst (a, b) = a"
nitpick [card = 1-20, expect = none]
by auto

lemma "\P. P = Id"
nitpick [card = 1-20, expect = none]
by auto

lemma "(a::'a\'b, a) \ Id\<^sup>*"
nitpick [card = 1-2, expect = none]
by auto

lemma "(a::'a\'a, a) \ Id\<^sup>* \ {(a, b)}\<^sup>*"
nitpick [card = 1-4, expect = none]
by auto

lemma "(a, a) \ Id"
nitpick [card = 1-50, expect = none]
by (auto simp: Id_def)

lemma "((a::'a, b::'a), (a, b)) \ Id"
nitpick [card = 1-10, expect = none]
by (auto simp: Id_def)

lemma "(x::'a\'a) \ UNIV"
nitpick [card = 1-50, expect = none]
sorry

lemma "{} = A - A"
nitpick [card = 1-100, expect = none]
by auto

lemma "g = Let (A \ B)"
nitpick [card = 1, expect = none]
nitpick [card = 12, expect = genuine]
oops

lemma "(let a_or_b = A \ B in a_or_b \ \ a_or_b)"
nitpick [expect = none]
by auto

lemma "A \ B"
nitpick [card = 100, expect = genuine]
oops

lemma "A = {b}"
nitpick [card = 100, expect = genuine]
oops

lemma "{a, b} = {b}"
nitpick [card = 50, expect = genuine]
oops

lemma "(a::'a\'a, a::'a\'a) \ R"
nitpick [card = 1, expect = genuine]
nitpick [card = 10, expect = genuine]
nitpick [card = 5, dont_box, expect = genuine]
oops

lemma "f (g::'a\'a) = x"
nitpick [card = 3, dont_box, expect = genuine]
nitpick [card = 8, expect = genuine]
oops

lemma "f (a, b) = x"
nitpick [card = 10, expect = genuine]
oops

lemma "f (a, a) = f (c, d)"
nitpick [card = 10, expect = genuine]
oops

lemma "(x::'a) = (\a. \b. \c. if c then a else b) x x True"
nitpick [card = 1-10, expect = none]
by auto

lemma "\F. F a b = G a b"
nitpick [card = 2, expect = none]
by auto

lemma "f = case_prod"
nitpick [card = 2, expect = genuine]
oops

lemma "(A::'a\'a, B::'a\'a) \ R \ (A, B) \ R"
nitpick [card = 15, expect = none]
by auto

lemma "(A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R) \
       A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
nitpick [card = 1-25, expect = none]
by auto

lemma "f = (\x::'a\'b. x)"
nitpick [card = 8, expect = genuine]
oops

subsection \<open>Quantifiers\<close>

lemma "x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x. x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x::'a \ bool. x = y"
nitpick [card 'a = 1, expect = genuine]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x::'a \ bool. x = y"
nitpick [card 'a = 1-15, expect = none]
by auto

lemma "\x y::'a \ bool. x = y"
nitpick [card = 1-15, expect = none]
by auto

lemma "\x. \y. f x y = f x (g x)"
nitpick [card = 1-4, expect = none]
by auto

lemma "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)"
nitpick [card = 1-4, expect = none]
by auto

lemma "\u. \v. \w. \x. f u v w x = f u (g u w) w (h u)"
nitpick [card = 3, expect = genuine]
oops

lemma "\u. \v. \w. \x. \y. \z.
       f u v w x y z = f u (g u) w (h u w) y (k u w y)"
nitpick [card = 1-2, expect = none]
sorry

lemma "\u. \v. \w. \x. \y. \z.
       f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
nitpick [card = 1-2, expect = genuine]
oops

lemma "\u. \v. \w. \x. \y. \z.
       f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
nitpick [card = 1-2, expect = genuine]
oops

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u) w (h u w)"
nitpick [card = 1-2, expect = none]
sorry

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u w) w (h u)"
nitpick [card = 1-2, dont_box, expect = genuine]
oops

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u) w (h u w)"
nitpick [card = 1-2, dont_box, expect = none]
sorry

lemma "\u::'a \ 'b. \v::'c. \w::'d. \x::'e \ 'f.
       f u v w x = f u (g u w) w (h u)"
nitpick [card = 1-2, dont_box, expect = genuine]
oops

lemma "\x. if (\y. x = y) then False else True"
nitpick [card = 1, expect = genuine]
nitpick [card = 2-5, expect = none]
oops

lemma "\x::'a\'b. if (\y. x = y) then False else True"
nitpick [card = 1, expect = genuine]
nitpick [card = 2, expect = none]
oops

lemma "\x. if (\y. x = y) then True else False"
nitpick [expect = none]
sorry

lemma "(\x::'a. \y. P x y) \ (\x::'a \ 'a. \y. P y x)"
nitpick [card 'a = 1, expect = genuine]
oops

lemma "\x. if x = y then (\y. y = x \ y \ x)
           else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
nitpick [expect = none]
by auto

lemma "\x. if x = y then (\y. y = x \ y \ x)
           else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
nitpick [expect = none]
by auto

lemma "let x = (\x. P x) in if x then x else \ x"
nitpick [expect = none]
by auto

lemma "let x = (\x::'a \ 'b. P x) in if x then x else \ x"
nitpick [expect = none]
by auto

subsection \<open>Schematic Variables\<close>

schematic_goal "x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x. x = ?x"
nitpick [expect = genuine]
oops

schematic_goal "\x. x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x::'a \ 'b. x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x. ?x = ?y"
nitpick [expect = none]
by auto

schematic_goal "\x. ?x = ?y"
nitpick [expect = none]
by auto

subsection \<open>Known Constants\<close>

lemma "x \ Pure.all \ False"
nitpick [card = 1, expect = genuine]
nitpick [card = 1, box "('a \ prop) \ prop", expect = genuine]
nitpick [card = 6, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = genuine]
oops

lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop True"
nitpick [expect = none]
by auto

lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop False"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ Pure.all P \ Pure.all (\x. P (I x))"
nitpick [expect = none]
by auto

lemma "x \ (\) \ False"
nitpick [card = 1, expect = genuine]
oops

lemma "P x \ P x"
nitpick [card = 1-10, expect = none]
by auto

lemma "P x \ Q x \ P x = Q x"
nitpick [card = 1-10, expect = none]
by auto

lemma "P x = Q x \ P x \ Q x"
nitpick [card = 1-10, expect = none]
by auto

lemma "x \ (\) \ False"
nitpick [expect = genuine]
oops

lemma "I \ (\x. x) \ ((\) x) \ (\y. ((\) x (I y)))"
nitpick [expect = none]
by auto

lemma "P x \ P x"
nitpick [card = 1-10, expect = none]
by auto

lemma "True \ True" "False \ True" "False \ False"
nitpick [expect = none]
by auto

lemma "True \ False"
nitpick [expect = genuine]
oops

lemma "x = Not"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ Not = (\x. Not (I x))"
nitpick [expect = none]
by auto

lemma "x = True"
nitpick [expect = genuine]
oops

lemma "x = False"
nitpick [expect = genuine]
oops

lemma "x = undefined"
nitpick [expect = genuine]
oops

lemma "(False, ()) = undefined \ ((), False) = undefined"
nitpick [expect = genuine]
oops

lemma "undefined = undefined"
nitpick [expect = none]
by auto

lemma "f undefined = f undefined"
nitpick [expect = none]
by auto

lemma "f undefined = g undefined"
nitpick [card = 33, expect = genuine]
oops

lemma "\!x. x = undefined"
nitpick [card = 15, expect = none]
by auto

lemma "x = All \ False"
nitpick [card = 1, dont_box, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = genuine]
oops

lemma "All (\x. f x y = f x y) = True"
nitpick [expect = none]
by auto

lemma "All (\x. f x y = f x y) = False"
nitpick [expect = genuine]
oops

lemma "x = Ex \ False"
nitpick [card = 1, dont_box, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = none]
oops

lemma "Ex (\x. f x y = f x y) = True"
nitpick [expect = none]
by auto

lemma "Ex (\x. f x y = f y x) = True"
nitpick [expect = none]
by auto

lemma "Ex (\x. f x y = f x y) = False"
nitpick [expect = genuine]
oops

lemma "Ex (\x. f x y \ f x y) = False"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ Ex P = Ex (\x. P (I x))"
nitpick [expect = none]
by auto

lemma "x = y \ y = x"
nitpick [expect = none]
by auto

lemma "x = y \ f x = f y"
nitpick [expect = none]
by auto

lemma "x = y \ y = z \ x = z"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
      "I = (\x. x) \ (\) = (\x y. x \ (I y))"
nitpick [expect = none]
by auto

lemma "(a \ b) = (\ (\ a \ \ b))"
nitpick [expect = none]
by auto

lemma "a \ b \ a" "a \ b \ b"
nitpick [expect = none]
by auto

lemma "(\) = (\x. (\) x)" "((\) ) = (\x y. x \ y)"
nitpick [expect = none]
by auto

lemma "((if a then b else c) = d) = ((a \ (b = d)) \ (\ a \ (c = d)))"
nitpick [expect = none]
by auto

lemma "(if a then b else c) = (THE d. (a \ (d = b)) \ (\ a \ (d = c)))"
nitpick [expect = none]
by auto

lemma "fst (x, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x::'a\'b, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x::'a\'b, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x, y::'a\'b) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y::'a\'b) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x::'a\'b, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x::'a\'b, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x, y::'a\'b) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y::'a\'b) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "I = (\x. x) \ fst = (\x. fst (I x))"
nitpick [expect = none]
by auto

lemma "fst (x, y) = snd (y, x)"
nitpick [expect = none]
by auto

lemma "(x, x) \ Id"
nitpick [expect = none]
by auto

lemma "(x, y) \ Id \ x = y"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ Id = {x. I x \ Id}"
nitpick [expect = none]
by auto

lemma "{} = {x. False}"
nitpick [expect = none]
by (metis empty_def)

lemma "x \ {}"
nitpick [expect = genuine]
oops

lemma "{a, b} = {b}"
nitpick [expect = genuine]
oops

lemma "{a, b} \ {b}"
nitpick [expect = genuine]
oops

lemma "{a} = {b}"
nitpick [expect = genuine]
oops

lemma "{a} \ {b}"
nitpick [expect = genuine]
oops

lemma "{a, b, c} = {c, b, a}"
nitpick [expect = none]
by auto

lemma "UNIV = {x. True}"
nitpick [expect = none]
by (simp only: UNIV_def)

lemma "x \ UNIV \ True"
nitpick [expect = none]
by (simp only: UNIV_def mem_Collect_eq)

lemma "x \ UNIV"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ (\) = (\x. ((\) (I x)))"
nitpick [expect = none]
apply (rule ext)
apply (rule ext)
by simp

lemma "insert = (\x y. insert x (y \ y))"
nitpick [expect = none]
by simp

lemma "I = (\x. x) \ trancl = (\x. trancl (I x))"
nitpick [card = 1-2, expect = none]
by auto

lemma "rtrancl = (\x. rtrancl x \ {(y, y)})"
nitpick [card = 1-3, expect = none]
apply (rule ext)
by auto

lemma "(x, x) \ rtrancl {(y, y)}"
nitpick [expect = none]
by auto

lemma "((x, x), (x, x)) \ rtrancl {}"
nitpick [card = 1-5, expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)"
nitpick [card = 1-5, expect = none]
by auto

lemma "x \ ((A::'a set) - B) \ x \ A \ x \ B"
nitpick [card = 1-5, expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ (\a \ A. a \ B) \ (\b \ B. b \ A)"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ \a \ A. a \ B"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ A \ B"
nitpick [card = 5, expect = genuine]
oops

lemma "A \ B \ A \ B"
nitpick [expect = none]
by auto

lemma "I = (\x::'a set. x) \ uminus = (\x. uminus (I x))"
nitpick [card = 1-7, expect = none]
by auto

lemma "A \ - A = UNIV"
nitpick [expect = none]
by auto

lemma "A \ - A = {}"
nitpick [expect = none]
by auto

lemma "A = -(A::'a set)"
nitpick [card 'a = 10, expect = genuine]
oops

lemma "finite A"
nitpick [expect = none]
oops

lemma "finite A \ finite B"
nitpick [expect = none]
oops

lemma "All finite"
nitpick [expect = none]
oops

subsection \<open>The and Eps\<close>

lemma "x = The"
nitpick [card = 5, expect = genuine]
oops

lemma "\x. x = The"
nitpick [card = 1-3]
by auto

lemma "P x \ (\y. P y \ y = x) \ The P = x"
nitpick [expect = none]
by auto

lemma "P x \ P y \ x \ y \ The P = z"
nitpick [expect = genuine]
oops

lemma "P x \ P y \ x \ y \ The P = x \ The P = y"
nitpick [card = 2, expect = none]
nitpick [card = 3-5, expect = genuine]
oops

lemma "P x \ P (The P)"
nitpick [card = 1-2, expect = none]
nitpick [card = 8, expect = genuine]
oops

lemma "(\x. \ P x) \ The P = y"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ The = (\x. The (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "x = Eps"
nitpick [card = 5, expect = genuine]
oops

lemma "\x. x = Eps"
nitpick [card = 1-3, expect = none]
by auto

lemma "P x \ (\y. P y \ y = x) \ Eps P = x"
nitpick [expect = none]
by auto

lemma "P x \ P y \ x \ y \ Eps P = z"
nitpick [expect = genuine]
apply auto
oops

lemma "P x \ P (Eps P)"
nitpick [card = 1-8, expect = none]
by (metis exE_some)

lemma "\x. \ P x \ Eps P = y"
nitpick [expect = genuine]
oops

lemma "P (Eps P)"
nitpick [expect = genuine]
oops

lemma "Eps (\x. x \ P) \ (P::nat set)"
nitpick [expect = genuine]
oops

lemma "\ P (Eps P)"
nitpick [expect = genuine]
oops

lemma "\ (P :: nat \ bool) (Eps P)"
nitpick [expect = genuine]
oops

lemma "P \ bot \ P (Eps P)"
nitpick [expect = none]
sorry

lemma "(P :: nat \ bool) \ bot \ P (Eps P)"
nitpick [expect = none]
sorry

lemma "P (The P)"
nitpick [expect = genuine]
oops

lemma "(P :: nat \ bool) (The P)"
nitpick [expect = genuine]
oops

lemma "\ P (The P)"
nitpick [expect = genuine]
oops

lemma "\ (P :: nat \ bool) (The P)"
nitpick [expect = genuine]
oops

lemma "The P \ x"
nitpick [expect = genuine]
oops

lemma "The P \ (x::nat)"
nitpick [expect = genuine]
oops

lemma "P x \ P (The P)"
nitpick [expect = genuine]
oops

lemma "P (x::nat) \ P (The P)"
nitpick [expect = genuine]
oops

lemma "P = {x} \ (THE x. x \ P) \ P"
nitpick [expect = none]
oops

lemma "P = {x::nat} \ (THE x. x \ P) \ P"
nitpick [expect = none]
oops

consts Q :: 'a

lemma "Q (Eps Q)"
nitpick [expect = genuine]
oops

lemma "(Q :: nat \ bool) (Eps Q)"
nitpick [expect = none] (* unfortunate *)
oops

lemma "\ (Q :: nat \ bool) (Eps Q)"
nitpick [expect = genuine]
oops

lemma "\ (Q :: nat \ bool) (Eps Q)"
nitpick [expect = genuine]
oops

lemma "(Q::'a \ bool) \ bot \ (Q::'a \ bool) (Eps Q)"
nitpick [expect = none]
sorry

lemma "(Q::nat \ bool) \ bot \ (Q::nat \ bool) (Eps Q)"
nitpick [expect = none]
sorry

lemma "Q (The Q)"
nitpick [expect = genuine]
oops

lemma "(Q::nat \ bool) (The Q)"
nitpick [expect = genuine]
oops

lemma "\ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "\ (Q::nat \ bool) (The Q)"
nitpick [expect = genuine]
oops

lemma "The Q \ x"
nitpick [expect = genuine]
oops

lemma "The Q \ (x::nat)"
nitpick [expect = genuine]
oops

lemma "Q x \ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "Q (x::nat) \ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "Q = (\x::'a. x = a) \ (Q::'a \ bool) (The Q)"
nitpick [expect = none]
sorry

lemma "Q = (\x::nat. x = a) \ (Q::nat \ bool) (The Q)"
nitpick [expect = none]
sorry

nitpick_params [max_potential = 1]

lemma "(THE j. j > Suc 2 \ j \ 3) \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = potential] (* unfortunate *)
oops

lemma "(THE j. j > Suc 2 \ j \ 4) = x \ x \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(THE j. j > Suc 2 \ j \ 4) = x \ x = 4"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(THE j. j > Suc 2 \ j \ 5) = x \ x = 4"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(THE j. j > Suc 2 \ j \ 5) = x \ x = 4 \ x = 5"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 3) \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 4) = x \ x \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
oops

lemma "(SOME j. j > Suc 2 \ j \ 4) = x \ x = 4"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(SOME j. j > Suc 2 \ j \ 5) = x \ x = 4"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 5) = x \ x = 4 \ x = 5"
nitpick [card nat = 6, expect = none]
sorry

nitpick_params [max_potential = 0]

subsection \<open>Destructors and Recursors\<close>

lemma "(x::'a) = (case True of True \ x | False \ x)"
nitpick [card = 2, expect = none]
by auto

lemma "x = (case (x, y) of (x', y') \ x')"
nitpick [expect = none]
sorry

end

quality98%

¤ Dauer der Verarbeitung: 0.14 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.