# HG changeset patch # User blanchet # Date 1410288696 -7200 # Node ID 990f89288143dc7e9bfe822101cd756c7b6eacca # Parent 4a6c9bcb418941815fd434518d534596e4642f4c ported Nitpick_Examples to new datatypes diff -r 4a6c9bcb4189 -r 990f89288143 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Sep 09 20:51:36 2014 +0200 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Sep 09 20:51:36 2014 +0200 @@ -885,7 +885,7 @@ apply simp done -lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)" +lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)" nitpick [card = 1-3, expect = none] apply simp done @@ -898,12 +898,12 @@ nitpick [expect = genuine] oops -lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)" +lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)" nitpick [card = 1-3, expect = none] apply simp done -lemma "P (rec_aexp_bexp_2 number ite equal x)" +lemma "P (rec_bexp number ite equal x)" nitpick [expect = genuine] oops @@ -967,22 +967,22 @@ apply simp done -lemma "rec_X a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)" +lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X a b c d e f x)" +lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)" +lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_X_Y_2 a b c d e f F = f" +lemma "rec_Y a b c d e f F = f" nitpick [card = 1-5, expect = none] apply simp done @@ -991,7 +991,7 @@ nitpick [expect = genuine] oops -lemma "P (rec_X_Y_2 a b c d e f y)" +lemma "P (rec_Y a b c d e f y)" nitpick [expect = genuine] oops @@ -1013,48 +1013,10 @@ nitpick [expect = genuine] oops -lemma "rec_X cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" -nitpick [card = 1-5, expect = none] -apply simp -done - -lemma "rec_X cx dx n1 s1 n2 s2 (DX x) = dx x (\b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))" -nitpick [card = 1-3, expect = none] -apply simp -done - -lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1" -nitpick [card = 1-4, expect = none] -apply simp -done - -lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_X cx dx n1 s1 n2 s2 x)" -nitpick [card = 1-4, expect = none] -apply simp -done - -lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2" -nitpick [card = 1-4, expect = none] -apply simp -done - -lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_X cx dx n1 s1 n2 s2 x)" -nitpick [card = 1-4, expect = none] -apply simp -done - lemma "P (rec_X cx dx n1 s1 n2 s2 x)" nitpick [expect = genuine] oops -lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" -nitpick [expect = genuine] -oops - -lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)" -nitpick [expect = genuine] -oops - datatype_new 'a YOpt = CY "('a \ 'a YOpt) option" lemma "P (x\'a YOpt)" @@ -1102,7 +1064,7 @@ apply simp done -lemma "rec_InfTree leaf node (Node x) = node x (\n. rec_InfTree leaf node (x n))" +lemma "rec_InfTree leaf node (Node g) = node ((\InfTree. (InfTree, rec_InfTree leaf node InfTree)) \ g)" nitpick [card = 1-3, expect = none] apply simp done @@ -1136,7 +1098,7 @@ apply simp done -lemma "rec_lambda var app lam (Lam x) = lam x (\a. rec_lambda var app lam (x a))" +lemma "rec_lambda var app lam (Lam x) = lam ((\lambda. (lambda, rec_lambda var app lam lambda)) \ x)" nitpick [card = 1-3, expect = none] apply simp done @@ -1147,7 +1109,7 @@ text {* Taken from "Inductive datatypes in HOL", p. 8: *} -datatype_new ('a, 'b) T = C "'a \ bool" | D "'b list" +datatype_new (dead 'a, 'b) T = C "'a \ bool" | D "'b list" datatype_new 'c U = E "('c, 'c U) T" lemma "P (x\'c U)"