adapt and reactivate Quickcheck_Types and add two test cases
authorAndreas Lochbihler
Fri Jul 11 15:35:11 2014 +0200 (2014-07-11)
changeset 5754336041934e429
parent 57542 faa8b4486d5a
child 57544 8840fa17e17c
adapt and reactivate Quickcheck_Types and add two test cases
src/HOL/Library/Quickcheck_Types.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Library/Quickcheck_Types.thy	Fri Jul 11 00:55:46 2014 +0200
     1.2 +++ b/src/HOL/Library/Quickcheck_Types.thy	Fri Jul 11 15:35:11 2014 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  *)
     1.5  
     1.6  theory Quickcheck_Types
     1.7 -imports Main
     1.8 +imports "../Main"
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -113,8 +113,7 @@
    1.13  
    1.14  definition "bot = Bot"
    1.15  
    1.16 -instance proof
    1.17 -qed (simp add: bot_bot_def)
    1.18 +instance ..
    1.19  
    1.20  end
    1.21  
    1.22 @@ -123,8 +122,7 @@
    1.23  
    1.24  definition "top = Value top"
    1.25  
    1.26 -instance proof
    1.27 -qed (simp add: top_bot_def less_eq_bot_def split: bot.split)
    1.28 +instance ..
    1.29  
    1.30  end
    1.31  
    1.32 @@ -152,7 +150,8 @@
    1.33  
    1.34  end
    1.35  
    1.36 -instance bot :: (lattice) bounded_lattice_bot ..
    1.37 +instance bot :: (lattice) bounded_lattice_bot
    1.38 +by(intro_classes)(simp add: bot_bot_def)
    1.39  
    1.40  section {* Values extended by a top element *}
    1.41  
    1.42 @@ -213,8 +212,7 @@
    1.43  
    1.44  definition "top = Top"
    1.45  
    1.46 -instance proof
    1.47 -qed (simp add: top_top_def)
    1.48 +instance ..
    1.49  
    1.50  end
    1.51  
    1.52 @@ -223,8 +221,7 @@
    1.53  
    1.54  definition "bot = Value bot"
    1.55  
    1.56 -instance proof
    1.57 -qed (simp add: bot_top_def less_eq_top_def split: top.split)
    1.58 +instance ..
    1.59  
    1.60  end
    1.61  
    1.62 @@ -252,7 +249,8 @@
    1.63  
    1.64  end
    1.65  
    1.66 -instance top :: (lattice) bounded_lattice_top ..
    1.67 +instance top :: (lattice) bounded_lattice_top
    1.68 +by(intro_classes)(simp add: top_top_def)
    1.69  
    1.70  
    1.71  datatype 'a flat_complete_lattice = Value 'a | Bot | Top
    1.72 @@ -294,8 +292,7 @@
    1.73  
    1.74  definition "bot = Bot"
    1.75  
    1.76 -instance proof
    1.77 -qed (simp add: bot_flat_complete_lattice_def)
    1.78 +instance ..
    1.79  
    1.80  end
    1.81  
    1.82 @@ -304,8 +301,7 @@
    1.83  
    1.84  definition "top = Top"
    1.85  
    1.86 -instance proof
    1.87 -qed (auto simp add: less_eq_flat_complete_lattice_def top_flat_complete_lattice_def split: flat_complete_lattice.splits)
    1.88 +instance ..
    1.89  
    1.90  end
    1.91  
    1.92 @@ -454,14 +450,28 @@
    1.93    ultimately show "Sup A <= z"
    1.94      unfolding Sup_flat_complete_lattice_def
    1.95      by auto
    1.96 +next
    1.97 +  show "Inf {} = (top :: 'a flat_complete_lattice)"
    1.98 +    by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
    1.99 +next
   1.100 +  show "Sup {} = (bot :: 'a flat_complete_lattice)"
   1.101 +    by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   1.102  qed
   1.103  
   1.104  end
   1.105  
   1.106  section {* Quickcheck configuration *}
   1.107  
   1.108 -quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
   1.109 +quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "Enum.finite_4 flat_complete_lattice"]]
   1.110  
   1.111  hide_type non_distrib_lattice flat_complete_lattice bot top
   1.112  
   1.113 +lemma "\<lbrakk> inf x z = inf y z; sup x z = sup y z \<rbrakk> \<Longrightarrow> x = y" 
   1.114 +quickcheck[exhaustive, expect=counterexample]
   1.115 +oops
   1.116 +
   1.117 +lemma "Inf {} = bot"
   1.118 +quickcheck[exhaustive, expect=counterexample]
   1.119 +oops
   1.120 +
   1.121  end
   1.122 \ No newline at end of file
     2.1 --- a/src/HOL/ROOT	Fri Jul 11 00:55:46 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Fri Jul 11 15:35:11 2014 +0200
     2.3 @@ -52,6 +52,7 @@
     2.4      (*legacy tools*)
     2.5      Refute
     2.6      Old_Recdef
     2.7 +    Quickcheck_Types
     2.8    theories [condition = ISABELLE_FULL_TEST]
     2.9      Sum_of_Squares_Remote
    2.10    document_files "root.bib" "root.tex"