# HG changeset patch # User wenzelm # Date 1268162599 -3600 # Node ID 86e48f81492b7ff906eaa5ddceb6360d625e8d3b # Parent b6720fe8afa795004e3b282b0e42dd7e40c7c4c6# Parent 3007b46c1660d754cb7e73ec3258bb40cbab912e merged diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Divides.thy Tue Mar 09 20:23:19 2010 +0100 @@ -376,7 +376,7 @@ end -class ring_div = semiring_div + idom +class ring_div = semiring_div + comm_ring_1 begin text {* Negation respects modular equivalence. *} @@ -2353,47 +2353,6 @@ apply (rule Divides.div_less_dividend, simp_all) done -text {* code generator setup *} - -context ring_1 -begin - -lemma of_int_num [code]: - "of_int k = (if k = 0 then 0 else if k < 0 then - - of_int (- k) else let - (l, m) = divmod_int k 2; - l' = of_int l - in if m = 0 then l' + l' else l' + l' + 1)" -proof - - have aux1: "k mod (2\int) \ (0\int) \ - of_int k = of_int (k div 2 * 2 + 1)" - proof - - have "k mod 2 < 2" by (auto intro: pos_mod_bound) - moreover have "0 \ k mod 2" by (auto intro: pos_mod_sign) - moreover assume "k mod 2 \ 0" - ultimately have "k mod 2 = 1" by arith - moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp - ultimately show ?thesis by auto - qed - have aux2: "\x. of_int 2 * x = x + x" - proof - - fix x - have int2: "(2::int) = 1 + 1" by arith - show "of_int 2 * x = x + x" - unfolding int2 of_int_add left_distrib by simp - qed - have aux3: "\x. x * of_int 2 = x + x" - proof - - fix x - have int2: "(2::int) = 1 + 1" by arith - show "x * of_int 2 = x + x" - unfolding int2 of_int_add right_distrib by simp - qed - from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3) -qed - -end - lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \ n dvd x - y" proof assume H: "x mod n = y mod n" @@ -2482,6 +2441,7 @@ mod_div_equality' [THEN eq_reflection] zmod_zdiv_equality' [THEN eq_reflection] + subsubsection {* Code generation *} definition pdivmod :: "int \ int \ int \ int" where @@ -2515,6 +2475,45 @@ then show ?thesis by (simp add: divmod_int_pdivmod) qed +context ring_1 +begin + +lemma of_int_num [code]: + "of_int k = (if k = 0 then 0 else if k < 0 then + - of_int (- k) else let + (l, m) = divmod_int k 2; + l' = of_int l + in if m = 0 then l' + l' else l' + l' + 1)" +proof - + have aux1: "k mod (2\int) \ (0\int) \ + of_int k = of_int (k div 2 * 2 + 1)" + proof - + have "k mod 2 < 2" by (auto intro: pos_mod_bound) + moreover have "0 \ k mod 2" by (auto intro: pos_mod_sign) + moreover assume "k mod 2 \ 0" + ultimately have "k mod 2 = 1" by arith + moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp + ultimately show ?thesis by auto + qed + have aux2: "\x. of_int 2 * x = x + x" + proof - + fix x + have int2: "(2::int) = 1 + 1" by arith + show "of_int 2 * x = x + x" + unfolding int2 of_int_add left_distrib by simp + qed + have aux3: "\x. x * of_int 2 = x + x" + proof - + fix x + have int2: "(2::int) = 1 + 1" by arith + show "x * of_int 2 = x + x" + unfolding int2 of_int_add right_distrib by simp + qed + from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3) +qed + +end + code_modulename SML Divides Arith diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Nitpick.thy Tue Mar 09 20:23:19 2010 +0100 @@ -36,7 +36,8 @@ and bisim :: "bisim_iterator \ 'a \ 'a \ bool" and bisim_iterator_max :: bisim_iterator and Quot :: "'a \ 'b" - and Tha :: "('a \ bool) \ 'a" + and safe_The :: "('a \ bool) \ 'a" + and safe_Eps :: "('a \ bool) \ 'a" datatype ('a, 'b) fin_fun = FinFun "('a \ 'b)" datatype ('a, 'b) fun_box = FunBox "('a \ 'b)" @@ -237,10 +238,11 @@ setup {* Nitpick_Isar.setup *} hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim - bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec - wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm - Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac - times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac + bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl' + wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm + int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom + norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac + less_eq_frac of_frac hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit word hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Nitpick_Examples/Induct_Nits.thy --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 20:23:19 2010 +0100 @@ -61,7 +61,7 @@ lemma "q2 = {}" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] -nitpick [wf, expect = likely_genuine] +nitpick [wf, expect = quasi_genuine] oops lemma "p2 = UNIV" @@ -72,7 +72,7 @@ lemma "q2 = UNIV" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] -nitpick [wf, expect = likely_genuine] +nitpick [wf, expect = quasi_genuine] sorry lemma "p2 = q2" diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 20:23:19 2010 +0100 @@ -18,29 +18,29 @@ subsection {* 3.1. Propositional Logic *} lemma "P \ Q" -nitpick +nitpick [expect = genuine] apply auto -nitpick 1 -nitpick 2 +nitpick [expect = genuine] 1 +nitpick [expect = genuine] 2 oops subsection {* 3.2. Type Variables *} lemma "P x \ P (THE y. P y)" -nitpick [verbose] +nitpick [verbose, expect = genuine] oops subsection {* 3.3. Constants *} lemma "P x \ P (THE y. P y)" -nitpick [show_consts] -nitpick [full_descrs, show_consts] -nitpick [dont_specialize, full_descrs, show_consts] +nitpick [show_consts, expect = genuine] +nitpick [full_descrs, show_consts, expect = genuine] +nitpick [dont_specialize, full_descrs, show_consts, expect = genuine] oops lemma "\!x. P x \ P (THE y. P y)" -nitpick -nitpick [card 'a = 1-50] +nitpick [expect = none] +nitpick [card 'a = 1\50, expect = none] (* sledgehammer *) apply (metis the_equality) done @@ -48,45 +48,45 @@ subsection {* 3.4. Skolemization *} lemma "\g. \x. g (f x) = x \ \y. \x. y = f x" -nitpick +nitpick [expect = genuine] oops lemma "\x. \f. f x = x" -nitpick +nitpick [expect = genuine] oops lemma "refl r \ sym r" -nitpick +nitpick [expect = genuine] oops subsection {* 3.5. Natural Numbers and Integers *} lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ i * m + j * n" -nitpick +nitpick [expect = genuine] oops lemma "\n. Suc n \ n \ P" -nitpick [card nat = 100, check_potential] +nitpick [card nat = 100, check_potential, expect = genuine] oops lemma "P Suc" -nitpick +nitpick [expect = none] oops lemma "P (op +\nat\nat\nat)" -nitpick [card nat = 1] -nitpick [card nat = 2] +nitpick [card nat = 1, expect = genuine] +nitpick [card nat = 2, expect = none] oops subsection {* 3.6. Inductive Datatypes *} lemma "hd (xs @ [y, y]) = hd xs" -nitpick -nitpick [show_consts, show_datatypes] +nitpick [expect = genuine] +nitpick [show_consts, show_datatypes, expect = genuine] oops lemma "\length xs = 1; length ys = 1\ \ xs = ys" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops subsection {* 3.7. Typedefs, Records, Rationals, and Reals *} @@ -99,7 +99,7 @@ definition C :: three where "C \ Abs_three 2" lemma "\P A; P B\ \ P x" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops fun my_int_rel where @@ -114,7 +114,7 @@ quotient_definition "add\my_int \ my_int \ my_int" is add_raw lemma "add x y = add x x" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops record point = @@ -122,11 +122,11 @@ Ycoord :: int lemma "Xcoord (p\point) = Xcoord (q\point)" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops lemma "4 * x + 3 * (y\real) \ 1 / 2" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops subsection {* 3.8. Inductive and Coinductive Predicates *} @@ -136,11 +136,11 @@ "even n \ even (Suc (Suc n))" lemma "\n. even n \ even (Suc n)" -nitpick [card nat = 100, unary_ints, verbose] +nitpick [card nat = 100, unary_ints, verbose, expect = potential] oops lemma "\n \ 99. even n \ even (Suc n)" -nitpick [card nat = 100, unary_ints, verbose] +nitpick [card nat = 100, unary_ints, verbose, expect = genuine] oops inductive even' where @@ -149,18 +149,18 @@ "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" -nitpick [card nat = 10, unary_ints, verbose, show_consts] +nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine] oops lemma "even' (n - 2) \ even' n" -nitpick [card nat = 10, show_consts] +nitpick [card nat = 10, show_consts, expect = genuine] oops coinductive nats where "nats (x\nat) \ nats x" lemma "nats = {0, 1, 2, 3, 4}" -nitpick [card nat = 10, show_consts] +nitpick [card nat = 10, show_consts, expect = genuine] oops inductive odd where @@ -168,7 +168,7 @@ "\odd m; even n\ \ odd (m + n)" lemma "odd n \ odd (n - 2)" -nitpick [card nat = 10, show_consts] +nitpick [card nat = 10, show_consts, expect = genuine] oops subsection {* 3.9. Coinductive Datatypes *} @@ -179,7 +179,8 @@ typedef 'a llist = "UNIV\('a list + (nat \ 'a)) set" by auto -definition LNil where "LNil = Abs_llist (Inl [])" +definition LNil where +"LNil = Abs_llist (Inl [])" definition LCons where "LCons y ys = Abs_llist (case Rep_llist ys of Inl ys' \ Inl (y # ys') @@ -197,16 +198,16 @@ *} lemma "xs \ LCons a xs" -nitpick +nitpick [expect = genuine] oops lemma "\xs = LCons a xs; ys = iterates (\b. a) b\ \ xs = ys" -nitpick [verbose] +nitpick [verbose, expect = genuine] oops lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" -nitpick [bisim_depth = -1, show_datatypes] -nitpick +nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] +nitpick [expect = none] sorry subsection {* 3.10. Boxing *} @@ -230,9 +231,9 @@ "subst\<^isub>1 \ (App t u) = App (subst\<^isub>1 \ t) (subst\<^isub>1 \ u)" lemma "\ loose t 0 \ subst\<^isub>1 \ t = t" -nitpick [verbose] -nitpick [eval = "subst\<^isub>1 \ t"] -(* nitpick [dont_box] *) +nitpick [verbose, expect = genuine] +nitpick [eval = "subst\<^isub>1 \ t", expect = genuine] +(* nitpick [dont_box, expect = unknown] *) oops primrec subst\<^isub>2 where @@ -242,19 +243,19 @@ "subst\<^isub>2 \ (App t u) = App (subst\<^isub>2 \ t) (subst\<^isub>2 \ u)" lemma "\ loose t 0 \ subst\<^isub>2 \ t = t" -nitpick [card = 1\6] +nitpick [card = 1\6, expect = none] sorry subsection {* 3.11. Scope Monotonicity *} lemma "length xs = length ys \ rev (zip xs ys) = zip xs (rev ys)" -nitpick [verbose] -nitpick [card = 8, verbose] +nitpick [verbose, expect = genuine] +nitpick [card = 8, verbose, expect = genuine] oops lemma "\g. \x\'b. g (f x) = x \ \y\'a. \x. y = f x" -nitpick [mono] -nitpick +nitpick [mono, expect = none] +nitpick [expect = genuine] oops subsection {* 3.12. Inductive Properties *} @@ -265,21 +266,21 @@ "n \ reach \ n + 2 \ reach" lemma "n \ reach \ 2 dvd n" -nitpick [unary_ints] +nitpick [unary_ints, expect = none] apply (induct set: reach) apply auto - nitpick + nitpick [expect = none] apply (thin_tac "n \ reach") - nitpick + nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 0" -nitpick [unary_ints] +nitpick [unary_ints, expect = none] apply (induct set: reach) apply auto - nitpick + nitpick [expect = none] apply (thin_tac "n \ reach") - nitpick + nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 4" @@ -297,13 +298,13 @@ "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" lemma "{a, b} \ labels t \ labels (swap t a b) = labels t" -nitpick +(* nitpick *) proof (induct t) case Leaf thus ?case by simp next case (Branch t u) thus ?case - nitpick - nitpick [non_std, show_all] + (* nitpick *) + nitpick [non_std, show_all, expect = genuine] oops lemma "labels (swap t a b) = @@ -338,7 +339,7 @@ theorem S\<^isub>1_sound: "w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick +nitpick [expect = genuine] oops inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where @@ -351,7 +352,7 @@ theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick +nitpick [expect = genuine] oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where @@ -369,7 +370,7 @@ theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" -nitpick +nitpick [expect = genuine] oops inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where @@ -465,11 +466,11 @@ (if x > y then insort\<^isub>1 u x else u))" theorem wf_insort\<^isub>1: "wf t \ wf (insort\<^isub>1 t x)" -nitpick +nitpick [expect = genuine] oops theorem wf_insort\<^isub>1_nat: "wf t \ wf (insort\<^isub>1 t (x\nat))" -nitpick [eval = "insort\<^isub>1 t x"] +nitpick [eval = "insort\<^isub>1 t x", expect = genuine] oops primrec insort\<^isub>2 where diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 20:23:19 2010 +0100 @@ -2,13 +2,13 @@ * Added and implemented "binary_ints" and "bits" options * Added "std" option and implemented support for nonstandard models + * Added and implemented "finitize" option to improve the precision of infinite + datatypes based on a monotonicity analysis * Added support for quotient types - * Added support for local definitions - * Disabled "fast_descrs" option by default + * Added support for local definitions (for "function" and "termination" + proofs) * Optimized "Multiset.multiset" and "FinFun.finfun" * Improved efficiency of "destroy_constrs" optimization - * Improved precision of infinite datatypes whose constructors don't appear - in the formula to falsify based on a monotonicity analysis * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 20:23:19 2010 +0100 @@ -326,8 +326,6 @@ val sound_finitizes = none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true | _ => false) finitizes) - val genuine_means_genuine = - got_all_user_axioms andalso none_true wfs andalso sound_finitizes val standard = forall snd stds (* val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us) @@ -603,7 +601,7 @@ fun show_kodkod_warning "" = () | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") - (* bool -> KK.raw_bound list -> problem_extension -> bool option *) + (* bool -> KK.raw_bound list -> problem_extension -> bool * bool option *) fun print_and_check_model genuine bounds ({free_names, sel_names, nonsel_names, rel_table, scope, ...} : problem_extension) = @@ -614,119 +612,126 @@ show_consts = show_consts} scope formats frees free_names sel_names nonsel_names rel_table bounds - val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok + val genuine_means_genuine = + got_all_user_axioms andalso none_true wfs andalso + sound_finitizes andalso codatatypes_ok in - pprint (Pretty.chunks - [Pretty.blk (0, - (pstrs ("Nitpick found a" ^ - (if not genuine then " potential " - else if genuine_means_genuine then " " - else " likely genuine ") ^ das_wort_model) @ - (case pretties_for_scope scope verbose of - [] => [] - | pretties => pstrs " for " @ pretties) @ - [Pretty.str ":\n"])), - Pretty.indent indent_size reconstructed_model]); - if genuine then - (if check_genuine andalso standard then - (case prove_hol_model scope tac_timeout free_names sel_names + (pprint (Pretty.chunks + [Pretty.blk (0, + (pstrs ("Nitpick found a" ^ + (if not genuine then " potential " + else if genuine_means_genuine then " " + else " quasi genuine ") ^ das_wort_model) @ + (case pretties_for_scope scope verbose of + [] => [] + | pretties => pstrs " for " @ pretties) @ + [Pretty.str ":\n"])), + Pretty.indent indent_size reconstructed_model]); + if genuine then + (if check_genuine andalso standard then + case prove_hol_model scope tac_timeout free_names sel_names rel_table bounds assms_t of - SOME true => print ("Confirmation by \"auto\": The above " ^ - das_wort_model ^ " is really genuine.") + SOME true => + print ("Confirmation by \"auto\": The above " ^ + das_wort_model ^ " is really genuine.") | SOME false => if genuine_means_genuine then error ("A supposedly genuine " ^ das_wort_model ^ " was \ \shown to be spurious by \"auto\".\nThis should never \ \happen.\nPlease send a bug report to blanchet\ \te@in.tum.de.") - else - print ("Refutation by \"auto\": The above " ^ das_wort_model ^ - " is spurious.") - | NONE => print "No confirmation by \"auto\".") - else - (); - if not standard andalso likely_in_struct_induct_step then - print "The existence of a nonstandard model suggests that the \ - \induction hypothesis is not general enough or perhaps even \ - \wrong. See the \"Inductive Properties\" section of the \ - \Nitpick manual for details (\"isabelle doc nitpick\")." - else - (); - if has_syntactic_sorts orig_t then - print "Hint: Maybe you forgot a type constraint?" + else + print ("Refutation by \"auto\": The above " ^ + das_wort_model ^ " is spurious.") + | NONE => print "No confirmation by \"auto\"." + else + (); + if not standard andalso likely_in_struct_induct_step then + print "The existence of a nonstandard model suggests that the \ + \induction hypothesis is not general enough or perhaps \ + \even wrong. See the \"Inductive Properties\" section of \ + \the Nitpick manual for details (\"isabelle doc nitpick\")." + else + (); + if has_syntactic_sorts orig_t then + print "Hint: Maybe you forgot a type constraint?" + else + (); + if not genuine_means_genuine then + if no_poly_user_axioms then + let + val options = + [] |> not got_all_mono_user_axioms + ? cons ("user_axioms", "\"true\"") + |> not (none_true wfs) + ? cons ("wf", "\"smart\" or \"false\"") + |> not sound_finitizes + ? cons ("finitize", "\"smart\" or \"false\"") + |> not codatatypes_ok + ? cons ("bisim_depth", "a nonnegative value") + val ss = + map (fn (name, value) => quote name ^ " set to " ^ value) + options + in + print ("Try again with " ^ + space_implode " " (serial_commas "and" ss) ^ + " to confirm that the " ^ das_wort_model ^ + " is genuine.") + end + else + print ("Nitpick is unable to guarantee the authenticity of \ + \the " ^ das_wort_model ^ " in the presence of \ + \polymorphic axioms.") + else + (); + NONE) + else + if not genuine then + (Unsynchronized.inc met_potential; + if check_potential then + let + val status = prove_hol_model scope tac_timeout free_names + sel_names rel_table bounds assms_t + in + (case status of + SOME true => print ("Confirmation by \"auto\": The \ + \above " ^ das_wort_model ^ + " is genuine.") + | SOME false => print ("Refutation by \"auto\": The above " ^ + das_wort_model ^ " is spurious.") + | NONE => print "No confirmation by \"auto\"."); + status + end + else + NONE) else - (); - if not genuine_means_genuine then - if no_poly_user_axioms then - let - val options = - [] |> not got_all_mono_user_axioms - ? cons ("user_axioms", "\"true\"") - |> not (none_true wfs) - ? cons ("wf", "\"smart\" or \"false\"") - |> not sound_finitizes - ? cons ("finitize", "\"smart\" or \"false\"") - |> not codatatypes_ok - ? cons ("bisim_depth", "a nonnegative value") - val ss = - map (fn (name, value) => quote name ^ " set to " ^ value) - options - in - print ("Try again with " ^ - space_implode " " (serial_commas "and" ss) ^ - " to confirm that the " ^ das_wort_model ^ - " is genuine.") - end - else - print ("Nitpick is unable to guarantee the authenticity of \ - \the " ^ das_wort_model ^ " in the presence of \ - \polymorphic axioms.") - else - (); - NONE) - else - if not genuine then - (Unsynchronized.inc met_potential; - if check_potential then - let - val status = prove_hol_model scope tac_timeout free_names - sel_names rel_table bounds assms_t - in - (case status of - SOME true => print ("Confirmation by \"auto\": The above " ^ - das_wort_model ^ " is genuine.") - | SOME false => print ("Refutation by \"auto\": The above " ^ - das_wort_model ^ " is spurious.") - | NONE => print "No confirmation by \"auto\"."); - status - end - else - NONE) - else - NONE + NONE) + |> pair genuine_means_genuine end - (* int -> int -> int -> bool -> rich_problem list -> int * int * int *) - fun solve_any_problem max_potential max_genuine donno first_time problems = + (* bool * int * int * int -> bool -> rich_problem list + -> bool * int * int * int *) + fun solve_any_problem (found_really_genuine, max_potential, max_genuine, + donno) first_time problems = let val max_potential = Int.max (0, max_potential) val max_genuine = Int.max (0, max_genuine) - (* bool -> int * KK.raw_bound list -> bool option *) + (* bool -> int * KK.raw_bound list -> bool * bool option *) fun print_and_check genuine (j, bounds) = print_and_check_model genuine bounds (snd (nth problems j)) val max_solutions = max_potential + max_genuine |> not need_incremental ? curry Int.min 1 in if max_solutions <= 0 then - (0, 0, donno) + (found_really_genuine, 0, 0, donno) else case KK.solve_any_problem overlord deadline max_threads max_solutions (map fst problems) of KK.NotInstalled => (print_m install_kodkodi_message; - (max_potential, max_genuine, donno + 1)) + (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.Normal ([], unsat_js, s) => (update_checked_problems problems unsat_js; show_kodkod_warning s; - (max_potential, max_genuine, donno)) + (found_really_genuine, max_potential, max_genuine, donno)) | KK.Normal (sat_ps, unsat_js, s) => let val (lib_ps, con_ps) = @@ -736,16 +741,19 @@ show_kodkod_warning s; if null con_ps then let - val num_genuine = take max_potential lib_ps - |> map (print_and_check false) - |> filter (curry (op =) (SOME true)) - |> length + val genuine_codes = + lib_ps |> take max_potential + |> map (print_and_check false) + |> filter (curry (op =) (SOME true) o snd) + val found_really_genuine = + found_really_genuine orelse exists fst genuine_codes + val num_genuine = length genuine_codes val max_genuine = max_genuine - num_genuine val max_potential = max_potential - (length lib_ps - num_genuine) in if max_genuine <= 0 then - (0, 0, donno) + (found_really_genuine, 0, 0, donno) else let (* "co_js" is the list of sound problems whose unsound @@ -765,18 +773,21 @@ |> max_potential <= 0 ? filter_out (#unsound o snd) in - solve_any_problem max_potential max_genuine donno false - problems + solve_any_problem (found_really_genuine, max_potential, + max_genuine, donno) false problems end end else let - val _ = take max_genuine con_ps - |> List.app (ignore o print_and_check true) - val max_genuine = max_genuine - length con_ps + val genuine_codes = + con_ps |> take max_genuine + |> map (print_and_check true) + val max_genuine = max_genuine - length genuine_codes + val found_really_genuine = + found_really_genuine orelse exists fst genuine_codes in if max_genuine <= 0 orelse not first_time then - (0, max_genuine, donno) + (found_really_genuine, 0, max_genuine, donno) else let val bye_js = sort_distinct int_ord @@ -784,7 +795,10 @@ val problems = problems |> filter_out_indices bye_js |> filter_out (#unsound o snd) - in solve_any_problem 0 max_genuine donno false problems end + in + solve_any_problem (found_really_genuine, 0, max_genuine, + donno) false problems + end end end | KK.TimedOut unsat_js => @@ -795,11 +809,13 @@ | KK.Error (s, unsat_js) => (update_checked_problems problems unsat_js; print_v (K ("Kodkod error: " ^ s ^ ".")); - (max_potential, max_genuine, donno + 1)) + (found_really_genuine, max_potential, max_genuine, donno + 1)) end - (* int -> int -> scope list -> int * int * int -> int * int * int *) - fun run_batch j n scopes (max_potential, max_genuine, donno) = + (* int -> int -> scope list -> bool * int * int * int + -> bool * int * int * int *) + fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine, + donno) = let val _ = if null scopes then @@ -869,7 +885,8 @@ else () in - solve_any_problem max_potential max_genuine donno true (rev problems) + solve_any_problem (found_really_genuine, max_potential, max_genuine, + donno) true (rev problems) end (* rich_problem list -> scope -> int *) @@ -901,8 +918,9 @@ "") ^ "." end - (* int -> int -> scope list -> int * int * int -> KK.outcome *) - fun run_batches _ _ [] (max_potential, max_genuine, donno) = + (* int -> int -> scope list -> bool * int * int * int -> KK.outcome *) + fun run_batches _ _ [] + (found_really_genuine, max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then (print_m (fn () => excipit "ran out of some resource"); "unknown") else if max_genuine = original_max_genuine then @@ -919,10 +937,12 @@ "Nitpick could not find a" ^ (if max_genuine = 1 then " better " ^ das_wort_model ^ "." else "ny better " ^ das_wort_model ^ "s.")); "potential") + else if found_really_genuine then + "genuine" else - if genuine_means_genuine then "genuine" else "likely_genuine" + "quasi_genuine" | run_batches j n (batch :: batches) z = - let val (z as (_, max_genuine, _)) = run_batch j n batch z in + let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in run_batches (j + 1) n (if max_genuine > 0 then batches else []) z end @@ -942,7 +962,8 @@ val batches = batch_list batch_size (!scopes) val outcome_code = - (run_batches 0 (length batches) batches (max_potential, max_genuine, 0) + (run_batches 0 (length batches) batches + (false, max_potential, max_genuine, 0) handle Exn.Interrupt => do_interrupted ()) handle TimeLimit.TimeOut => (print_m (fn () => excipit "ran out of time"); diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 20:23:19 2010 +0100 @@ -361,7 +361,8 @@ (@{const_name finite}, 1), (@{const_name unknown}, 0), (@{const_name is_unknown}, 1), - (@{const_name Tha}, 1), + (@{const_name safe_The}, 1), + (@{const_name safe_Eps}, 1), (@{const_name Frac}, 0), (@{const_name norm_frac}, 0)] val built_in_nat_consts = @@ -1821,7 +1822,7 @@ val bisim_max = @{const bisim_iterator_max} val n_var = Var (("n", 0), iter_T) val n_var_minus_1 = - Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T) + Const (@{const_name safe_The}, (iter_T --> bool_T) --> iter_T) $ Abs ("m", iter_T, HOLogic.eq_const iter_T $ (suc_const iter_T $ Bound 0) $ n_var) val x_var = Var (("x", 0), T) diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 20:23:19 2010 +0100 @@ -1388,7 +1388,7 @@ (Func (R1, Formula Neut)) r)) (to_opt R1 u1) | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u])) - | Op1 (Tha, _, R, u1) => + | Op1 (SafeThe, _, R, u1) => if is_opt_rep R then kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom else diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 20:23:19 2010 +0100 @@ -264,20 +264,22 @@ $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3))) | fin_fun_body _ _ _ = NONE -(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *) -fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 = +(* mdata -> bool -> typ -> typ -> mtyp * sign_atom * mtyp *) +fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus + T1 T2 = let - val M1 = fresh_mtype_for_type mdata T1 - val M2 = fresh_mtype_for_type mdata T2 - val a = if is_fin_fun_supported_type (body_type T2) andalso - exists_alpha_sub_mtype_fresh M1 then + val M1 = fresh_mtype_for_type mdata all_minus T1 + val M2 = fresh_mtype_for_type mdata all_minus T2 + val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso + is_fin_fun_supported_type (body_type T2) then V (Unsynchronized.inc max_fresh) else S Minus in (M1, a, M2) end -(* mdata -> typ -> mtyp *) +(* mdata -> bool -> typ -> mtyp *) and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, - datatype_mcache, constr_mcache, ...}) = + datatype_mcache, constr_mcache, ...}) + all_minus = let (* typ -> mtyp *) fun do_type T = @@ -285,7 +287,7 @@ MAlpha else case T of Type (@{type_name fun}, [T1, T2]) => - MFun (fresh_mfun_for_fun_type mdata T1 T2) + MFun (fresh_mfun_for_fun_type mdata false T1 T2) | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2)) | Type (z as (s, _)) => if could_exist_alpha_sub_mtype thy alpha_T T then @@ -347,14 +349,14 @@ case AList.lookup (op =) (!constr_mcache) x of SOME M => M | NONE => if T = alpha_T then - let val M = fresh_mtype_for_type mdata T in + let val M = fresh_mtype_for_type mdata false T in (Unsynchronized.change constr_mcache (cons (x, M)); M) end else - (fresh_mtype_for_type mdata (body_type T); + (fresh_mtype_for_type mdata false (body_type T); AList.lookup (op =) (!constr_mcache) x |> the) else - fresh_mtype_for_type mdata T + fresh_mtype_for_type mdata false T fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s @@ -629,7 +631,7 @@ alpha_T, max_fresh, ...}) = let (* typ -> mtyp *) - val mtype_for = fresh_mtype_for_type mdata + val mtype_for = fresh_mtype_for_type mdata false (* mtyp -> mtyp *) fun plus_set_mtype_for_dom M = MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M) @@ -765,15 +767,6 @@ val ba_set_M = range_type T |> mtype_for_set in (MFun (ab_set_M, S Minus, ba_set_M), accum) end | @{const_name trancl} => do_fragile_set_operation T accum - | @{const_name rtrancl} => - (print_g "*** rtrancl"; mtype_unsolvable) - | @{const_name finite} => - if is_finite_type hol_ctxt T then - let val M1 = mtype_for (domain_type (domain_type T)) in - (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum) - end - else - (print_g "*** finite"; mtype_unsolvable) | @{const_name rel_comp} => let val x = Unsynchronized.inc max_fresh @@ -796,6 +789,10 @@ MFun (plus_set_mtype_for_dom a_M, S Minus, plus_set_mtype_for_dom b_M)), accum) end + | @{const_name finite} => + let val M1 = mtype_for (domain_type (domain_type T)) in + (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum) + end | @{const_name Sigma} => let val x = Unsynchronized.inc max_fresh @@ -813,14 +810,15 @@ (MFun (a_set_M, S Minus, MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) end - | @{const_name Tha} => - let - val a_M = mtype_for (domain_type (domain_type T)) - val a_set_M = plus_set_mtype_for_dom a_M - in (MFun (a_set_M, S Minus, a_M), accum) end | _ => - if s = @{const_name minus_class.minus} andalso - is_set_type (domain_type T) then + if s = @{const_name safe_The} orelse + s = @{const_name safe_Eps} then + let + val a_set_M = mtype_for (domain_type T) + val a_M = dest_MFun a_set_M |> #1 + in (MFun (a_set_M, S Minus, a_M), accum) end + else if s = @{const_name minus_class.minus} andalso + is_set_type (domain_type T) then let val set_T = domain_type T val left_set_M = mtype_for set_T @@ -842,13 +840,8 @@ (mtype_for_sel mdata x, accum) else if is_constr thy stds x then (mtype_for_constr mdata x, accum) - else if is_built_in_const thy stds fast_descrs x andalso - s <> @{const_name is_unknown} andalso - s <> @{const_name unknown} then - (* the "unknown" part is a hack *) - case def_of_const thy def_table x of - SOME t' => do_term t' accum |>> mtype_of_mterm - | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable) + else if is_built_in_const thy stds fast_descrs x then + (fresh_mtype_for_type mdata true T, accum) else let val M = mtype_for T in (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, @@ -936,7 +929,7 @@ val M1 = mtype_of_mterm m1 val M2 = mtype_of_mterm m2 val accum = accum ||> add_mtypes_equal M1 M2 - val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T) + val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T) val m = MApp (MApp (MRaw (Const x, MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2) in @@ -952,7 +945,7 @@ fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) = let (* typ -> mtyp *) - val mtype_for = fresh_mtype_for_type mdata + val mtype_for = fresh_mtype_for_type mdata false (* term -> accumulator -> mterm * accumulator *) val do_term = consider_term mdata (* sign -> term -> accumulator -> mterm * accumulator *) @@ -1059,7 +1052,7 @@ else let (* typ -> mtyp *) - val mtype_for = fresh_mtype_for_type mdata + val mtype_for = fresh_mtype_for_type mdata false (* term -> accumulator -> mterm * accumulator *) val do_term = consider_term mdata (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *) @@ -1205,8 +1198,26 @@ val T' = type_from_mtype T M in case t of - Const (x as (s, T)) => - if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then + Const (x as (s, _)) => + if s = @{const_name insert} then + case nth_range_type 2 T' of + set_T' as Type (@{type_name fin_fun}, [elem_T', _]) => + Abs (Name.uu, elem_T', Abs (Name.uu, set_T', + Const (@{const_name If}, + bool_T --> set_T' --> set_T' --> set_T') + $ (Const (@{const_name is_unknown}, elem_T' --> bool_T) + $ Bound 1) + $ (Const (@{const_name unknown}, set_T')) + $ (coerce_term hol_ctxt Ts T' T (Const x) + $ Bound 1 $ Bound 0))) + | _ => Const (s, T') + else if s = @{const_name finite} then + case domain_type T' of + set_T' as Type (@{type_name fin_fun}, _) => + Abs (Name.uu, set_T', @{const True}) + | _ => Const (s, T') + else if s = @{const_name "=="} orelse + s = @{const_name "op ="} then Const (s, T') else if is_built_in_const thy stds fast_descrs x then coerce_term hol_ctxt Ts T' T t @@ -1228,16 +1239,6 @@ | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm", [m]) end - | MAbs (s, T, M, a, m') => - let - val T = type_from_mtype T M - val t' = term_from_mterm (T :: Ts) m' - val T' = fastype_of1 (T :: Ts, t') - in - Abs (s, T, t') - |> should_finitize (T --> T') a - ? construct_value thy stds (fin_fun_constr T T') o single - end | MApp (m1, m2) => let val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2) @@ -1253,6 +1254,16 @@ | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", [T1], []) in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end + | MAbs (s, T, M, a, m') => + let + val T = type_from_mtype T M + val t' = term_from_mterm (T :: Ts) m' + val T' = fastype_of1 (T :: Ts, t') + in + Abs (s, T, t') + |> should_finitize (T --> T') a + ? construct_value thy stds (fin_fun_constr T T') o single + end in Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); pairself (map (term_from_mterm [])) msp diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 20:23:19 2010 +0100 @@ -39,7 +39,7 @@ Closure | SingletonSet | IsUnknown | - Tha | + SafeThe | First | Second | Cast @@ -158,7 +158,7 @@ Closure | SingletonSet | IsUnknown | - Tha | + SafeThe | First | Second | Cast @@ -232,7 +232,7 @@ | string_for_op1 Closure = "Closure" | string_for_op1 SingletonSet = "SingletonSet" | string_for_op1 IsUnknown = "IsUnknown" - | string_for_op1 Tha = "Tha" + | string_for_op1 SafeThe = "SafeThe" | string_for_op1 First = "First" | string_for_op1 Second = "Second" | string_for_op1 Cast = "Cast" @@ -516,8 +516,15 @@ val t1 = list_comb (t0, ts') val T1 = fastype_of1 (Ts, t1) in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end - (* styp -> term list -> term *) - fun construct (x as (_, T)) ts = + (* op2 -> string -> styp -> term -> nut *) + fun do_description_operator oper undef_s (x as (_, T)) t1 = + if fast_descrs then + Op2 (oper, range_type T, Any, sub t1, + sub (Const (undef_s, range_type T))) + else + do_apply (Const x) [t1] + (* styp -> term list -> nut *) + fun do_construct (x as (_, T)) ts = case num_binder_types T - length ts of 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any)) o nth_sel_for_constr x) @@ -552,18 +559,10 @@ do_quantifier Exist s T t1 | (t0 as Const (@{const_name Ex}, _), [t1]) => sub' (t0 $ eta_expand Ts t1 1) - | (t0 as Const (@{const_name The}, T), [t1]) => - if fast_descrs then - Op2 (The, range_type T, Any, sub t1, - sub (Const (@{const_name undefined_fast_The}, range_type T))) - else - do_apply t0 [t1] - | (t0 as Const (@{const_name Eps}, T), [t1]) => - if fast_descrs then - Op2 (Eps, range_type T, Any, sub t1, - sub (Const (@{const_name undefined_fast_Eps}, range_type T))) - else - do_apply t0 [t1] + | (Const (x as (@{const_name The}, _)), [t1]) => + do_description_operator The @{const_name undefined_fast_The} x t1 + | (Const (x as (@{const_name Eps}, _)), [t1]) => + do_description_operator Eps @{const_name undefined_fast_Eps} x t1 | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2 | (Const (@{const_name "op &"}, _), [t1, t2]) => Op2 (And, bool_T, Any, sub' t1, sub' t2) @@ -605,7 +604,7 @@ Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (x as (s as @{const_name Suc}, T)), []) => if is_built_in_const thy stds false x then Cst (Suc, T, Any) - else if is_constr thy stds x then construct x [] + else if is_constr thy stds x then do_construct x [] else ConstName (s, T, Any) | (Const (@{const_name finite}, T), [t1]) => (if is_finite_type hol_ctxt (domain_type T) then @@ -616,7 +615,7 @@ | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any) | (Const (x as (s as @{const_name zero_class.zero}, T)), []) => if is_built_in_const thy stds false x then Cst (Num 0, T, Any) - else if is_constr thy stds x then construct x [] + else if is_constr thy stds x then do_construct x [] else ConstName (s, T, Any) | (Const (x as (s as @{const_name one_class.one}, T)), []) => if is_built_in_const thy stds false x then Cst (Num 1, T, Any) @@ -670,8 +669,11 @@ | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any) | (Const (@{const_name is_unknown}, _), [t1]) => Op1 (IsUnknown, bool_T, Any, sub t1) - | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) => - Op1 (Tha, T2, Any, sub t1) + | (Const (@{const_name safe_The}, + Type (@{type_name fun}, [_, T2])), [t1]) => + Op1 (SafeThe, T2, Any, sub t1) + | (Const (x as (@{const_name safe_Eps}, _)), [t1]) => + do_description_operator Eps @{const_name undefined_fast_Eps} x t1 | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => @@ -691,7 +693,7 @@ Op2 (Union, T1, Any, sub t1, sub t2) | (t0 as Const (x as (s, T)), ts) => if is_constr thy stds x then - construct x ts + do_construct x ts else if String.isPrefix numeral_prefix s then Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any) else diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 20:23:19 2010 +0100 @@ -221,7 +221,8 @@ $ do_term new_Ts old_Ts polar t2 | Const (s as @{const_name The}, T) => do_description_operator s T | Const (s as @{const_name Eps}, T) => do_description_operator s T - | Const (s as @{const_name Tha}, T) => do_description_operator s T + | Const (s as @{const_name safe_The}, T) => do_description_operator s T + | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T | Const (x as (s, T)) => Const (s, if s = @{const_name converse} orelse s = @{const_name trancl} then @@ -1341,6 +1342,8 @@ let val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) |> filter_out (fn Type (@{type_name fun_box}, _) => true + | @{typ signed_bit} => true + | @{typ unsigned_bit} => true | T => is_small_finite_type hol_ctxt T orelse triple_lookup (type_match thy) monos T = SOME (SOME false)) diff -r 3007b46c1660 -r 86e48f81492b src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Tue Mar 09 14:36:41 2010 +0100 +++ b/src/HOL/Tools/transfer.ML Tue Mar 09 20:23:19 2010 +0100 @@ -8,10 +8,11 @@ signature TRANSFER = sig datatype selection = Direction of term * term | Hints of string list | Prop - val transfer: Context.generic -> selection -> string list -> thm -> thm + val transfer: Context.generic -> selection -> string list -> thm -> thm list type entry - val add: entry * entry -> thm -> Context.generic -> Context.generic - val del: thm -> Context.generic -> Context.generic + val add: thm -> bool -> entry -> Context.generic -> Context.generic + val del: thm -> entry -> Context.generic -> Context.generic + val drop: thm -> Context.generic -> Context.generic val setup: theory -> theory end; @@ -29,14 +30,15 @@ ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI})); in direction_of key end; -type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list, - guess : bool, hints : string list }; +type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list, + hints : string list }; -fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry, - { inj = inj2, emb = emb2, ret = ret2, cong = cong2, guess = guess2, hints = hints2 } : entry) = - { inj = merge Thm.eq_thm (inj1, inj2), emb = merge Thm.eq_thm (emb1, emb2), - ret = merge Thm.eq_thm (ret1, ret2), cong = merge Thm.eq_thm (cong1, cong2), - guess = guess1 andalso guess2, hints = merge (op =) (hints1, hints2) }; +val empty_entry = { inj = [], embed = [], return = [], cong = [], hints = [] }; +fun merge_entry ({ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } : entry, + { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } : entry) = + { inj = merge Thm.eq_thm (inj1, inj2), embed = merge Thm.eq_thm (embed1, embed2), + return = merge Thm.eq_thm (return1, return2), cong = merge Thm.eq_thm (cong1, cong2), + hints = merge (op =) (hints1, hints2) }; structure Data = Generic_Data ( @@ -49,6 +51,9 @@ (* data lookup *) +fun transfer_rules_of { inj, embed, return, cong, ... } = + (inj, embed, return, cong); + fun get_by_direction context (a, D) = let val ctxt = Context.proof_of context; @@ -58,9 +63,9 @@ fun eq_direction ((a, D), thm') = let val (a', D') = direction_of thm'; - in a0 aconvc a' andalso D0 aconvc D' end; - in case AList.lookup eq_direction (Data.get context) (a, D) of - SOME e => ((a0, D0), e) + in a aconvc a' andalso D aconvc D' end; + in case AList.lookup eq_direction (Data.get context) (a0, D0) of + SOME e => ((a0, D0), transfer_rules_of e) | NONE => error ("Transfer: no such instance: (" ^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")") end; @@ -68,7 +73,7 @@ fun get_by_hints context hints = let val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints - then SOME (direction_of k, e) else NONE) (Data.get context); + then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context); val _ = if null insts then error ("Transfer: no such labels: " ^ commas (map quote hints)) else (); in insts end; @@ -84,9 +89,9 @@ val _ = if null tys then error "Transfer: unable to guess instance" else (); val tyss = splits (curry Type.could_unify) tys; val get_ty = typ_of o ctyp_of_term o fst o direction_of; - val insts = map_filter (fn tys => get_first (fn (k, ss) => + val insts = map_filter (fn tys => get_first (fn (k, e) => if Type.could_unify (hd tys, range_type (get_ty k)) - then SOME (direction_of k, ss) + then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context)) tyss; val _ = if null insts then error "Transfer: no instances, provide direction or hints explicitly" else (); @@ -95,8 +100,7 @@ (* applying transfer data *) -fun transfer_thm inj_only a0 D0 {inj = inj, emb = emb, ret = ret, cong = cg, guess = _, hints = _} - leave ctxt0 th = +fun transfer_thm inj_only ((a0, D0), (inj, embed, return, cong)) leave ctxt0 th = let val ([a, D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0); @@ -116,15 +120,14 @@ Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''; val th1 = Drule.cterm_instantiate (cns ~~ cis) th; val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1); - val simpset = (Simplifier.context ctxt''' HOL_ss) - addsimps inj addsimps (if inj_only then [] else emb @ ret) addcongs cg; + val simpset = Simplifier.context ctxt''' HOL_ss + addsimps inj addsimps (if inj_only then [] else embed @ return) addcongs cong; val th3 = Simplifier.asm_full_simplify simpset (fold_rev implies_intr (map cprop_of hs) th2); in hd (Variable.export ctxt''' ctxt0 [th3]) end; fun transfer_thm_multiple inj_only insts leave ctxt thm = - Conjunction.intr_balanced (map - (fn ((a, D), e) => transfer_thm false a D e leave ctxt thm) insts); + map (fn inst => transfer_thm false inst leave ctxt thm) insts; datatype selection = Direction of term * term | Hints of string list | Prop; @@ -138,44 +141,41 @@ (* maintaining transfer data *) -fun merge_update eq m (k, v) [] = [(k, v)] - | merge_update eq m (k, v) ((k', v') :: al) = - if eq (k, k') then (k', m (v, v')) :: al else (k', v') :: merge_update eq m (k, v) al; - -(*? fun merge_update eq m (k, v) = AList.map_entry eq k (fn v' => m (v, v'));*) - -fun merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0} - ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, - {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2} : entry) = +fun extend_entry ctxt (a, D) guess + { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } + { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = let - fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs, ys)) + fun add_del eq del add = union eq add #> subtract eq del; + val guessed = if guess + then map (fn thm => transfer_thm true + ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1 + else []; in - {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, - ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2, - hints = subtract (op =) hints0 (union (op =) hints1 hints2) } + { inj = union Thm.eq_thm inj1 inj2, embed = union Thm.eq_thm embed1 embed2, + return = union Thm.eq_thm guessed (union Thm.eq_thm return1 return2), + cong = union Thm.eq_thm cong1 cong2, hints = union (op =) hints1 hints2 } end; -fun add (e0 as {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}, - ed as {inj = injd, emb = embd, ret = retd, cong = cgd, guess = _, hints = hintsd}) key context = - context - |> Data.map (fn al => - let - val ctxt = Context.proof_of context; - val (a0, D0) = check_morphism_key ctxt key; - val entry = if g then - let - val inj' = if null inja then #inj - (case AList.lookup Thm.eq_thm al key of SOME e => e - | NONE => error "Transfer: cannot generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") - else inja - val ret' = merge Thm.eq_thm (reta, map - (fn th => transfer_thm true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, - hints = hintsa} [] ctxt th RS sym) emba); - in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end - else e0; - in merge_update Thm.eq_thm (merge_entries ed) (key, entry) al end); +fun diminish_entry + { inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 } + { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = + { inj = subtract Thm.eq_thm inj0 inj2, embed = subtract Thm.eq_thm embed0 embed2, + return = subtract Thm.eq_thm return0 return2, cong = subtract Thm.eq_thm cong0 cong2, + hints = subtract (op =) hints0 hints2 }; -fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, [])); +fun add key guess entry context = + let + val ctxt = Context.proof_of context; + val a_D = check_morphism_key ctxt key; + in + context + |> Data.map (AList.map_default Thm.eq_thm + (key, empty_entry) (extend_entry ctxt a_D guess entry)) + end; + +fun del key entry = Data.map (AList.map_entry Thm.eq_thm key (diminish_entry entry)); + +fun drop key = Data.map (AList.delete Thm.eq_thm key); (* syntax *) @@ -188,22 +188,24 @@ fun keyword k = Scan.lift (Args.$$$ k) >> K (); fun keyword_colon k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -val congN = "cong"; -val injN = "inj"; -val embedN = "embed"; -val returnN = "return"; val addN = "add"; val delN = "del"; val modeN = "mode"; val automaticN = "automatic"; val manualN = "manual"; -val directionN = "direction"; +val injN = "inj"; +val embedN = "embed"; +val returnN = "return"; +val congN = "cong"; val labelsN = "labels"; -val leavingN = "leaving"; -val any_keyword = keyword_colon congN || keyword_colon injN || keyword_colon embedN - || keyword_colon returnN || keyword_colon directionN || keyword_colon modeN - || keyword_colon delN || keyword_colon labelsN || keyword_colon leavingN; +val leavingN = "leaving"; +val directionN = "direction"; + +val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon modeN + || keyword_colon injN || keyword_colon embedN || keyword_colon returnN + || keyword_colon congN || keyword_colon labelsN + || keyword_colon leavingN || keyword_colon directionN; val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name)) @@ -216,23 +218,26 @@ val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms); val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names); -val entry_pair = Scan.optional mode true -- these_pair inj -- these_pair embed +val entry_pair = these_pair inj -- these_pair embed -- these_pair return -- these_pair cong -- these_pair labels - >> (fn (((((g, (inja, injd)), (emba, embd)), (reta, retd)), (cga, cgd)), (hintsa, hintsd)) => - ({inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}, - {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd})); + >> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)), + (hintsa, hintsd)) => + ({inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa}, + {inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd})); val selection = (keyword_colon directionN |-- (Args.term -- Args.term) >> Direction) || these names >> (fn hints => if null hints then Prop else Hints hints); in -val transfer_attribute = Scan.lift (Args.$$$ delN >> K (Thm.declaration_attribute del)) - || Scan.unless any_keyword (keyword addN) |-- entry_pair - >> (fn entry_pair => Thm.declaration_attribute (add entry_pair)) +val transfer_attribute = Scan.lift (Args.$$$ delN >> K (Thm.declaration_attribute drop)) + || Scan.unless any_keyword (keyword addN) |-- Scan.optional mode true -- entry_pair + >> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute + (fn thm => add thm guess entry_add #> del thm entry_del)); val transferred_attribute = selection -- these (keyword_colon leavingN |-- names) - >> (fn (selection, leave) => Thm.rule_attribute (fn context => transfer context selection leave)); + >> (fn (selection, leave) => Thm.rule_attribute (fn context => + Conjunction.intr_balanced o transfer context selection leave)); end;