Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Quickcheck.thy
changeset 26944 1fe801f9cfc9
parent 26829 229e8078b1e0
child 27103 d8549f4d900b
equal deleted inserted replaced
26943:aec0d97a01c4 26944:1fe801f9cfc9 
   289   contains FOO*)
 
   289   contains FOO*)
 
   290 
   290 
   291 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   291 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   292   @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
 
   292   @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
 
   293 
   293 
   294 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   294 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   295 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   295 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   296 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   296 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   297 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   297 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   298 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   298 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   299 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   299 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   300 ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   300 ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   301 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   301 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   302 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   302 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   303 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   303 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   304 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   304 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   305 
   305 
   306 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   306 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   307   @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
 
   307   @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
 
   308 
   308 
   309 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   309 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   310 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   310 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   311 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   311 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   312 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   312 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   313 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   313 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   314 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   314 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   315 ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   315 ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   316 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   316 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   317 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   317 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   318 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   318 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   319 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   319 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   320 ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   320 ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   321 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   321 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   322 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   322 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   323 
   323 
   324 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   324 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   325   @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"}
 
   325   @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"}
 
   326   [@{typ "int list"}, @{typ "int list"}] *}
 
   326   [@{typ "int list"}, @{typ "int list"}] *}
 
   327 
   327 
   328 ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   328 ML {* f 15 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   329 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   329 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   330 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   330 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   331 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   331 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   332 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   332 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   333 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   333 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   334 ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   334 ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   335 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   335 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   336 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   336 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   337 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   337 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   338 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   338 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   339 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   339 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   340 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   340 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   341 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   341 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   342 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   342 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   343 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   343 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   344 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   344 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   345 ML {* f 88 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   345 ML {* f 88 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   346 
   346 
   347 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   347 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   348 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   348 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   349 ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   349 ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   350 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   350 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   351 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   351 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   352 ML {* f 6 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   352 ML {* f 6 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   353 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   353 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   354 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   354 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   355 
   355 
   356 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   356 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   357   @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *}
 
   357   @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *}
 
   358 
   358 
   359 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   359 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   360 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   360 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   361 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   361 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   362 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   362 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   363 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   363 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   364 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   364 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   365 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   365 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   366 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   366 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   367 ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   367 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   368 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   368 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   369 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   369 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   370 
   370 
   371 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   371 ML {* val f = Quickcheck.compile_generator_expr @{theory}
 
   372   @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
 
   372   @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
 
   373 
   373 
   374 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   374 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   375 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   375 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   376 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   376 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   377 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   377 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   378 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   378 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   379 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
   379 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
   380 
   380 
   381 end
 
   381 end
isabelle