shortened definitions by adding some termify constants
authorbulwahn
Fri Jan 20 09:28:52 2012 +0100 (2012-01-20)
changeset 46307ec8f975c059b
parent 46306 940ddb42c998
child 46308 e5abbec2697a
shortened definitions by adding some termify constants
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 09:28:51 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 09:28:52 2012 +0100
     1.3 @@ -119,17 +119,13 @@
     1.4  
     1.5  end
     1.6  
     1.7 +definition (in term_syntax) [code_unfold]: "valtermify_pair x y = Code_Evaluation.valtermify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) {\<cdot>} x {\<cdot>} y"
     1.8 +
     1.9  instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
    1.10  begin
    1.11  
    1.12  definition
    1.13 -  "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
    1.14 -    %u. let T1 = (Typerep.typerep (TYPE('a)));
    1.15 -            T2 = (Typerep.typerep (TYPE('b)))
    1.16 -    in Code_Evaluation.App (Code_Evaluation.App (
    1.17 -      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
    1.18 -      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
    1.19 -      (t1 ())) (t2 ()))) d) d"
    1.20 +  "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d"
    1.21  
    1.22  instance ..
    1.23  
    1.24 @@ -140,7 +136,7 @@
    1.25  
    1.26  fun exhaustive_set
    1.27  where
    1.28 -  "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
    1.29 +  "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
    1.30  
    1.31  instance ..
    1.32  
    1.33 @@ -178,22 +174,19 @@
    1.34  
    1.35  end
    1.36  
    1.37 +definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
    1.38 +
    1.39 +definition (in term_syntax) [code_unfold]: "valtermify_fun_upd g a b = Code_Evaluation.valtermify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
    1.40 +
    1.41  instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
    1.42  begin
    1.43  
    1.44  fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.45  where
    1.46 -  "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
    1.47 +  "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d)
    1.48     orelse (if i > 1 then
    1.49 -     full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
    1.50 -       f (g(a := b),
    1.51 -         (%_. let A = (Typerep.typerep (TYPE('a)));
    1.52 -                  B = (Typerep.typerep (TYPE('b)));
    1.53 -                  fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
    1.54 -              in
    1.55 -                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    1.56 -                  (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
    1.57 -                (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
    1.58 +     full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b.
    1.59 +       f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)"
    1.60  
    1.61  definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
    1.62  where
    1.63 @@ -214,6 +207,8 @@
    1.64    "check_all_n_lists f n =
    1.65       (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
    1.66  
    1.67 +definition (in term_syntax) [code_unfold]: "termify_fun_upd g a b = (Code_Evaluation.termify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
    1.68 +
    1.69  definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
    1.70  where
    1.71    "mk_map_term T1 T2 domm rng =
    1.72 @@ -307,48 +302,31 @@
    1.73  
    1.74  end
    1.75  
    1.76 +definition (in term_syntax) [code_unfold]: "termify_pair x y = Code_Evaluation.termify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) <\<cdot>> x <\<cdot>> y"
    1.77  
    1.78  instantiation prod :: (check_all, check_all) check_all
    1.79  begin
    1.80  
    1.81  definition
    1.82 -  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
    1.83 -    %u. let T1 = (Typerep.typerep (TYPE('a)));
    1.84 -            T2 = (Typerep.typerep (TYPE('b)))
    1.85 -    in Code_Evaluation.App (Code_Evaluation.App (
    1.86 -      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
    1.87 -      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
    1.88 -      (t1 ())) (t2 ()))))"
    1.89 +  "check_all f = check_all (%x. check_all (%y. f (valtermify_pair x y)))"
    1.90  
    1.91  definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
    1.92  where
    1.93 -  "enum_term_of_prod = (%_ _. map (%(x, y).
    1.94 -       let T1 = (Typerep.typerep (TYPE('a)));
    1.95 -           T2 = (Typerep.typerep (TYPE('b)))
    1.96 -       in Code_Evaluation.App (Code_Evaluation.App (
    1.97 -         Code_Evaluation.Const (STR ''Product_Type.Pair'') 
    1.98 -           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
    1.99 -     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
   1.100 +  "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
   1.101 +     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   1.102  
   1.103  instance ..
   1.104  
   1.105  end
   1.106  
   1.107 +definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\<cdot>} x"
   1.108 +definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\<cdot>} x"
   1.109  
   1.110  instantiation sum :: (check_all, check_all) check_all
   1.111  begin
   1.112  
   1.113  definition
   1.114 -  "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
   1.115 -     let T1 = (Typerep.typerep (TYPE('a)));
   1.116 -         T2 = (Typerep.typerep (TYPE('b)))
   1.117 -       in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   1.118 -           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
   1.119 -             | None => check_all (%(b, t). f (Inr b, %_. let
   1.120 -                 T1 = (Typerep.typerep (TYPE('a)));
   1.121 -                 T2 = (Typerep.typerep (TYPE('b)))
   1.122 -               in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   1.123 -                 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
   1.124 +  "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))"
   1.125  
   1.126  definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   1.127  where
   1.128 @@ -598,7 +576,9 @@
   1.129    exhaustive'_def
   1.130    exhaustive_code_numeral'_def
   1.131  
   1.132 -hide_const valterm_emptyset valtermify_insert term_emptyset termify_insert setify
   1.133 +hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
   1.134 +  valtermify_Inl valtermify_Inr
   1.135 +  termify_fun_upd term_emptyset termify_insert termify_pair setify
   1.136  
   1.137  hide_const (open)
   1.138    exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'