# HG changeset patch
# User huffman
# Date 1333542440 -7200
# Node ID fc7de207e488560eb3bc5dc08e57978c0b43fff8
# Parent  e0bff2ae939faa8c533715b0d299b16fd9fd3cd4# Parent  803729c9fd4dc20b14110268d4b078321fd6fcab
merged

diff -r e0bff2ae939f -r fc7de207e488 NEWS
--- a/NEWS	Wed Apr 04 11:50:08 2012 +0200
+++ b/NEWS	Wed Apr 04 14:27:20 2012 +0200
@@ -422,7 +422,9 @@
   - Support for multisets.
 
   - Added "use_subtype" options.
- 
+  - Added "quickcheck_locale" configuration to specify how to process
+    conjectures in a locale context.
+
 * Nitpick:
   - Fixed infinite loop caused by the 'peephole_optim' option and
     affecting 'rat' and 'real'.
diff -r e0bff2ae939f -r fc7de207e488 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Apr 04 11:50:08 2012 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Apr 04 14:27:20 2012 +0200
@@ -1382,9 +1382,9 @@
     is a quotient extension theorem. Quotient extension theorems
     allow for quotienting inside container types. Given a polymorphic
     type that serves as a container, a map function defined for this
-    container  using @{command (HOL) "enriched_type"} and a relation
+    container using @{command (HOL) "enriched_type"} and a relation
     map defined for for the container type, the quotient extension
-    theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
+    theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3
     (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
     are stored in a database and are used all the steps of lifting
     theorems.
@@ -1740,6 +1740,15 @@
     \item[@{text no_assms}] specifies whether assumptions in
     structured proofs should be ignored.
 
+    \item[@{text locale}] specifies how to process conjectures in
+    a locale context, i.e., they can be interpreted or expanded.
+    The option is a whitespace-separated list of the two words
+    @{text interpret} and @{text expand}. The list determines the
+    order they are employed. The default setting is to first use 
+    interpretations and then test the expanded conjecture.
+    The option is only provided as attribute declaration, but not
+    as parameter to the command. 
+
     \item[@{text timeout}] sets the time limit in seconds.
 
     \item[@{text default_type}] sets the type(s) generally used to
diff -r e0bff2ae939f -r fc7de207e488 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Apr 04 11:50:08 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Apr 04 14:27:20 2012 +0200
@@ -1959,9 +1959,9 @@
     is a quotient extension theorem. Quotient extension theorems
     allow for quotienting inside container types. Given a polymorphic
     type that serves as a container, a map function defined for this
-    container  using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
+    container using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
     map defined for for the container type, the quotient extension
-    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
+    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient{\isadigit{3}}\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient{\isadigit{3}}\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
     are stored in a database and are used all the steps of lifting
     theorems.
 
@@ -2504,6 +2504,15 @@
     \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in
     structured proofs should be ignored.
 
+    \item[\isa{locale}] specifies how to process conjectures in
+    a locale context, i.e., they can be interpreted or expanded.
+    The option is a whitespace-separated list of the two words
+    \isa{interpret} and \isa{expand}. The list determines the
+    order they are employed. The default setting is to first use 
+    interpretations and then test the expanded conjecture.
+    The option is only provided as attribute declaration, but not
+    as parameter to the command. 
+
     \item[\isa{timeout}] sets the time limit in seconds.
 
     \item[\isa{default{\isaliteral{5F}{\isacharunderscore}}type}] sets the type(s) generally used to
diff -r e0bff2ae939f -r fc7de207e488 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Apr 04 11:50:08 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Apr 04 14:27:20 2012 +0200
@@ -69,7 +69,7 @@
 
 lemma "app (fs @ gs) x = app gs (app fs x)"
   quickcheck[random, expect = no_counterexample]
-  quickcheck[exhaustive, size = 4, expect = no_counterexample]
+  quickcheck[exhaustive, size = 2, expect = no_counterexample]
   by (induct fs arbitrary: x) simp_all
 
 lemma "app (fs @ gs) x = app fs (app gs x)"
@@ -477,15 +477,31 @@
 locale antisym =
   fixes R
   assumes "R x y --> R y x --> x = y"
-begin
 
-lemma
+interpretation equal : antisym "op =" by default simp
+interpretation order_nat : antisym "op <= :: nat => _ => _" by default simp
+
+lemma (in antisym)
   "R x y --> R y z --> R x z"
 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
 quickcheck[exhaustive, expect = counterexample]
 oops
 
-end
+declare [[quickcheck_locale = "interpret"]]
+
+lemma (in antisym)
+  "R x y --> R y z --> R x z"
+quickcheck[exhaustive, expect = no_counterexample]
+oops
+
+declare [[quickcheck_locale = "expand"]]
+
+lemma (in antisym)
+  "R x y --> R y z --> R x z"
+quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
 
 subsection {* Examples with HOL quantifiers *}
 
diff -r e0bff2ae939f -r fc7de207e488 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Apr 04 11:50:08 2012 +0200
+++ b/src/Tools/quickcheck.ML	Wed Apr 04 14:27:20 2012 +0200
@@ -30,6 +30,7 @@
   val finite_types : bool Config.T
   val finite_type_size : int Config.T
   val tag : string Config.T
+  val locale : string Config.T
   val set_active_testers: string list -> Context.generic -> Context.generic
   datatype expectation = No_Expectation | No_Counterexample | Counterexample;
   datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
@@ -176,6 +177,7 @@
 val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10)
 
 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
+val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand")
 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
@@ -336,6 +338,15 @@
     all t
   end
 
+fun locale_config_of s =
+  let
+    val cs = space_explode " " s
+  in
+    if forall (fn c => c = "expand" orelse c = "interpret") cs then cs
+    else (Output.warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
+      ["interpret", "expand"])
+  end
+
 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   let
     val lthy = Proof.context_of state;
@@ -356,12 +367,14 @@
     fun axioms_of locale = case fst (Locale.specification_of thy locale) of
         NONE => []
       | SOME t => the_default [] (all_axioms_of lthy t)
-    val goals = case some_locale
+   val config = locale_config_of (Config.get lthy locale) 
+   val goals = case some_locale
      of NONE => [(proto_goal, eval_terms)]
-      | SOME locale =>
-          (Logic.list_implies (axioms_of locale, proto_goal), eval_terms) ::
-          map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
-          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
+      | SOME locale => fold (fn c =>
+          if c = "expand" then cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms) else
+          if c = "interpret" then
+            append (map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
+          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale)) else I) config [];
     val _ = verbose_message lthy (Pretty.string_of
       (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term lthy o fst) goals)))
   in