# HG changeset patch # User huffman # Date 1244470955 25200 # Node ID bd96f81f657214c93fbe7b920ed1030cdec727d3 # Parent ff0ab207849a367a22c61bdda833d806695b7ee2# Parent 6f589131ba94f8f86a3f9716ecf09f88c2d77d60 merged diff -r ff0ab207849a -r bd96f81f6572 NEWS --- a/NEWS Sun Jun 07 20:57:52 2009 -0700 +++ b/NEWS Mon Jun 08 07:22:35 2009 -0700 @@ -25,6 +25,8 @@ * ML antiquotation @{code_datatype} inserts definition of a datatype generated by the code generator; see Predicate.thy for an example. +* New method "linarith" invokes existing linear arithmetic decision procedure only. + *** ML *** diff -r ff0ab207849a -r bd96f81f6572 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/Library/Enum.thy Mon Jun 08 07:22:35 2009 -0700 @@ -1,5 +1,4 @@ -(* Title: HOL/Library/Enum.thy - Author: Florian Haftmann, TU Muenchen +(* Author: Florian Haftmann, TU Muenchen *) header {* Finite types as explicit enumerations *} @@ -286,76 +285,9 @@ definition [code del]: "enum = map (split Char) (product enum enum)" -lemma enum_char [code]: - "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, - Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, - Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8, - Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB, - Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE, - Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1, - Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4, - Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7, - Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA, - Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD, - Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'', - Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'', - Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','', - CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', - CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'', - CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'', - CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'', - CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'', - CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'', - CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC, - CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'', - CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'', - CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'', - CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'', - CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'', - Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1, - Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4, - Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7, - Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA, - Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD, - Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0, - Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3, - Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6, - Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9, - Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC, - Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF, - Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2, - Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5, - Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8, - Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB, - Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE, - Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1, - Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4, - Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7, - Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA, - Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD, - Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0, - Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3, - Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6, - Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9, - Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC, - Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF, - Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2, - Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5, - Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8, - Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB, - Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE, - Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1, - Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4, - Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7, - Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA, - Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD, - Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0, - Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3, - Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6, - Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9, - Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC, - Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]" - unfolding enum_char_def enum_nibble_def by simp +lemma enum_chars [code]: + "enum = chars" + unfolding enum_char_def chars_def enum_nibble_def by simp instance proof qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric] diff -r ff0ab207849a -r bd96f81f6572 src/HOL/Library/Fin_Fun.thy --- a/src/HOL/Library/Fin_Fun.thy Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/Library/Fin_Fun.thy Mon Jun 08 07:22:35 2009 -0700 @@ -1186,10 +1186,10 @@ proof - from enum_distinct have "card (set (enum :: char list)) = length (enum :: char list)" - by -(rule distinct_card) + by - (rule distinct_card) also have "set enum = (UNIV :: char set)" by auto - also note enum_char - finally show ?thesis by simp + also note enum_chars + finally show ?thesis by (simp add: chars_def) qed instantiation char :: card_UNIV begin diff -r ff0ab207849a -r bd96f81f6572 src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/Quickcheck.thy Mon Jun 08 07:22:35 2009 -0700 @@ -40,6 +40,26 @@ end +instantiation char :: random +begin + +definition + "random _ = Random.select chars o\ (\c. Pair (c, \u. Code_Eval.term_of c))" + +instance .. + +end + +instantiation String.literal :: random +begin + +definition + "random _ = Pair (STR [], \u. Code_Eval.term_of (STR []))" + +instance .. + +end + instantiation nat :: random begin @@ -77,6 +97,13 @@ "beyond k 0 = 0" by (simp add: beyond_def) +lemma random_aux_rec: + fixes random_aux :: "code_numeral \ 'a" + assumes "random_aux 0 = rhs 0" + and "\k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)" + shows "random_aux k = rhs k" + using assms by (rule code_numeral.induct) + use "Tools/quickcheck_generators.ML" setup {* Quickcheck_Generators.setup *} diff -r ff0ab207849a -r bd96f81f6572 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/SetInterval.thy Mon Jun 08 07:22:35 2009 -0700 @@ -833,6 +833,13 @@ apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) done +lemma setsum_ub_add_nat: assumes "(m::nat) \ n + 1" + shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" +proof- + have "{m .. n+p} = {m..n} \ {n+1..n+p}" using `m \ n+1` by auto + thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint + atLeastSucAtMost_greaterThanAtMost) +qed lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ setsum f {m.. ('a::ab_group_add)" + shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} = + (if m <= n then f m - f(n + 1) else 0)" +by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) + subsection{* Shifting bounds *} diff -r ff0ab207849a -r bd96f81f6572 src/HOL/String.thy --- a/src/HOL/String.thy Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/String.thy Mon Jun 08 07:22:35 2009 -0700 @@ -46,8 +46,6 @@ primrec nibble_pair_of_char :: "char \ nibble \ nibble" where "nibble_pair_of_char (Char n m) = (n, m)" -declare nibble_pair_of_char.simps [code del] - setup {* let val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15); @@ -82,6 +80,76 @@ setup StringSyntax.setup +definition chars :: string where + "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, + Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, + Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8, + Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB, + Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE, + Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1, + Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4, + Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7, + Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA, + Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD, + Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'', + Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'', + Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','', + CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', + CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'', + CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'', + CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'', + CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'', + CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'', + CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC, + CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'', + CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'', + CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'', + CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'', + CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'', + Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1, + Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4, + Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7, + Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA, + Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD, + Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0, + Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3, + Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6, + Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9, + Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC, + Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF, + Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2, + Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5, + Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8, + Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB, + Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE, + Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1, + Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4, + Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7, + Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA, + Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD, + Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0, + Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3, + Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6, + Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9, + Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC, + Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF, + Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2, + Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5, + Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8, + Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB, + Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE, + Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1, + Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4, + Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7, + Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA, + Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD, + Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0, + Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3, + Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6, + Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9, + Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC, + Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]" + subsection {* Strings as dedicated datatype *} diff -r ff0ab207849a -r bd96f81f6572 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/Tools/quickcheck_generators.ML Mon Jun 08 07:22:35 2009 -0700 @@ -11,6 +11,7 @@ -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed val ensure_random_typecopy: string -> theory -> theory + val random_aux_specification: string -> term list -> local_theory -> local_theory val eval_ref: (unit -> int -> int * int -> term list option * (int * int)) option ref val setup: theory -> theory end; @@ -133,7 +134,109 @@ (** datatypes **) -(* still under construction *) +(* definitional scheme for random instances on datatypes *) + +(*FIXME avoid this low-level proving*) +val rct = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg + |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_fun; +fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k; +val aT = rct |> Thm.ctyp_of_term |> dest_ctyp_nth 1; + +fun random_aux_primrec eq lthy = + let + val thy = ProofContext.theory_of lthy; + val rews = map mk_meta_eq [@{thm code_numeral_zero_minus_one}, + @{thm Suc_code_numeral_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}]; + val (rt as Free (random_aux, T)) $ (vt as Free (v, _)) = + (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; + val Type (_, [_, iT]) = T; + val icT = Thm.ctyp_of thy iT; + fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t); + val eqs0 = [subst_v @{term "0::code_numeral"} eq, subst_v (@{term "Suc_code_numeral"} $ vt) eq]; + val eqs1 = map (Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) rews) []) eqs0 + val ((_, eqs2), lthy') = PrimrecPackage.add_primrec_simple + [((Binding.name random_aux, T), NoSyn)] eqs1 lthy; + val eq_tac = ALLGOALS Goal.conjunction_tac THEN ALLGOALS (simp_tac (HOL_ss addsimps rews)) + THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2))); + val eqs3 = Goal.prove_multi lthy' [v] [] eqs0 (K eq_tac); + val rct' = Thm.instantiate_cterm ([(aT, icT)], []) rct + val rule = @{thm random_aux_rec} + |> Drule.instantiate ([(aT, icT)], [(rct', Thm.cterm_of thy rt)]) + |> (fn thm => thm OF eqs3) + val tac = ALLGOALS (rtac rule); + val simp = Goal.prove lthy' [v] [] eq (K tac); + in (simp, lthy') end; + +fun random_aux_primrec_multi prefix [eq] lthy = + lthy + |> random_aux_primrec eq + |>> (fn simp => [simp]) + | random_aux_primrec_multi prefix (eqs as _ :: _ :: _) lthy = + let + val thy = ProofContext.theory_of lthy; + val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs; + val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss; + val Ts = map fastype_of lhss; + val tupleT = foldr1 HOLogic.mk_prodT Ts; + val aux_lhs = Free ("mutual_" ^ prefix, fastype_of arg --> tupleT) $ arg; + val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) + (aux_lhs, foldr1 HOLogic.mk_prod rhss); + fun mk_proj t [T] = [t] + | mk_proj t (Ts as T :: (Ts' as _ :: _)) = + Const (@{const_name fst}, foldr1 HOLogic.mk_prodT Ts --> T) $ t + :: mk_proj (Const (@{const_name snd}, + foldr1 HOLogic.mk_prodT Ts --> foldr1 HOLogic.mk_prodT Ts') $ t) Ts'; + val projs = mk_proj (aux_lhs) Ts; + val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs; + val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) => + ((Binding.name name, NoSyn), (Attrib.empty_binding, rhs))) vs proj_eqs; + val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq; + fun prove_eqs aux_simp proj_defs lthy = + let + val proj_simps = map (snd o snd) proj_defs; + fun tac { context = ctxt, ... } = ALLGOALS Goal.conjunction_tac + THEN ALLGOALS (simp_tac (HOL_ss addsimps proj_simps)) + THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp]) + THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv])); + in (Goal.prove_multi lthy [v] [] eqs tac, lthy) end; + in + lthy + |> random_aux_primrec aux_eq' + ||>> fold_map (LocalTheory.define Thm.definitionK) proj_defs + |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs) + end; + +fun random_aux_specification prefix eqs lthy = + let + val _ $ Free (v, _) $ Free (w, _) = + (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o hd) eqs; + fun mk_proto_eq eq = + let + val (head $ arg, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; + in ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (head, lambda arg rhs)) end; + val proto_eqs = map mk_proto_eq eqs; + fun prove_simps proto_simps lthy = + let + val ext_simps = map (fn thm => fun_cong OF [thm]) proto_simps; + val tac = ALLGOALS Goal.conjunction_tac + THEN ALLGOALS (ProofContext.fact_tac ext_simps); + in (Goal.prove_multi lthy [v, w] [] eqs (K tac), lthy) end; + val b = Binding.qualify true prefix (Binding.name "simps"); + in + lthy + |> random_aux_primrec_multi prefix proto_eqs + |-> (fn proto_simps => prove_simps proto_simps) + |-> (fn simps => LocalTheory.note Thm.generatedK ((b, + Code.add_default_eqn_attrib :: map (Attrib.internal o K) + [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]), + simps)) + |> snd + end + + +(* constructing random instances on datatypes *) + +(*still under construction*) (** setup **) diff -r ff0ab207849a -r bd96f81f6572 src/HOL/ex/Quickcheck_Generators.thy --- a/src/HOL/ex/Quickcheck_Generators.thy Sun Jun 07 20:57:52 2009 -0700 +++ b/src/HOL/ex/Quickcheck_Generators.thy Mon Jun 08 07:22:35 2009 -0700 @@ -136,6 +136,8 @@ ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); fun add_random_inst [@{type_name bool}] thy = thy | add_random_inst [@{type_name nat}] thy = thy + | add_random_inst [@{type_name char}] thy = thy + | add_random_inst [@{type_name String.literal}] thy = thy | add_random_inst tycos thy = random_inst tycos thy handle REC msg => (warning msg; thy) | TYP msg => (warning msg; thy) diff -r ff0ab207849a -r bd96f81f6572 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Sun Jun 07 20:57:52 2009 -0700 +++ b/src/Tools/code/code_ml.ML Mon Jun 08 07:22:35 2009 -0700 @@ -47,9 +47,6 @@ fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = let - val pr_label_classrel = translate_string (fn "." => "__" | c => c) - o Long_Name.qualifier; - val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier; fun pr_dicts fxy ds = let fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_" @@ -272,11 +269,11 @@ val w = Code_Printer.first_upper v ^ "_"; fun pr_superclass_field (class, classrel) = (concat o map str) [ - pr_label_classrel classrel, ":", "'" ^ v, deresolve class + deresolve classrel, ":", "'" ^ v, deresolve class ]; fun pr_classparam_field (classparam, ty) = concat [ - (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty + (str o deresolve) classparam, str ":", pr_typ NOBR ty ]; fun pr_classparam_proj (classparam, _) = semicolon [ @@ -284,7 +281,7 @@ (str o deresolve) classparam, Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)], str "=", - str ("#" ^ pr_label_classparam classparam), + str ("#" ^ deresolve classparam), str w ]; fun pr_superclass_proj (_, classrel) = @@ -293,7 +290,7 @@ (str o deresolve) classrel, Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)], str "=", - str ("#" ^ pr_label_classrel classrel), + str ("#" ^ deresolve classrel), str w ]; in @@ -314,13 +311,13 @@ let fun pr_superclass (_, (classrel, dss)) = concat [ - (str o pr_label_classrel) classrel, + (str o deresolve) classrel, str "=", pr_dicts NOBR [DictConst dss] ]; fun pr_classparam ((classparam, c_inst), (thm, _)) = concat [ - (str o pr_label_classparam) classparam, + (str o deresolve) classparam, str "=", pr_app (K false) thm reserved_names NOBR (c_inst, []) ];