# HG changeset patch # User haftmann # Date 1228316396 -3600 # Node ID 48cd567f6940f10c5d9323ce611a19c91dc72cb8 # Parent 15a4b2cf8c34418bb8dffa7b5e7b48434d3e72e4# Parent e89dde5f365c31f59a06d879742b8f6382a16bfc merged diff -r 15a4b2cf8c34 -r 48cd567f6940 src/HOL/ex/Sudoku.thy --- 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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 diff -r 15a4b2cf8c34 -r 48cd567f6940 src/Pure/Isar/expression.ML --- 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; diff -r 15a4b2cf8c34 -r 48cd567f6940 src/Pure/Isar/isar_syn.ML --- 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.$$$ "\\" || 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" diff -r 15a4b2cf8c34 -r 48cd567f6940 src/Pure/Isar/locale.ML --- 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 = diff -r 15a4b2cf8c34 -r 48cd567f6940 src/Pure/Isar/new_locale.ML --- 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