blanchet@33197: (* Title: HOL/Nitpick_Examples/Manual_Nits.thy blanchet@33197: Author: Jasmin Blanchette, TU Muenchen blanchet@45035: Copyright 2009-2011 blanchet@33197: blanchet@33197: Examples from the Nitpick manual. blanchet@33197: *) blanchet@33197: blanchet@33197: header {* Examples from the Nitpick Manual *} blanchet@33197: blanchet@37477: (* The "expect" arguments to Nitpick in this theory and the other example blanchet@37477: theories are there so that the example can also serve as a regression test blanchet@37477: suite. *) blanchet@37477: blanchet@33197: theory Manual_Nits wenzelm@41413: imports Main "~~/src/HOL/Library/Quotient_Product" RealDef blanchet@33197: begin blanchet@33197: blanchet@45053: chapter {* 2. First Steps *} blanchet@33197: blanchet@41278: nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1, krauss@42208: timeout = 240] blanchet@33197: blanchet@45053: subsection {* 2.1. Propositional Logic *} blanchet@33197: blanchet@33197: lemma "P \ Q" blanchet@35671: nitpick [expect = genuine] blanchet@33197: apply auto blanchet@35671: nitpick [expect = genuine] 1 blanchet@35671: nitpick [expect = genuine] 2 blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.2. Type Variables *} blanchet@33197: blanchet@33197: lemma "P x \ P (THE y. P y)" blanchet@35671: nitpick [verbose, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.3. Constants *} blanchet@33197: blanchet@33197: lemma "P x \ P (THE y. P y)" blanchet@35671: nitpick [show_consts, expect = genuine] blanchet@39362: nitpick [dont_specialize, show_consts, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\!x. P x \ P (THE y. P y)" blanchet@35671: nitpick [expect = none] blanchet@42959: nitpick [card 'a = 1\50, expect = none] blanchet@33197: (* sledgehammer *) blanchet@33197: apply (metis the_equality) blanchet@33197: done blanchet@33197: blanchet@45053: subsection {* 2.4. Skolemization *} blanchet@33197: blanchet@33197: lemma "\g. \x. g (f x) = x \ \y. \x. y = f x" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\x. \f. f x = x" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "refl r \ sym r" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.5. Natural Numbers and Integers *} blanchet@33197: blanchet@33197: lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ i * m + j * n" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\n. Suc n \ n \ P" blanchet@42421: nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "P Suc" blanchet@35671: nitpick [expect = none] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "P (op +\nat\nat\nat)" blanchet@35671: nitpick [card nat = 1, expect = genuine] blanchet@35671: nitpick [card nat = 2, expect = none] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.6. Inductive Datatypes *} blanchet@33197: blanchet@33197: lemma "hd (xs @ [y, y]) = hd xs" blanchet@35671: nitpick [expect = genuine] blanchet@35671: nitpick [show_consts, show_datatypes, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\length xs = 1; length ys = 1\ \ xs = ys" blanchet@35671: nitpick [show_datatypes, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} blanchet@33197: wenzelm@45694: definition "three = {0\nat, 1, 2}" wenzelm@45694: typedef (open) three = three wenzelm@45694: unfolding three_def by blast blanchet@33197: blanchet@33197: definition A :: three where "A \ Abs_three 0" blanchet@33197: definition B :: three where "B \ Abs_three 1" blanchet@33197: definition C :: three where "C \ Abs_three 2" blanchet@33197: blanchet@33197: lemma "\P A; P B\ \ P x" blanchet@35671: nitpick [show_datatypes, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@35284: fun my_int_rel where blanchet@35284: "my_int_rel (x, y) (u, v) = (x + v = u + y)" blanchet@35284: blanchet@35284: quotient_type my_int = "nat \ nat" / my_int_rel nipkow@39302: by (auto simp add: equivp_def fun_eq_iff) blanchet@35284: blanchet@35284: definition add_raw where blanchet@35284: "add_raw \ \(x, y) (u, v). (x + (u\nat), y + (v\nat))" blanchet@35284: blanchet@35284: quotient_definition "add\my_int \ my_int \ my_int" is add_raw blanchet@35284: blanchet@35284: lemma "add x y = add x x" blanchet@35671: nitpick [show_datatypes, expect = genuine] blanchet@35284: oops blanchet@35284: blanchet@35711: ML {* blanchet@35712: fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) = blanchet@35712: HOLogic.mk_number T (snd (HOLogic.dest_number t1) blanchet@35712: - snd (HOLogic.dest_number t2)) blanchet@35712: | my_int_postproc _ _ _ _ t = t blanchet@35711: *} blanchet@35711: blanchet@38288: declaration {* blanchet@38284: Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc blanchet@38242: *} blanchet@35711: blanchet@35711: lemma "add x y = add x x" blanchet@35711: nitpick [show_datatypes] blanchet@35711: oops blanchet@35711: blanchet@33197: record point = blanchet@33197: Xcoord :: int blanchet@33197: Ycoord :: int blanchet@33197: blanchet@33197: lemma "Xcoord (p\point) = Xcoord (q\point)" blanchet@35671: nitpick [show_datatypes, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "4 * x + 3 * (y\real) \ 1 / 2" blanchet@35671: nitpick [show_datatypes, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.8. Inductive and Coinductive Predicates *} blanchet@33197: blanchet@33197: inductive even where blanchet@33197: "even 0" | blanchet@33197: "even n \ even (Suc (Suc n))" blanchet@33197: blanchet@33197: lemma "\n. even n \ even (Suc n)" blanchet@35710: nitpick [card nat = 50, unary_ints, verbose, expect = potential] blanchet@33197: oops blanchet@33197: blanchet@35710: lemma "\n \ 49. even n \ even (Suc n)" blanchet@38184: nitpick [card nat = 50, unary_ints, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: inductive even' where blanchet@33197: "even' (0\nat)" | blanchet@33197: "even' 2" | blanchet@33197: "\even' m; even' n\ \ even' (m + n)" blanchet@33197: blanchet@33197: lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" blanchet@35671: nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "even' (n - 2) \ even' n" blanchet@35671: nitpick [card nat = 10, show_consts, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: coinductive nats where blanchet@33197: "nats (x\nat) \ nats x" blanchet@33197: blanchet@33197: lemma "nats = {0, 1, 2, 3, 4}" blanchet@35671: nitpick [card nat = 10, show_consts, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: inductive odd where blanchet@33197: "odd 1" | blanchet@33197: "\odd m; even n\ \ odd (m + n)" blanchet@33197: blanchet@33197: lemma "odd n \ odd (n - 2)" blanchet@35671: nitpick [card nat = 10, show_consts, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.9. Coinductive Datatypes *} blanchet@33197: blanchet@35665: (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since blanchet@38184: we cannot rely on its presence, we expediently provide our own blanchet@38184: axiomatization. The examples also work unchanged with Lochbihler's blanchet@38184: "Coinductive_List" theory. *) blanchet@35665: wenzelm@45694: definition "llist = (UNIV\('a list + (nat \ 'a)) set)" wenzelm@45694: wenzelm@45694: typedef (open) 'a llist = "llist\('a list + (nat \ 'a)) set" wenzelm@45694: unfolding llist_def by auto blanchet@35665: blanchet@35671: definition LNil where blanchet@35671: "LNil = Abs_llist (Inl [])" blanchet@35665: definition LCons where blanchet@35665: "LCons y ys = Abs_llist (case Rep_llist ys of blanchet@35665: Inl ys' \ Inl (y # ys') blanchet@35665: | Inr f \ Inr (\n. case n of 0 \ y | Suc m \ f m))" blanchet@35665: blanchet@35665: axiomatization iterates :: "('a \ 'a) \ 'a \ 'a llist" blanchet@35665: blanchet@35665: lemma iterates_def [nitpick_simp]: blanchet@35665: "iterates f a = LCons a (iterates f (f a))" blanchet@35665: sorry blanchet@35665: blanchet@38288: declaration {* blanchet@38284: Nitpick_HOL.register_codatatype @{typ "'a llist"} "" blanchet@35665: (map dest_Const [@{term LNil}, @{term LCons}]) blanchet@35665: *} blanchet@35665: blanchet@33197: lemma "xs \ LCons a xs" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\xs = LCons a xs; ys = iterates (\b. a) b\ \ xs = ys" blanchet@35671: nitpick [verbose, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" blanchet@35671: nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@45053: subsection {* 2.10. Boxing *} blanchet@33197: blanchet@33197: datatype tm = Var nat | Lam tm | App tm tm blanchet@33197: blanchet@33197: primrec lift where blanchet@33197: "lift (Var j) k = Var (if j < k then j else j + 1)" | blanchet@33197: "lift (Lam t) k = Lam (lift t (k + 1))" | blanchet@33197: "lift (App t u) k = App (lift t k) (lift u k)" blanchet@33197: blanchet@33197: primrec loose where blanchet@33197: "loose (Var j) k = (j \ k)" | blanchet@33197: "loose (Lam t) k = loose t (Suc k)" | blanchet@33197: "loose (App t u) k = (loose t k \ loose u k)" blanchet@33197: blanchet@33197: primrec subst\<^isub>1 where blanchet@33197: "subst\<^isub>1 \ (Var j) = \ j" | blanchet@33197: "subst\<^isub>1 \ (Lam t) = blanchet@33197: Lam (subst\<^isub>1 (\n. case n of 0 \ Var 0 | Suc m \ lift (\ m) 1) t)" | blanchet@33197: "subst\<^isub>1 \ (App t u) = App (subst\<^isub>1 \ t) (subst\<^isub>1 \ u)" blanchet@33197: blanchet@33197: lemma "\ loose t 0 \ subst\<^isub>1 \ t = t" blanchet@35671: nitpick [verbose, expect = genuine] blanchet@35671: nitpick [eval = "subst\<^isub>1 \ t", expect = genuine] blanchet@35671: (* nitpick [dont_box, expect = unknown] *) blanchet@33197: oops blanchet@33197: blanchet@33197: primrec subst\<^isub>2 where blanchet@33197: "subst\<^isub>2 \ (Var j) = \ j" | blanchet@33197: "subst\<^isub>2 \ (Lam t) = blanchet@33197: Lam (subst\<^isub>2 (\n. case n of 0 \ Var 0 | Suc m \ lift (\ m) 0) t)" | blanchet@33197: "subst\<^isub>2 \ (App t u) = App (subst\<^isub>2 \ t) (subst\<^isub>2 \ u)" blanchet@33197: blanchet@33197: lemma "\ loose t 0 \ subst\<^isub>2 \ t = t" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@45053: subsection {* 2.11. Scope Monotonicity *} blanchet@33197: blanchet@33197: lemma "length xs = length ys \ rev (zip xs ys) = zip xs (rev ys)" blanchet@35671: nitpick [verbose, expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: lemma "\g. \x\'b. g (f x) = x \ \y\'a. \x. y = f x" blanchet@35671: nitpick [mono, expect = none] blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@45053: subsection {* 2.12. Inductive Properties *} blanchet@34982: blanchet@34982: inductive_set reach where blanchet@34982: "(4\nat) \ reach" | blanchet@34982: "n \ reach \ n < 4 \ 3 * n + 1 \ reach" | blanchet@34982: "n \ reach \ n + 2 \ reach" blanchet@34982: blanchet@34982: lemma "n \ reach \ 2 dvd n" blanchet@38184: (* nitpick *) blanchet@34982: apply (induct set: reach) blanchet@34982: apply auto blanchet@42959: nitpick [card = 1\4, bits = 1\4, expect = none] blanchet@34982: apply (thin_tac "n \ reach") blanchet@35671: nitpick [expect = genuine] blanchet@34982: oops blanchet@34982: blanchet@34982: lemma "n \ reach \ 2 dvd n \ n \ 0" blanchet@38184: (* nitpick *) blanchet@34982: apply (induct set: reach) blanchet@34982: apply auto blanchet@42959: nitpick [card = 1\4, bits = 1\4, expect = none] blanchet@34982: apply (thin_tac "n \ reach") blanchet@35671: nitpick [expect = genuine] blanchet@34982: oops blanchet@34982: blanchet@34982: lemma "n \ reach \ 2 dvd n \ n \ 4" blanchet@34982: by (induct set: reach) arith+ blanchet@34982: blanchet@34982: datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree" blanchet@34982: blanchet@34982: primrec labels where blanchet@34982: "labels (Leaf a) = {a}" | blanchet@34982: "labels (Branch t u) = labels t \ labels u" blanchet@34982: blanchet@34982: primrec swap where blanchet@34982: "swap (Leaf c) a b = blanchet@34982: (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" | blanchet@34982: "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" blanchet@34982: blanchet@35180: lemma "{a, b} \ labels t \ labels (swap t a b) = labels t" blanchet@35671: (* nitpick *) blanchet@34982: proof (induct t) blanchet@34982: case Leaf thus ?case by simp blanchet@34982: next blanchet@34982: case (Branch t u) thus ?case blanchet@35671: (* nitpick *) blanchet@35671: nitpick [non_std, show_all, expect = genuine] blanchet@34982: oops blanchet@34982: blanchet@34982: lemma "labels (swap t a b) = blanchet@34982: (if a \ labels t then blanchet@34982: if b \ labels t then labels t else (labels t - {a}) \ {b} blanchet@34982: else blanchet@34982: if b \ labels t then (labels t - {b}) \ {a} else labels t)" blanchet@35309: (* nitpick *) blanchet@34982: proof (induct t) blanchet@34982: case Leaf thus ?case by simp blanchet@34982: next blanchet@34982: case (Branch t u) thus ?case blanchet@42959: nitpick [non_std, card = 1\4, expect = none] blanchet@34982: by auto blanchet@34982: qed blanchet@34982: blanchet@45053: section {* 3. Case Studies *} blanchet@33197: blanchet@36268: nitpick_params [max_potential = 0] blanchet@33197: blanchet@45053: subsection {* 3.1. A Context-Free Grammar *} blanchet@33197: blanchet@33197: datatype alphabet = a | b blanchet@33197: blanchet@33197: inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where blanchet@33197: "[] \ S\<^isub>1" blanchet@33197: | "w \ A\<^isub>1 \ b # w \ S\<^isub>1" blanchet@33197: | "w \ B\<^isub>1 \ a # w \ S\<^isub>1" blanchet@33197: | "w \ S\<^isub>1 \ a # w \ A\<^isub>1" blanchet@33197: | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" blanchet@33197: | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" blanchet@33197: blanchet@33197: theorem S\<^isub>1_sound: blanchet@33197: "w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where blanchet@33197: "[] \ S\<^isub>2" blanchet@33197: | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" blanchet@33197: | "w \ B\<^isub>2 \ a # w \ S\<^isub>2" blanchet@33197: | "w \ S\<^isub>2 \ a # w \ A\<^isub>2" blanchet@33197: | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" blanchet@33197: | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" blanchet@33197: blanchet@33197: theorem S\<^isub>2_sound: blanchet@33197: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where blanchet@33197: "[] \ S\<^isub>3" blanchet@33197: | "w \ A\<^isub>3 \ b # w \ S\<^isub>3" blanchet@33197: | "w \ B\<^isub>3 \ a # w \ S\<^isub>3" blanchet@33197: | "w \ S\<^isub>3 \ a # w \ A\<^isub>3" blanchet@33197: | "w \ S\<^isub>3 \ b # w \ B\<^isub>3" blanchet@33197: | "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" blanchet@33197: blanchet@33197: theorem S\<^isub>3_sound: blanchet@33197: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: theorem S\<^isub>3_complete: blanchet@33197: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where blanchet@33197: "[] \ S\<^isub>4" blanchet@33197: | "w \ A\<^isub>4 \ b # w \ S\<^isub>4" blanchet@33197: | "w \ B\<^isub>4 \ a # w \ S\<^isub>4" blanchet@33197: | "w \ S\<^isub>4 \ a # w \ A\<^isub>4" blanchet@33197: | "\v \ A\<^isub>4; w \ A\<^isub>4\ \ b # v @ w \ A\<^isub>4" blanchet@33197: | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" blanchet@33197: | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" blanchet@33197: blanchet@33197: theorem S\<^isub>4_sound: blanchet@33197: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: theorem S\<^isub>4_complete: blanchet@33197: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: blanchet@33197: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" blanchet@33197: "w \ A\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" blanchet@33197: "w \ B\<^isub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@45053: subsection {* 3.2. AA Trees *} blanchet@33197: blanchet@34982: datatype 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" blanchet@33197: blanchet@33197: primrec data where blanchet@33197: "data \ = undefined" | blanchet@33197: "data (N x _ _ _) = x" blanchet@33197: blanchet@33197: primrec dataset where blanchet@33197: "dataset \ = {}" | blanchet@33197: "dataset (N x _ t u) = {x} \ dataset t \ dataset u" blanchet@33197: blanchet@33197: primrec level where blanchet@33197: "level \ = 0" | blanchet@33197: "level (N _ k _ _) = k" blanchet@33197: blanchet@33197: primrec left where blanchet@33197: "left \ = \" | blanchet@33197: "left (N _ _ t\<^isub>1 _) = t\<^isub>1" blanchet@33197: blanchet@33197: primrec right where blanchet@33197: "right \ = \" | blanchet@33197: "right (N _ _ _ t\<^isub>2) = t\<^isub>2" blanchet@33197: blanchet@33197: fun wf where blanchet@33197: "wf \ = True" | blanchet@33197: "wf (N _ k t u) = blanchet@33197: (if t = \ then blanchet@33197: k = 1 \ (u = \ \ (level u = 1 \ left u = \ \ right u = \)) blanchet@33197: else blanchet@33197: wf t \ wf u \ u \ \ \ level t < k \ level u \ k \ level (right u) < k)" blanchet@33197: blanchet@33197: fun skew where blanchet@33197: "skew \ = \" | blanchet@33197: "skew (N x k t u) = blanchet@33197: (if t \ \ \ k = level t then blanchet@33197: N (data t) k (left t) (N x k (right t) u) blanchet@33197: else blanchet@33197: N x k t u)" blanchet@33197: blanchet@33197: fun split where blanchet@33197: "split \ = \" | blanchet@33197: "split (N x k t u) = blanchet@33197: (if u \ \ \ k = level (right u) then blanchet@33197: N (data u) (Suc k) (N x k t (left u)) (right u) blanchet@33197: else blanchet@33197: N x k t u)" blanchet@33197: blanchet@33197: theorem dataset_skew_split: blanchet@33197: "dataset (skew t) = dataset t" blanchet@33197: "dataset (split t) = dataset t" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: theorem wf_skew_split: blanchet@33197: "wf t \ skew t = t" blanchet@33197: "wf t \ split t = t" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: primrec insort\<^isub>1 where blanchet@33197: "insort\<^isub>1 \ x = N x 1 \ \" | blanchet@33197: "insort\<^isub>1 (N y k t u) x = blanchet@33197: (* (split \ skew) *) (N y k (if x < y then insort\<^isub>1 t x else t) blanchet@33197: (if x > y then insort\<^isub>1 u x else u))" blanchet@33197: blanchet@33197: theorem wf_insort\<^isub>1: "wf t \ wf (insort\<^isub>1 t x)" blanchet@35671: nitpick [expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: theorem wf_insort\<^isub>1_nat: "wf t \ wf (insort\<^isub>1 t (x\nat))" blanchet@35671: nitpick [eval = "insort\<^isub>1 t x", expect = genuine] blanchet@33197: oops blanchet@33197: blanchet@33197: primrec insort\<^isub>2 where blanchet@33197: "insort\<^isub>2 \ x = N x 1 \ \" | blanchet@33197: "insort\<^isub>2 (N y k t u) x = blanchet@33197: (split \ skew) (N y k (if x < y then insort\<^isub>2 t x else t) blanchet@33197: (if x > y then insort\<^isub>2 u x else u))" blanchet@33197: blanchet@33197: theorem wf_insort\<^isub>2: "wf t \ wf (insort\<^isub>2 t x)" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \ dataset t" blanchet@42959: nitpick [card = 1\5, expect = none] blanchet@33197: sorry blanchet@33197: blanchet@33197: end