--- 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 ***
--- 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]
--- 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
--- 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\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))"
+
+instance ..
+
+end
+
+instantiation String.literal :: random
+begin
+
+definition
+ "random _ = Pair (STR [], \<lambda>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 \<Rightarrow> 'a"
+ assumes "random_aux 0 = rhs 0"
+ and "\<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 *}
--- 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) \<le> 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} \<union> {n+1..n+p}" using `m \<le> n+1` by auto
+ thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint
+ atLeastSucAtMost_greaterThanAtMost)
+qed
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
@@ -846,6 +853,12 @@
apply (simp add: add_ac)
done
+lemma setsum_natinterval_difff:
+ fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
+ shows "setsum (\<lambda>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 *}
--- 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 \<Rightarrow> nibble \<times> 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 *}
--- 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 **)
--- 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)
--- 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, [])
];