1.1 --- a/NEWS Sat Jun 28 15:30:46 2008 +0200
1.2 +++ b/NEWS Sat Jun 28 21:21:13 2008 +0200
1.3 @@ -19,6 +19,12 @@
1.4 interface instead.
1.5
1.6
1.7 +*** Document preparation ***
1.8 +
1.9 +* Antiquotation @{lemma} now imitates a regular terminal proof,
1.10 +demanding keyword 'by' and supporting the full method expressions.
1.11 +
1.12 +
1.13 *** HOL ***
1.14
1.15 * Methods "case_tac" and "induct_tac" now refer to the very same rules
2.1 --- a/src/HOL/List.thy Sat Jun 28 15:30:46 2008 +0200
2.2 +++ b/src/HOL/List.thy Sat Jun 28 21:21:13 2008 +0200
2.3 @@ -215,40 +215,40 @@
2.4 \begin{figure}[htbp]
2.5 \fbox{
2.6 \begin{tabular}{l}
2.7 -@{lemma "[a,b]@[c,d] = [a,b,c,d]" simp}\\
2.8 -@{lemma "length [a,b,c] = 3" simp}\\
2.9 -@{lemma "set [a,b,c] = {a,b,c}" simp}\\
2.10 -@{lemma "map f [a,b,c] = [f a, f b, f c]" simp}\\
2.11 -@{lemma "rev [a,b,c] = [c,b,a]" simp}\\
2.12 -@{lemma "hd [a,b,c,d] = a" simp}\\
2.13 -@{lemma "tl [a,b,c,d] = [b,c,d]" simp}\\
2.14 -@{lemma "last [a,b,c,d] = d" simp}\\
2.15 -@{lemma "butlast [a,b,c,d] = [a,b,c]" simp}\\
2.16 -@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" simp}\\
2.17 -@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" simp}\\
2.18 -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" simp}\\
2.19 -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" simp}\\
2.20 -@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" simp}\\
2.21 -@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" simp}\\
2.22 -@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" simp}\\
2.23 -@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" simp}\\
2.24 -@{lemma "take 2 [a,b,c,d] = [a,b]" simp}\\
2.25 -@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" simp}\\
2.26 -@{lemma "drop 2 [a,b,c,d] = [c,d]" simp}\\
2.27 -@{lemma "drop 6 [a,b,c,d] = []" simp}\\
2.28 -@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" simp}\\
2.29 -@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" simp}\\
2.30 -@{lemma "distinct [2,0,1::nat]" simp}\\
2.31 -@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" simp}\\
2.32 -@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" simp}\\
2.33 -@{lemma "nth [a,b,c,d] 2 = c" simp}\\
2.34 -@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" simp}\\
2.35 -@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" (simp add:sublist_def)}\\
2.36 -@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" (simp add:rotate1_def)}\\
2.37 -@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" (simp add:rotate1_def rotate_def nat_number)}\\
2.38 -@{lemma "replicate 4 a = [a,a,a,a]" (simp add:nat_number)}\\
2.39 -@{lemma "[2..<5] = [2,3,4]" (simp add:nat_number)}\\
2.40 -@{lemma "listsum [1,2,3::nat] = 6" simp}
2.41 +@{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
2.42 +@{lemma "length [a,b,c] = 3" by simp}\\
2.43 +@{lemma "set [a,b,c] = {a,b,c}" by simp}\\
2.44 +@{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
2.45 +@{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
2.46 +@{lemma "hd [a,b,c,d] = a" by simp}\\
2.47 +@{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
2.48 +@{lemma "last [a,b,c,d] = d" by simp}\\
2.49 +@{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
2.50 +@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
2.51 +@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
2.52 +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
2.53 +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
2.54 +@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
2.55 +@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
2.56 +@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
2.57 +@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
2.58 +@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
2.59 +@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
2.60 +@{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
2.61 +@{lemma "drop 6 [a,b,c,d] = []" by simp}\\
2.62 +@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
2.63 +@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
2.64 +@{lemma "distinct [2,0,1::nat]" by simp}\\
2.65 +@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
2.66 +@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
2.67 +@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
2.68 +@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
2.69 +@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
2.70 +@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
2.71 +@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
2.72 +@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
2.73 +@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
2.74 +@{lemma "listsum [1,2,3::nat] = 6" by simp}
2.75 \end{tabular}}
2.76 \caption{Characteristic examples}
2.77 \label{fig:Characteristic}
3.1 --- a/src/Pure/Thy/thy_output.ML Sat Jun 28 15:30:46 2008 +0200
3.2 +++ b/src/Pure/Thy/thy_output.ML Sat Jun 28 21:21:13 2008 +0200
3.3 @@ -463,15 +463,13 @@
3.4 val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
3.5 in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
3.6
3.7 -fun pretty_fact ctxt (prop, method_text) =
3.8 +fun pretty_lemma ctxt (prop, method_text) =
3.9 let
3.10 val _ = ctxt
3.11 |> Proof.theorem_i NONE (K I) [[(prop, [])]]
3.12 |> Proof.global_terminal_proof (method_text, NONE);
3.13 in pretty_term ctxt prop end;
3.14
3.15 -val hd_src = Args.src o (apfst o apsnd) (single o hd) o Args.dest_src;
3.16 -
3.17 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
3.18
3.19 fun pretty_term_style ctxt (name, t) =
3.20 @@ -529,11 +527,17 @@
3.21
3.22 (* commands *)
3.23
3.24 +val embedded_lemma =
3.25 + args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args))
3.26 + (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
3.27 +
3.28 +val _ = OuterKeyword.keyword "by";
3.29 +
3.30 val _ = add_commands
3.31 [("thm", args Attrib.thms (output_list pretty_thm)),
3.32 ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
3.33 ("prop", args Args.prop (output pretty_term)),
3.34 - ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact o hd_src)),
3.35 + ("lemma", embedded_lemma),
3.36 ("term", args Args.term (output pretty_term)),
3.37 ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
3.38 ("term_type", args Args.term (output pretty_term_typ)),