--- a/src/HOL/ex/Sudoku.thy Wed Dec 03 15:58:44 2008 +0100
+++ b/src/HOL/ex/Sudoku.thy Wed Dec 03 15:59:56 2008 +0100
@@ -1,7 +1,7 @@
(* Title: Sudoku.thy
ID: $Id$
Author: Tjark Weber
- Copyright 2005-2007
+ Copyright 2005-2008
*)
header {* A SAT-based Sudoku Solver *}
@@ -11,9 +11,12 @@
begin
text {*
- Please make sure you are using an efficient SAT solver (e.g. zChaff)
+ Please make sure you are using an efficient SAT solver (e.g., zChaff)
when loading this theory. See Isabelle's settings file for details.
+ Using zChaff, each Sudoku in this theory is solved in less than a
+ second.
+
See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
LPAR'05) for further explanations.
*}
@@ -135,4 +138,180 @@
refute
oops
+text {*
+ Some "exceptionally difficult" Sudokus, taken from
+ \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}
+ (accessed December 2, 2008).
+*}
+
+text {*
+\begin{verbatim}
+Rating Program: gsf's sudoku q1 (rating)
+Rating: 99408
+Poster: JPF
+Label: Easter Monster
+1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1
+1 . . | . . . | . . 2
+. 9 . | 4 . . | . 5 .
+. . 6 | . . . | 7 . .
+------+-------+------
+. 5 . | 9 . 3 | . . .
+. . . | . 7 . | . . .
+. . . | 8 5 . | . 4 .
+------+-------+------
+7 . . | . . . | 6 . .
+. 3 . | . . 9 | . 8 .
+. . 2 | . . . | . . 1
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ 1 x12 x13 x14 x15 x16 x17 x18 2
+ x21 9 x23 4 x25 x26 x27 5 x29
+ x31 x32 6 x34 x35 x36 7 x38 x39
+ x41 5 x43 9 x45 3 x47 x48 x49
+ x51 x52 x53 x54 7 x56 x57 x58 x59
+ x61 x62 x63 8 5 x66 x67 4 x69
+ 7 x72 x73 x74 x75 x76 6 x78 x79
+ x81 3 x83 x84 x85 9 x87 8 x89
+ x91 x92 2 x94 x95 x96 x97 x98 1 "
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: gsf's sudoku q1 (Processing time)
+Rating: 4m19s@2 GHz
+Poster: tarek
+Label: tarek071223170000-052
+..1..4.......6.3.5...9.....8.....7.3.......285...7.6..3...8...6..92......4...1...
+. . 1 | . . 4 | . . .
+. . . | . 6 . | 3 . 5
+. . . | 9 . . | . . .
+------+-------+------
+8 . . | . . . | 7 . 3
+. . . | . . . | . 2 8
+5 . . | . 7 . | 6 . .
+------+-------+------
+3 . . | . 8 . | . . 6
+. . 9 | 2 . . | . . .
+. 4 . | . . 1 | . . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 x12 1 x14 x15 4 x17 x18 x19
+ x21 x22 x23 x24 6 x26 3 x28 5
+ x31 x32 x33 9 x35 x36 x37 x38 x39
+ 8 x42 x43 x44 x45 x46 7 x48 3
+ x51 x52 x53 x54 x55 x56 x57 2 8
+ 5 x62 x63 x64 7 x66 6 x68 x69
+ 3 x72 x73 x74 8 x76 x77 x78 6
+ x81 x82 9 2 x85 x86 x87 x88 x89
+ x91 4 x93 x94 x95 1 x97 x98 x99"
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1
+Rating: 11.9
+Poster: tarek
+Label: golden nugget
+.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....
+. . . | . . . | . 3 9
+. . . | . . 1 | . . 5
+. . 3 | . 5 . | 8 . .
+------+-------+------
+. . 8 | . 9 . | . . 6
+. 7 . | . . 2 | . . .
+1 . . | 4 . . | . . .
+------+-------+------
+. . 9 | . 8 . | . 5 .
+. 2 . | . . . | 6 . .
+4 . . | 7 . . | . . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 x12 x13 x14 x15 x16 x17 3 9
+ x21 x22 x23 x24 x25 1 x27 x28 5
+ x31 x32 3 x34 5 x36 8 x38 x39
+ x41 x42 8 x44 9 x46 x47 x48 6
+ x51 7 x53 x54 x55 2 x57 x58 x59
+ 1 x62 x63 4 x65 x66 x67 x68 x69
+ x71 x72 9 x74 8 x76 x77 5 x79
+ x81 2 x83 x84 x85 x86 6 x88 x89
+ 4 x92 x93 7 x95 x96 x97 x98 x99"
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: dukuso's suexrat9
+Rating: 4483
+Poster: coloin
+Label: col-02-08-071
+.2.4.37.........32........4.4.2...7.8...5.........1...5.....9...3.9....7..1..86..
+. 2 . | 4 . 3 | 7 . .
+. . . | . . . | . 3 2
+. . . | . . . | . . 4
+------+-------+------
+. 4 . | 2 . . | . 7 .
+8 . . | . 5 . | . . .
+. . . | . . 1 | . . .
+------+-------+------
+5 . . | . . . | 9 . .
+. 3 . | 9 . . | . . 7
+. . 1 | . . 8 | 6 . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 2 x13 4 x15 3 7 x18 x19
+ x21 x22 x23 x24 x25 x26 x27 3 2
+ x31 x32 x33 x34 x35 x36 x37 x38 4
+ x41 4 x43 2 x45 x46 x47 7 x49
+ 8 x52 x53 x54 5 x56 x57 x58 x59
+ x61 x62 x63 x64 x65 1 x67 x68 x69
+ 5 x72 x73 x74 x75 x76 9 x78 x79
+ x81 3 x83 9 x85 x86 x87 x88 7
+ x91 x92 1 x94 x95 8 6 x98 x99"
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: dukuso's suexratt (10000 2 option)
+Rating: 2141
+Poster: tarek
+Label: golden nugget
+.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....
+. . . | . . . | . 3 9
+. . . | . . 1 | . . 5
+. . 3 | . 5 . | 8 . .
+------+-------+------
+. . 8 | . 9 . | . . 6
+. 7 . | . . 2 | . . .
+1 . . | 4 . . | . . .
+------+-------+------
+. . 9 | . 8 . | . 5 .
+. 2 . | . . . | 6 . .
+4 . . | 7 . . | . . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 x12 x13 x14 x15 x16 x17 3 9
+ x21 x22 x23 x24 x25 1 x27 x28 5
+ x31 x32 3 x34 5 x36 8 x38 x39
+ x41 x42 8 x44 9 x46 x47 x48 6
+ x51 7 x53 x54 x55 2 x57 x58 x59
+ 1 x62 x63 4 x65 x66 x67 x68 x69
+ x71 x72 9 x74 8 x76 x77 5 x79
+ x81 2 x83 x84 x85 x86 6 x88 x89
+ 4 x92 x93 7 x95 x96 x97 x98 x99"
+ refute
+oops
+
end
--- a/src/Pure/Isar/expression.ML Wed Dec 03 15:58:44 2008 +0100
+++ b/src/Pure/Isar/expression.ML Wed Dec 03 15:59:56 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/expression.ML
- ID: $Id$
Author: Clemens Ballarin, TU Muenchen
New locale development --- experimental.
@@ -25,10 +24,8 @@
string * Proof.context
(* Interpretation *)
- val sublocale_cmd: (thm list list -> Proof.context -> Proof.context) ->
- string -> expression -> theory -> Proof.state;
- val sublocale: (thm list list -> Proof.context -> Proof.context) ->
- string -> expression_i -> theory -> Proof.state;
+ val sublocale_cmd: string -> expression -> theory -> Proof.state;
+ val sublocale: string -> expression_i -> theory -> Proof.state;
(* Debugging and development *)
val parse_expression: OuterParse.token list -> expression * OuterParse.token list
@@ -434,7 +431,7 @@
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
+ fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = NewLocale.params_of thy loc |>
map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
@@ -443,11 +440,11 @@
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
val inst'' = map2 TypeInfer.constrain parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
- val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
+ val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
- val (marked', ctxt'') = NewLocale.activate_declarations thy (loc, morph) (marked, ctxt);
- in (i+1, marked', insts', ctxt'') end;
+ val ctxt'' = NewLocale.activate_declarations thy (loc, morph) ctxt;
+ in (i+1, insts', ctxt'') end;
fun prep_elem raw_elem (insts, elems, ctxt) =
let
@@ -465,7 +462,7 @@
val fors = prep_vars fixed context |> fst;
val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
- val (_, _, insts', ctxt') = fold prep_inst raw_insts (0, NewLocale.empty, [], ctxt);
+ val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_idents ctxt);
val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
@@ -542,7 +539,7 @@
(* Declare parameters and imported facts *)
val context' = context |>
ProofContext.add_fixes_i fixed |> snd |>
- pair NewLocale.empty |> fold (NewLocale.activate_facts thy) deps |> snd;
+ NewLocale.clear_idents |> fold (NewLocale.activate_facts thy) deps;
val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
in ((fixed, deps, elems'), (parms, spec, defs)) end;
@@ -804,7 +801,7 @@
local
fun gen_sublocale prep_expr intern
- after_qed raw_target expression thy =
+ raw_target expression thy =
let
val target = intern thy raw_target;
val target_ctxt = NewLocale.init target thy;
@@ -814,13 +811,10 @@
fun store_dep ((name, morph), thms) =
NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
- fun after_qed' results =
- fold store_dep (deps ~~ prep_result propss results) #>
- after_qed results;
-
+ fun after_qed results = fold store_dep (deps ~~ prep_result propss results);
in
goal_ctxt |>
- Proof.theorem_i NONE after_qed' (prep_propp propss) |>
+ Proof.theorem_i NONE after_qed (prep_propp propss) |>
Element.refine_witness |> Seq.hd
end;
--- a/src/Pure/Isar/isar_syn.ML Wed Dec 03 15:58:44 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Dec 03 15:59:56 2008 +0100
@@ -403,7 +403,7 @@
"prove sublocale relation between a locale and a locale expression" K.thy_goal
(P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
>> (fn (loc, expr) =>
- Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd (K I) loc expr))));
+ Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
val _ =
OuterSyntax.command "interpretation"
--- a/src/Pure/Isar/locale.ML Wed Dec 03 15:58:44 2008 +0100
+++ b/src/Pure/Isar/locale.ML Wed Dec 03 15:59:56 2008 +0100
@@ -91,6 +91,9 @@
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Storing results *)
+ val global_note_qualified: string ->
+ ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+ theory -> (string * thm list) list * theory
val local_note_qualified: string ->
((Name.binding * attribute list) * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
@@ -2409,7 +2412,6 @@
ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
- (* prfx = (flag indicating full qualification, name prefix) *)
let
val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
fun after_qed' results =
--- a/src/Pure/Isar/new_locale.ML Wed Dec 03 15:58:44 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Wed Dec 03 15:59:56 2008 +0100
@@ -1,5 +1,4 @@
-(* Title: Pure/Isar/expression.ML
- ID: $Id$
+(* Title: Pure/Isar/new_locale.ML
Author: Clemens Ballarin, TU Muenchen
New locale development --- experimental.
@@ -7,11 +6,9 @@
signature NEW_LOCALE =
sig
- type identifiers
- val empty: identifiers
-
type locale
+ val clear_idents: Proof.context -> Proof.context
val test_locale: theory -> string -> bool
val register_locale: string ->
(string * sort) list * (Name.binding * typ option * mixfix) list ->
@@ -39,9 +36,9 @@
(* Activation *)
val activate_declarations: theory -> string * Morphism.morphism ->
- identifiers * Proof.context -> identifiers * Proof.context
+ Proof.context -> Proof.context
val activate_facts: theory -> string * Morphism.morphism ->
- identifiers * Proof.context -> identifiers * Proof.context
+ Proof.context -> Proof.context
(* val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
val init: string -> theory -> Proof.context
@@ -57,6 +54,8 @@
end;
+(*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
+
(* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
functor ThmsFun() =
struct
@@ -184,15 +183,36 @@
(*** Activate context elements of locale ***)
-(** Resolve locale dependencies in a depth-first fashion **)
+(** Identifiers: activated locales in theory or proof context **)
type identifiers = (string * term list) list;
val empty = ([] : identifiers);
+fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+
local
-fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+structure IdentifiersData = GenericDataFun
+(
+ type T = identifiers;
+ val empty = empty;
+ val extend = I;
+ fun merge _ = Library.merge (op =); (* FIXME cannot do this properly without theory context *)
+);
+
+in
+
+val get_idents = IdentifiersData.get o Context.Proof;
+val put_idents = Context.proof_map o IdentifiersData.put;
+val clear_idents = put_idents empty;
+
+end;
+
+
+(** Resolve locale dependencies in a depth-first fashion **)
+
+local
val roundup_bound = 120;
@@ -220,18 +240,17 @@
in
-fun roundup thy activate_dep (name, morph) (marked, ctxt) =
+fun roundup thy activate_dep (name, morph) (marked, input) =
let
- val Loc {dependencies, ...} = the_locale thy name;
val (dependencies', marked') = add thy 0 (name, morph) ([], marked);
in
- (marked', ctxt |> fold_rev (activate_dep thy) dependencies')
+ (marked', input |> fold_rev (activate_dep thy) dependencies')
end;
end;
-(* Declarations and facts *)
+(* Declarations, facts and entire locale content *)
fun activate_decls thy (name, morph) ctxt =
let
@@ -252,10 +271,7 @@
fold_rev activate notes input
end;
-
-(* Entire locale content *)
-
-fun activate name thy activ_elem input =
+fun activate_all name thy activ_elem (marked, input) =
let
val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
the_locale thy name;
@@ -267,7 +283,7 @@
(if not (null defs)
then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
else I) |>
- pair empty |> roundup thy (activate_notes activ_elem) (name, Morphism.identity) |> snd
+ pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
end;
@@ -302,11 +318,14 @@
in
-fun activate_declarations thy = roundup thy activate_decls;
+fun activate_declarations thy dep ctxt =
+ roundup thy activate_decls dep (get_idents ctxt, ctxt) |> uncurry put_idents;
+
+fun activate_facts thy dep ctxt =
+ roundup thy (activate_notes init_elem) dep (get_idents ctxt, ctxt) |> uncurry put_idents;
-fun activate_facts thy = roundup thy (activate_notes init_elem);
-
-fun init name thy = activate name thy init_elem (ProofContext.init thy);
+fun init name thy = activate_all name thy init_elem (empty, ProofContext.init thy) |>
+ uncurry put_idents;
fun print_locale thy show_facts name =
let
@@ -314,7 +333,7 @@
val ctxt = init name' thy
in
Pretty.big_list "locale elements:"
- (activate name' thy (cons_elem show_facts) [] |> rev |>
+ (activate_all name' thy (cons_elem show_facts) (empty, []) |> snd |> rev |>
map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
end