src/HOL/Quickcheck_Narrowing.thy
changeset 43315 893de45ac28d
parent 43314 a9090cabca14
child 43316 3e274608f06b
equal deleted inserted replaced
43314:a9090cabca14 43315:893de45ac28d
   308     by (simp add: of_int_inverse)
   308     by (simp add: of_int_inverse)
   309   ultimately show ?thesis
   309   ultimately show ?thesis
   310     unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
   310     unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
   311 qed
   311 qed
   312 
   312 
   313 type_synonym pos = "code_int list"
       
   314 (*
       
   315 subsubsection {* Term refinement *}
       
   316 
       
   317 definition new :: "pos => type list list => term list"
       
   318 where
       
   319   "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps"
       
   320 
       
   321 fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list"
       
   322 where
       
   323   "refine (Var p (SumOfProd ss)) [] = new p ss"
       
   324 | "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)"
       
   325 | "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))"
       
   326 
       
   327 text {* Find total instantiations of a partial value *}
       
   328 
       
   329 function total :: "term => term list"
       
   330 where
       
   331   "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]"
       
   332 | "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]"
       
   333 by pat_completeness auto
       
   334 
       
   335 termination sorry
       
   336 *)
       
   337 subsubsection {* Narrowing generator type class *}
   313 subsubsection {* Narrowing generator type class *}
   338 
   314 
   339 class narrowing =
   315 class narrowing =
   340   fixes narrowing :: "code_int => 'a cons"
   316   fixes narrowing :: "code_int => 'a cons"
   341 
   317 
   342 definition cons1 :: "('a::narrowing => 'b) => 'b narrowing"
       
   343 where
       
   344   "cons1 f = apply (cons f) narrowing"
       
   345 
       
   346 definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing"
       
   347 where
       
   348   "cons2 f = apply (apply (cons f) narrowing) narrowing"
       
   349 
       
   350 definition drawn_from :: "'a list => 'a cons"
   318 definition drawn_from :: "'a list => 'a cons"
   351 where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
   319 where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
   352 
   320 
   353 instantiation int :: narrowing
   321 instantiation int :: narrowing
   354 begin
   322 begin
   358 
   326 
   359 instance ..
   327 instance ..
   360 
   328 
   361 end
   329 end
   362 
   330 
   363 instantiation unit :: narrowing
       
   364 begin
       
   365 
       
   366 definition
       
   367   "narrowing = cons ()"
       
   368 
       
   369 instance ..
       
   370 
       
   371 end
       
   372 
       
   373 instantiation bool :: narrowing
       
   374 begin
       
   375 
       
   376 definition
       
   377   "narrowing = sum (cons True) (cons False)" 
       
   378 
       
   379 instance ..
       
   380 
       
   381 end
       
   382 
       
   383 instantiation option :: (narrowing) narrowing
       
   384 begin
       
   385 
       
   386 definition
       
   387   "narrowing = sum (cons None) (cons1 Some)"
       
   388 
       
   389 instance ..
       
   390 
       
   391 end
       
   392 
       
   393 instantiation sum :: (narrowing, narrowing) narrowing
       
   394 begin
       
   395 
       
   396 definition
       
   397   "narrowing = sum (cons1 Inl) (cons1 Inr)"
       
   398 
       
   399 instance ..
       
   400 
       
   401 end
       
   402 
       
   403 instantiation list :: (narrowing) narrowing
       
   404 begin
       
   405 
       
   406 function narrowing_list :: "'a list narrowing"
       
   407 where
       
   408   "narrowing_list d = sum (cons []) (apply (apply (cons Cons) narrowing) narrowing_list) d"
       
   409 by pat_completeness auto
       
   410 
       
   411 termination proof (relation "measure nat_of")
       
   412 qed (auto simp add: of_int_inverse nat_of_def)
       
   413     
       
   414 instance ..
       
   415 
       
   416 end
       
   417 
       
   418 instantiation nat :: narrowing
       
   419 begin
       
   420 
       
   421 function narrowing_nat :: "nat narrowing"
       
   422 where
       
   423   "narrowing_nat d = sum (cons 0) (apply (cons Suc) narrowing_nat) d"
       
   424 by pat_completeness auto
       
   425 
       
   426 termination proof (relation "measure nat_of")
       
   427 qed (auto simp add: of_int_inverse nat_of_def)
       
   428 
       
   429 instance ..
       
   430 
       
   431 end
       
   432 
       
   433 instantiation Enum.finite_1 :: narrowing
       
   434 begin
       
   435 
       
   436 definition narrowing_finite_1 :: "Enum.finite_1 narrowing"
       
   437 where
       
   438   "narrowing_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
       
   439 
       
   440 instance ..
       
   441 
       
   442 end
       
   443 
       
   444 instantiation Enum.finite_2 :: narrowing
       
   445 begin
       
   446 
       
   447 definition narrowing_finite_2 :: "Enum.finite_2 narrowing"
       
   448 where
       
   449   "narrowing_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
       
   450 
       
   451 instance ..
       
   452 
       
   453 end
       
   454 
       
   455 instantiation Enum.finite_3 :: narrowing
       
   456 begin
       
   457 
       
   458 definition narrowing_finite_3 :: "Enum.finite_3 narrowing"
       
   459 where
       
   460   "narrowing_finite_3 = sum (cons (Enum.finite_3.a\<^isub>1 :: Enum.finite_3)) (sum (cons (Enum.finite_3.a\<^isub>2 :: Enum.finite_3)) (cons (Enum.finite_3.a\<^isub>3 :: Enum.finite_3)))"
       
   461 
       
   462 instance ..
       
   463 
       
   464 end
       
   465 
       
   466 instantiation Enum.finite_4 :: narrowing
       
   467 begin
       
   468 
       
   469 definition narrowing_finite_4 :: "Enum.finite_4 narrowing"
       
   470 where
       
   471   "narrowing_finite_4 = sum (cons Enum.finite_4.a\<^isub>1) (sum (cons Enum.finite_4.a\<^isub>2) (sum (cons Enum.finite_4.a\<^isub>3) (cons Enum.finite_4.a\<^isub>4)))"
       
   472 
       
   473 instance ..
       
   474 
       
   475 end
       
   476 
       
   477 datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
   331 datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
   478 
   332 
   479 (* FIXME: hard-wired maximal depth of 100 here *)
   333 (* FIXME: hard-wired maximal depth of 100 here *)
   480 fun exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   334 definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   481 where
   335 where
   482   "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   336   "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   483 
   337 
   484 fun "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   338 definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   485 where
   339 where
   486   "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   340   "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   487 
   341 
   488 subsubsection {* class @{text is_testable} *}
   342 subsubsection {* class @{text is_testable} *}
   489 
   343 
   497 
   351 
   498 definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
   352 definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
   499 where
   353 where
   500   "ensure_testable f = f"
   354   "ensure_testable f = f"
   501 
   355 
   502 declare simp_thms(17,19)[code del]
       
   503 
   356 
   504 subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   357 subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   505 
   358 
   506 datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   359 datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   507 
   360 
   528 setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
   381 setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
   529 use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
   382 use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
   530 
   383 
   531 setup {* Narrowing_Generators.setup *}
   384 setup {* Narrowing_Generators.setup *}
   532 
   385 
   533 hide_type (open) code_int narrowing_type narrowing_term cons
   386 hide_type code_int narrowing_type narrowing_term cons property
   534 hide_const (open) int_of of_int nth error toEnum map_index split_At empty
   387 hide_const int_of of_int nth error toEnum map_index split_At empty
   535   C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists
   388   C cons conv nonEmpty "apply" sum ensure_testable all exists 
   536 hide_fact empty_def
   389 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   537 
   390 
   538 end
   391 end