# HG changeset patch # User blanchet # Date 1277804331 -7200 # Node ID ff1137a9c0561b8375a98a4f5aed741b09970ee0 # Parent 1e99d8fc3d0716a4b4d29890027d429ea3fc4e4c# Parent df12f798df99ae3d6f462e6979d6de0977c22d20 merged diff -r df12f798df99 -r ff1137a9c056 NEWS --- a/NEWS Tue Jun 29 11:29:31 2010 +0200 +++ b/NEWS Tue Jun 29 11:38:51 2010 +0200 @@ -17,6 +17,26 @@ *** HOL *** +* Constant "split" has been merged with constant "prod_case"; names +of ML functions, facts etc. involving split have been retained so far, +though. INCOMPATIBILITY. + +* Dropped old infix syntax "mem" for List.member; use "in set" +instead. INCOMPATIBILITY. + +* Refactoring of code-generation specific operations in List.thy + + constants + null ~> List.null + + facts + mem_iff ~> member_def + null_empty ~> null_def + +INCOMPATIBILITY. Note that these were not suppossed to be used +regularly unless for striking reasons; their main purpose was code +generation. + * Some previously unqualified names have been qualified: types diff -r df12f798df99 -r ff1137a9c056 doc-src/Classes/Thy/document/Classes.tex --- a/doc-src/Classes/Thy/document/Classes.tex Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Classes/Thy/document/Classes.tex Tue Jun 29 11:38:51 2010 +0200 @@ -1166,14 +1166,14 @@ \hspace*{0pt} ~inverse ::~a -> a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ -\hspace*{0pt}inverse{\char95}int i = negate i;\\ +\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ +\hspace*{0pt}mult{\char95}int i j = i + j;\\ \hspace*{0pt}\\ \hspace*{0pt}neutral{\char95}int ::~Integer;\\ \hspace*{0pt}neutral{\char95}int = 0;\\ \hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ -\hspace*{0pt}mult{\char95}int i j = i + j;\\ +\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ +\hspace*{0pt}inverse{\char95}int i = negate i;\\ \hspace*{0pt}\\ \hspace*{0pt}instance Semigroup Integer where {\char123}\\ \hspace*{0pt} ~mult = mult{\char95}int;\\ @@ -1241,9 +1241,9 @@ \hspace*{0pt} ~type 'a group\\ \hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\ \hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\ -\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ +\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ \hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\ -\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ +\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ \hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ \hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\ \hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\ @@ -1275,11 +1275,11 @@ \hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\ \hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ +\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ \hspace*{0pt}\\ \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ \hspace*{0pt}\\ -\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ +\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ \hspace*{0pt}\\ \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ \hspace*{0pt}\\ diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/Inductive_Predicate.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Tue Jun 29 11:38:51 2010 +0200 @@ -0,0 +1,220 @@ +theory Inductive_Predicate +imports Setup +begin + +subsection {* Inductive Predicates *} +(*<*) +hide_const append + +inductive append +where + "append [] ys ys" +| "append xs ys zs ==> append (x # xs) ys (x # zs)" +(*>*) +text {* +To execute inductive predicates, a special preprocessor, the predicate + compiler, generates code equations from the introduction rules of the predicates. +The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. +Consider the simple predicate @{const append} given by these two +introduction rules: +*} +text %quote {* +@{thm append.intros(1)[of ys]}\\ +\noindent@{thm append.intros(2)[of xs ys zs x]} +*} +text {* +\noindent To invoke the compiler, simply use @{command_def "code_pred"}: +*} +code_pred %quote append . +text {* +\noindent The @{command "code_pred"} command takes the name +of the inductive predicate and then you put a period to discharge +a trivial correctness proof. +The compiler infers possible modes +for the predicate and produces the derived code equations. +Modes annotate which (parts of the) arguments are to be taken as input, +and which output. Modes are similar to types, but use the notation @{text "i"} +for input and @{text "o"} for output. + +For @{term "append"}, the compiler can infer the following modes: +\begin{itemize} +\item @{text "i \ i \ i \ bool"} +\item @{text "i \ i \ o \ bool"} +\item @{text "o \ o \ i \ bool"} +\end{itemize} +You can compute sets of predicates using @{command_def "values"}: +*} +values %quote "{zs. append [(1::nat),2,3] [4,5] zs}" +text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *} +values %quote "{(xs, ys). append xs ys [(2::nat),3]}" +text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *} +text {* +\noindent If you are only interested in the first elements of the set +comprehension (with respect to a depth-first search on the introduction rules), you can +pass an argument to +@{command "values"} to specify the number of elements you want: +*} + +values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}" +values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}" + +text {* +\noindent The @{command "values"} command can only compute set + comprehensions for which a mode has been inferred. + +The code equations for a predicate are made available as theorems with + the suffix @{text "equation"}, and can be inspected with: +*} +thm %quote append.equation +text {* +\noindent More advanced options are described in the following subsections. +*} +subsubsection {* Alternative names for functions *} +text {* +By default, the functions generated from a predicate are named after the predicate with the +mode mangled into the name (e.g., @{text "append_i_i_o"}). +You can specify your own names as follows: +*} +code_pred %quote (modes: i => i => o => bool as concat, + o => o => i => bool as split, + i => o => i => bool as suffix) append . + +subsubsection {* Alternative introduction rules *} +text {* +Sometimes the introduction rules of an predicate are not executable because they contain +non-executable constants or specific modes could not be inferred. +It is also possible that the introduction rules yield a function that loops forever +due to the execution in a depth-first search manner. +Therefore, you can declare alternative introduction rules for predicates with the attribute +@{attribute "code_pred_intro"}. +For example, the transitive closure is defined by: +*} +text %quote {* +@{thm tranclp.intros(1)[of r a b]}\\ +\noindent @{thm tranclp.intros(2)[of r a b c]} +*} +text {* +\noindent These rules do not suit well for executing the transitive closure +with the mode @{text "(i \ o \ bool) \ i \ o \ bool"}, as the second rule will +cause an infinite loop in the recursive call. +This can be avoided using the following alternative rules which are +declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}: +*} +lemma %quote [code_pred_intro]: + "r a b \ r\<^sup>+\<^sup>+ a b" + "r a b \ r\<^sup>+\<^sup>+ b c \ r\<^sup>+\<^sup>+ a c" +by auto +text {* +\noindent After declaring all alternative rules for the transitive closure, +you invoke @{command "code_pred"} as usual. +As you have declared alternative rules for the predicate, you are urged to prove that these +introduction rules are complete, i.e., that you can derive an elimination rule for the +alternative rules: +*} +code_pred %quote tranclp +proof - + case tranclp + from this converse_tranclpE[OF this(1)] show thesis by metis +qed +text {* +\noindent Alternative rules can also be used for constants that have not +been defined inductively. For example, the lexicographic order which +is defined as: *} +text %quote {* +@{thm [display] lexord_def[of "r"]} +*} +text {* +\noindent To make it executable, you can derive the following two rules and prove the +elimination rule: +*} +(*<*) +lemma append: "append xs ys zs = (xs @ ys = zs)" +by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros) +(*>*) +lemma %quote [code_pred_intro]: + "append xs (a # v) ys \ lexord r (xs, ys)" +(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) + +lemma %quote [code_pred_intro]: + "append u (a # v) xs \ append u (b # w) ys \ r (a, b) + \ lexord r (xs, ys)" +(*<*)unfolding lexord_def Collect_def append mem_def apply simp +apply (rule disjI2) by auto +(*>*) + +code_pred %quote lexord +(*<*) +proof - + fix r xs ys + assume lexord: "lexord r (xs, ys)" + assume 1: "\ r' xs' ys' a v. r = r' \ (xs, ys) = (xs', ys') \ append xs' (a # v) ys' \ thesis" + assume 2: "\ r' xs' ys' u a v b w. r = r' \ (xs, ys) = (xs', ys') \ append u (a # v) xs' \ append u (b # w) ys' \ r' (a, b) \ thesis" + { + assume "\a v. ys = xs @ a # v" + from this 1 have thesis + by (fastsimp simp add: append) + } moreover + { + assume "\u a b v w. (a, b) \ r \ xs = u @ a # v \ ys = u @ b # w" + from this 2 have thesis by (fastsimp simp add: append mem_def) + } moreover + note lexord + ultimately show thesis + unfolding lexord_def + by (fastsimp simp add: Collect_def) +qed +(*>*) +subsubsection {* Options for values *} +text {* +In the presence of higher-order predicates, multiple modes for some predicate could be inferred +that are not disambiguated by the pattern of the set comprehension. +To disambiguate the modes for the arguments of a predicate, you can state +the modes explicitly in the @{command "values"} command. +Consider the simple predicate @{term "succ"}: +*} +inductive succ :: "nat \ nat \ bool" +where + "succ 0 (Suc 0)" +| "succ x y \ succ (Suc x) (Suc y)" + +code_pred succ . + +text {* +\noindent For this, the predicate compiler can infer modes @{text "o \ o \ bool"}, @{text "i \ o \ bool"}, + @{text "o \ i \ bool"} and @{text "i \ i \ bool"}. +The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple +modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \ o \ bool"} +is chosen. To choose another mode for the argument, you can declare the mode for the argument between +the @{command "values"} and the number of elements. +*} +values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}" +values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}" + +subsubsection {* Embedding into functional code within Isabelle/HOL *} +text {* +To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL, +you have a number of options: +\begin{itemize} +\item You want to use the first-order predicate with the mode + where all arguments are input. Then you can use the predicate directly, e.g. +\begin{quote} + @{text "valid_suffix ys zs = "}\\ + @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"} +\end{quote} +\item If you know that the execution returns only one value (it is deterministic), then you can + use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists + is defined with +\begin{quote} + @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"} +\end{quote} + Note that if the evaluation does not return a unique value, it raises a run-time error + @{term "not_unique"}. +\end{itemize} +*} +subsubsection {* Further Examples *} +text {* Further examples for compiling inductive predicates can be found in +the @{text "HOL/ex/Predicate_Compile_ex"} theory file. +There are also some examples in the Archive of Formal Proofs, notably +in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions. +*} +end diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/ML.thy Tue Jun 29 11:38:51 2010 +0200 @@ -31,7 +31,7 @@ @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ @{index_ML Code.get_type: "theory -> string - -> (string * sort) list * (string * typ list) list"} \\ + -> (string * sort) list * ((string * string list) * typ list) list"} \\ @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} \end{mldecls} diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/Program.thy --- a/doc-src/Codegen/Thy/Program.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/Program.thy Tue Jun 29 11:38:51 2010 +0200 @@ -174,7 +174,7 @@ *} lemma %quote [code_unfold]: - "x \ set xs \ member xs x" by (fact in_set_code) + "x \ set xs \ List.member xs x" by (fact in_set_member) text {* \item eliminating superfluous constants: @@ -188,7 +188,7 @@ *} lemma %quote [code_unfold]: - "xs = [] \ List.null xs" by (fact empty_null) + "xs = [] \ List.null xs" by (fact eq_Nil_null) text_raw {* \end{itemize} @@ -339,7 +339,7 @@ else collect_duplicates (z#xs) (z#ys) zs)" text {* - \noindent The membership test during preprocessing is rewritten, + \noindent During preprocessing, the membership test is rewritten, resulting in @{const List.member}, which itself performs an explicit equality check. *} @@ -429,219 +429,4 @@ likely to be used in such situations. *} -subsection {* Inductive Predicates *} -(*<*) -hide_const append - -inductive append -where - "append [] ys ys" -| "append xs ys zs ==> append (x # xs) ys (x # zs)" -(*>*) -text {* -To execute inductive predicates, a special preprocessor, the predicate - compiler, generates code equations from the introduction rules of the predicates. -The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. -Consider the simple predicate @{const append} given by these two -introduction rules: -*} -text %quote {* -@{thm append.intros(1)[of ys]}\\ -\noindent@{thm append.intros(2)[of xs ys zs x]} -*} -text {* -\noindent To invoke the compiler, simply use @{command_def "code_pred"}: -*} -code_pred %quote append . -text {* -\noindent The @{command "code_pred"} command takes the name -of the inductive predicate and then you put a period to discharge -a trivial correctness proof. -The compiler infers possible modes -for the predicate and produces the derived code equations. -Modes annotate which (parts of the) arguments are to be taken as input, -and which output. Modes are similar to types, but use the notation @{text "i"} -for input and @{text "o"} for output. - -For @{term "append"}, the compiler can infer the following modes: -\begin{itemize} -\item @{text "i \ i \ i \ bool"} -\item @{text "i \ i \ o \ bool"} -\item @{text "o \ o \ i \ bool"} -\end{itemize} -You can compute sets of predicates using @{command_def "values"}: -*} -values %quote "{zs. append [(1::nat),2,3] [4,5] zs}" -text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *} -values %quote "{(xs, ys). append xs ys [(2::nat),3]}" -text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *} -text {* -\noindent If you are only interested in the first elements of the set -comprehension (with respect to a depth-first search on the introduction rules), you can -pass an argument to -@{command "values"} to specify the number of elements you want: -*} - -values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}" -values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}" - -text {* -\noindent The @{command "values"} command can only compute set - comprehensions for which a mode has been inferred. - -The code equations for a predicate are made available as theorems with - the suffix @{text "equation"}, and can be inspected with: -*} -thm %quote append.equation -text {* -\noindent More advanced options are described in the following subsections. -*} -subsubsection {* Alternative names for functions *} -text {* -By default, the functions generated from a predicate are named after the predicate with the -mode mangled into the name (e.g., @{text "append_i_i_o"}). -You can specify your own names as follows: -*} -code_pred %quote (modes: i => i => o => bool as concat, - o => o => i => bool as split, - i => o => i => bool as suffix) append . - -subsubsection {* Alternative introduction rules *} -text {* -Sometimes the introduction rules of an predicate are not executable because they contain -non-executable constants or specific modes could not be inferred. -It is also possible that the introduction rules yield a function that loops forever -due to the execution in a depth-first search manner. -Therefore, you can declare alternative introduction rules for predicates with the attribute -@{attribute "code_pred_intro"}. -For example, the transitive closure is defined by: -*} -text %quote {* -@{thm tranclp.intros(1)[of r a b]}\\ -\noindent @{thm tranclp.intros(2)[of r a b c]} -*} -text {* -\noindent These rules do not suit well for executing the transitive closure -with the mode @{text "(i \ o \ bool) \ i \ o \ bool"}, as the second rule will -cause an infinite loop in the recursive call. -This can be avoided using the following alternative rules which are -declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}: -*} -lemma %quote [code_pred_intro]: - "r a b \ r\<^sup>+\<^sup>+ a b" - "r a b \ r\<^sup>+\<^sup>+ b c \ r\<^sup>+\<^sup>+ a c" -by auto -text {* -\noindent After declaring all alternative rules for the transitive closure, -you invoke @{command "code_pred"} as usual. -As you have declared alternative rules for the predicate, you are urged to prove that these -introduction rules are complete, i.e., that you can derive an elimination rule for the -alternative rules: -*} -code_pred %quote tranclp -proof - - case tranclp - from this converse_tranclpE[OF this(1)] show thesis by metis -qed -text {* -\noindent Alternative rules can also be used for constants that have not -been defined inductively. For example, the lexicographic order which -is defined as: *} -text %quote {* -@{thm [display] lexord_def[of "r"]} -*} -text {* -\noindent To make it executable, you can derive the following two rules and prove the -elimination rule: -*} -(*<*) -lemma append: "append xs ys zs = (xs @ ys = zs)" -by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros) -(*>*) -lemma %quote [code_pred_intro]: - "append xs (a # v) ys \ lexord r (xs, ys)" -(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) - -lemma %quote [code_pred_intro]: - "append u (a # v) xs \ append u (b # w) ys \ r (a, b) - \ lexord r (xs, ys)" -(*<*)unfolding lexord_def Collect_def append mem_def apply simp -apply (rule disjI2) by auto -(*>*) - -code_pred %quote lexord -(*<*) -proof - - fix r xs ys - assume lexord: "lexord r (xs, ys)" - assume 1: "\ r' xs' ys' a v. r = r' \ (xs, ys) = (xs', ys') \ append xs' (a # v) ys' \ thesis" - assume 2: "\ r' xs' ys' u a v b w. r = r' \ (xs, ys) = (xs', ys') \ append u (a # v) xs' \ append u (b # w) ys' \ r' (a, b) \ thesis" - { - assume "\a v. ys = xs @ a # v" - from this 1 have thesis - by (fastsimp simp add: append) - } moreover - { - assume "\u a b v w. (a, b) \ r \ xs = u @ a # v \ ys = u @ b # w" - from this 2 have thesis by (fastsimp simp add: append mem_def) - } moreover - note lexord - ultimately show thesis - unfolding lexord_def - by (fastsimp simp add: Collect_def) -qed -(*>*) -subsubsection {* Options for values *} -text {* -In the presence of higher-order predicates, multiple modes for some predicate could be inferred -that are not disambiguated by the pattern of the set comprehension. -To disambiguate the modes for the arguments of a predicate, you can state -the modes explicitly in the @{command "values"} command. -Consider the simple predicate @{term "succ"}: -*} -inductive succ :: "nat \ nat \ bool" -where - "succ 0 (Suc 0)" -| "succ x y \ succ (Suc x) (Suc y)" - -code_pred succ . - -text {* -\noindent For this, the predicate compiler can infer modes @{text "o \ o \ bool"}, @{text "i \ o \ bool"}, - @{text "o \ i \ bool"} and @{text "i \ i \ bool"}. -The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple -modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \ o \ bool"} -is chosen. To choose another mode for the argument, you can declare the mode for the argument between -the @{command "values"} and the number of elements. -*} -values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}" -values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}" - -subsubsection {* Embedding into functional code within Isabelle/HOL *} -text {* -To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL, -you have a number of options: -\begin{itemize} -\item You want to use the first-order predicate with the mode - where all arguments are input. Then you can use the predicate directly, e.g. -\begin{quote} - @{text "valid_suffix ys zs = "}\\ - @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"} -\end{quote} -\item If you know that the execution returns only one value (it is deterministic), then you can - use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists - is defined with -\begin{quote} - @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"} -\end{quote} - Note that if the evaluation does not return a unique value, it raises a run-time error - @{term "not_unique"}. -\end{itemize} -*} -subsubsection {* Further Examples *} -text {* Further examples for compiling inductive predicates can be found in -the @{text "HOL/ex/Predicate_Compile_ex"} theory file. -There are also some examples in the Archive of Formal Proofs, notably -in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions. -*} end diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/ROOT.ML --- a/doc-src/Codegen/Thy/ROOT.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/ROOT.ML Tue Jun 29 11:38:51 2010 +0200 @@ -4,6 +4,7 @@ use_thy "Introduction"; use_thy "Program"; +use_thy "Inductive_Predicate"; use_thy "Adaptation"; use_thy "Further"; use_thy "ML"; diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Tue Jun 29 11:38:51 2010 +0200 @@ -0,0 +1,491 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Inductive{\isacharunderscore}Predicate}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Inductive{\isacharunderscore}Predicate\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsubsection{Inductive Predicates% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +To execute inductive predicates, a special preprocessor, the predicate + compiler, generates code equations from the introduction rules of the predicates. +The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. +Consider the simple predicate \isa{append} given by these two +introduction rules:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\ +\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ append\ \isacommand{{\isachardot}}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name +of the inductive predicate and then you put a period to discharge +a trivial correctness proof. +The compiler infers possible modes +for the predicate and produces the derived code equations. +Modes annotate which (parts of the) arguments are to be taken as input, +and which output. Modes are similar to types, but use the notation \isa{i} +for input and \isa{o} for output. + +For \isa{append}, the compiler can infer the following modes: +\begin{itemize} +\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} +\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} +\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} +\end{itemize} +You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\noindent If you are only interested in the first elements of the set +comprehension (with respect to a depth-first search on the introduction rules), you can +pass an argument to +\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\isacommand{values}\isamarkupfalse% +\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set + comprehensions for which a mode has been inferred. + +The code equations for a predicate are made available as theorems with + the suffix \isa{equation}, and can be inspected with:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{thm}\isamarkupfalse% +\ append{\isachardot}equation% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent More advanced options are described in the following subsections.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Alternative names for functions% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +By default, the functions generated from a predicate are named after the predicate with the +mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). +You can specify your own names as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline +\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline +\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsubsection{Alternative introduction rules% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Sometimes the introduction rules of an predicate are not executable because they contain +non-executable constants or specific modes could not be inferred. +It is also possible that the introduction rules yield a function that loops forever +due to the execution in a depth-first search manner. +Therefore, you can declare alternative introduction rules for predicates with the attribute +\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}. +For example, the transitive closure is defined by:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\ +\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent These rules do not suit well for executing the transitive closure +with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will +cause an infinite loop in the recursive call. +This can be avoided using the following alternative rules which are +declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline +\isacommand{by}\isamarkupfalse% +\ auto% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent After declaring all alternative rules for the transitive closure, +you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. +As you have declared alternative rules for the predicate, you are urged to prove that these +introduction rules are complete, i.e., that you can derive an elimination rule for the +alternative rules:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ tranclp\isanewline +\isacommand{proof}\isamarkupfalse% +\ {\isacharminus}\isanewline +\ \ \isacommand{case}\isamarkupfalse% +\ tranclp\isanewline +\ \ \isacommand{from}\isamarkupfalse% +\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse% +\ thesis\ \isacommand{by}\isamarkupfalse% +\ metis\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Alternative rules can also be used for constants that have not +been defined inductively. For example, the lexicographic order which +is defined as:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\begin{isabelle}% +lexord\ r\ {\isacharequal}\isanewline +{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline +\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline +\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}% +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent To make it executable, you can derive the following two rules and prove the +elimination rule:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ lexord% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsubsection{Options for values% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +In the presence of higher-order predicates, multiple modes for some predicate could be inferred +that are not disambiguated by the pattern of the set comprehension. +To disambiguate the modes for the arguments of a predicate, you can state +the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. +Consider the simple predicate \isa{succ}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive}\isamarkupfalse% +\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ succ% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{{\isachardot}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, + \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. +The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple +modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} +is chosen. To choose another mode for the argument, you can declare the mode for the argument between +the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\isacommand{values}\isamarkupfalse% +\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL, +you have a number of options: +\begin{itemize} +\item You want to use the first-order predicate with the mode + where all arguments are input. Then you can use the predicate directly, e.g. +\begin{quote} + \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\ + \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}} +\end{quote} +\item If you know that the execution returns only one value (it is deterministic), then you can + use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists + is defined with +\begin{quote} + \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}} +\end{quote} + Note that if the evaluation does not return a unique value, it raises a run-time error + \isa{not{\isacharunderscore}unique}. +\end{itemize}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Further Examples% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Further examples for compiling inductive predicates can be found in +the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file. +There are also some examples in the Archive of Formal Proofs, notably +in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Jun 29 11:38:51 2010 +0200 @@ -149,7 +149,6 @@ \hspace*{0pt}structure Example :~sig\\ \hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ \hspace*{0pt} ~val rev :~'a list -> 'a list\\ -\hspace*{0pt} ~val list{\char95}case :~'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a\\ \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ \hspace*{0pt} ~val empty :~'a queue\\ \hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ @@ -161,9 +160,6 @@ \hspace*{0pt}\\ \hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\ -\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\ -\hspace*{0pt}\\ \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ \hspace*{0pt}\\ \hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ @@ -234,10 +230,6 @@ \noindent% \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\ -\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\ -\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\ -\hspace*{0pt}\\ \hspace*{0pt}data Queue a = AQueue [a] [a];\\ \hspace*{0pt}\\ \hspace*{0pt}empty ::~forall a.~Queue a;\\ @@ -248,7 +240,7 @@ \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ \hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ \hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\ +\hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\ \hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ \hspace*{0pt}\\ \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/document/ML.tex --- a/doc-src/Codegen/Thy/document/ML.tex Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/document/ML.tex Tue Jun 29 11:38:51 2010 +0200 @@ -61,7 +61,7 @@ \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% -\verb| -> (string * sort) list * (string * typ list) list| \\ +\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| \end{mldecls} diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Program.tex Tue Jun 29 11:38:51 2010 +0200 @@ -89,8 +89,8 @@ \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ \hspace*{0pt}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\ -\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));% +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % @@ -292,13 +292,13 @@ \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ \hspace*{0pt}\\ +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ \hspace*{0pt}instance Semigroup Nat where {\char123}\\ \hspace*{0pt} ~mult = mult{\char95}nat;\\ \hspace*{0pt}{\char125};\\ @@ -346,8 +346,8 @@ \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ \hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ \hspace*{0pt} ~val neutral{\char95}nat :~nat\\ -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ \hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ \hspace*{0pt} ~val bexp :~nat -> nat\\ @@ -368,11 +368,11 @@ \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ \hspace*{0pt}\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ \hspace*{0pt}\\ \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ @@ -434,8 +434,8 @@ \isatagquote \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}code{\isacharparenright}% +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% \endisatagquote {\isafoldquote}% % @@ -477,7 +477,7 @@ \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ empty{\isacharunderscore}null{\isacharparenright}% +\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% \endisatagquote {\isafoldquote}% % @@ -763,8 +763,8 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent The membership test during preprocessing is rewritten, - resulting in \isa{member}, which itself +\noindent During preprocessing, the membership test is rewritten, + resulting in \isa{List{\isachardot}member}, which itself performs an explicit equality check.% \end{isamarkuptext}% \isamarkuptrue% @@ -878,7 +878,7 @@ \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ \hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = rev xs;\\ +\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ \hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% \end{isamarkuptext}% @@ -972,7 +972,8 @@ \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue (AQueue [] (rev xs)));% +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % @@ -991,458 +992,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Inductive Predicates% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -To execute inductive predicates, a special preprocessor, the predicate - compiler, generates code equations from the introduction rules of the predicates. -The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. -Consider the simple predicate \isa{append} given by these two -introduction rules:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\ -\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ append\ \isacommand{{\isachardot}}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name -of the inductive predicate and then you put a period to discharge -a trivial correctness proof. -The compiler infers possible modes -for the predicate and produces the derived code equations. -Modes annotate which (parts of the) arguments are to be taken as input, -and which output. Modes are similar to types, but use the notation \isa{i} -for input and \isa{o} for output. - -For \isa{append}, the compiler can infer the following modes: -\begin{itemize} -\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} -\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} -\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} -\end{itemize} -You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -\noindent If you are only interested in the first elements of the set -comprehension (with respect to a depth-first search on the introduction rules), you can -pass an argument to -\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline -\isacommand{values}\isamarkupfalse% -\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set - comprehensions for which a mode has been inferred. - -The code equations for a predicate are made available as theorems with - the suffix \isa{equation}, and can be inspected with:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{thm}\isamarkupfalse% -\ append{\isachardot}equation% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent More advanced options are described in the following subsections.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Alternative names for functions% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -By default, the functions generated from a predicate are named after the predicate with the -mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). -You can specify your own names as follows:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline -\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline -\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isamarkupsubsubsection{Alternative introduction rules% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Sometimes the introduction rules of an predicate are not executable because they contain -non-executable constants or specific modes could not be inferred. -It is also possible that the introduction rules yield a function that loops forever -due to the execution in a depth-first search manner. -Therefore, you can declare alternative introduction rules for predicates with the attribute -\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}. -For example, the transitive closure is defined by:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\ -\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent These rules do not suit well for executing the transitive closure -with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will -cause an infinite loop in the recursive call. -This can be avoided using the following alternative rules which are -declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline -\isacommand{by}\isamarkupfalse% -\ auto% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent After declaring all alternative rules for the transitive closure, -you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. -As you have declared alternative rules for the predicate, you are urged to prove that these -introduction rules are complete, i.e., that you can derive an elimination rule for the -alternative rules:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ tranclp\isanewline -\isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ tranclp\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse% -\ thesis\ \isacommand{by}\isamarkupfalse% -\ metis\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Alternative rules can also be used for constants that have not -been defined inductively. For example, the lexicographic order which -is defined as:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\begin{isabelle}% -lexord\ r\ {\isacharequal}\isanewline -{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline -\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline -\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}% -\end{isabelle}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent To make it executable, you can derive the following two rules and prove the -elimination rule:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline -\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ lexord% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isamarkupsubsubsection{Options for values% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -In the presence of higher-order predicates, multiple modes for some predicate could be inferred -that are not disambiguated by the pattern of the set comprehension. -To disambiguate the modes for the arguments of a predicate, you can state -the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. -Consider the simple predicate \isa{succ}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{inductive}\isamarkupfalse% -\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline -\isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline -{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ succ% -\isadelimproof -\ % -\endisadelimproof -% -\isatagproof -\isacommand{{\isachardot}}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, - \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. -The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple -modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} -is chosen. To choose another mode for the argument, you can declare the mode for the argument between -the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline -\isacommand{values}\isamarkupfalse% -\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL, -you have a number of options: -\begin{itemize} -\item You want to use the first-order predicate with the mode - where all arguments are input. Then you can use the predicate directly, e.g. -\begin{quote} - \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\ - \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}} -\end{quote} -\item If you know that the execution returns only one value (it is deterministic), then you can - use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists - is defined with -\begin{quote} - \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}} -\end{quote} - Note that if the evaluation does not return a unique value, it raises a run-time error - \isa{not{\isacharunderscore}unique}. -\end{itemize}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Further Examples% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Further examples for compiling inductive predicates can be found in -the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file. -There are also some examples in the Archive of Formal Proofs, notably -in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isadelimtheory % \endisadelimtheory diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/examples/Example.hs Tue Jun 29 11:38:51 2010 +0200 @@ -2,10 +2,6 @@ module Example where { -list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a; -list_case f1 f2 (a : list) = f2 a list; -list_case f1 f2 [] = f1; - data Queue a = AQueue [a] [a]; empty :: forall a. Queue a; @@ -16,7 +12,7 @@ dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys); dequeue (AQueue (v : va) []) = let { - (y : ys) = rev (v : va); + (y : ys) = reverse (v : va); } in (Just y, AQueue [] ys); enqueue :: forall a. a -> Queue a -> Queue a; diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/Thy/examples/example.ML --- a/doc-src/Codegen/Thy/examples/example.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/Thy/examples/example.ML Tue Jun 29 11:38:51 2010 +0200 @@ -1,7 +1,6 @@ structure Example : sig val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a val rev : 'a list -> 'a list - val list_case : 'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a datatype 'a queue = AQueue of 'a list * 'a list val empty : 'a queue val dequeue : 'a queue -> 'a option * 'a queue @@ -13,9 +12,6 @@ fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs; -fun list_case f1 f2 (a :: lista) = f2 a lista - | list_case f1 f2 [] = f1; - datatype 'a queue = AQueue of 'a list * 'a list; val empty : 'a queue = AQueue ([], []); diff -r df12f798df99 -r ff1137a9c056 doc-src/Codegen/codegen.tex --- a/doc-src/Codegen/codegen.tex Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/Codegen/codegen.tex Tue Jun 29 11:38:51 2010 +0200 @@ -32,6 +32,7 @@ \input{Thy/document/Introduction.tex} \input{Thy/document/Program.tex} +\input{Thy/document/Inductive_Predicate.tex} \input{Thy/document/Adaptation.tex} \input{Thy/document/Further.tex} \input{Thy/document/ML.tex} diff -r df12f798df99 -r ff1137a9c056 doc-src/TutorialI/Types/document/Pairs.tex --- a/doc-src/TutorialI/Types/document/Pairs.tex Tue Jun 29 11:29:31 2010 +0200 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Tue Jun 29 11:38:51 2010 +0200 @@ -60,7 +60,7 @@ Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where \cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as \begin{center} -\isa{split\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}} +\isa{prod{\isacharunderscore}case\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}} \hfill(\isa{split{\isacharunderscore}def}) \end{center} Pattern matching in @@ -74,7 +74,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The most obvious approach is the brute force expansion of \isa{split}:% +The most obvious approach is the brute force expansion of \isa{prod{\isacharunderscore}case}:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% @@ -105,10 +105,10 @@ If we consider why this lemma presents a problem, we realize that we need to replace variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the equation would simplify to \isa{a} by the simplification rules -\isa{split\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. +\isa{prod{\isacharunderscore}case\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. To reason about tuple patterns requires some way of converting a variable of product type into a pair. -In case of a subterm of the form \isa{split\ f\ p} this is easy: the split +In case of a subterm of the form \isa{prod{\isacharunderscore}case\ f\ p} this is easy: the split rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:% \index{*split (method)}% \end{isamarkuptext}% @@ -169,7 +169,7 @@ {\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p% +\ {\isadigit{1}}{\isachardot}\ case\ p\ of\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymRightarrow}\ fst\ p\ {\isacharequal}\ x% \end{isabelle} A paired \isa{let} reduces to a paired $\lambda$-abstraction, which can be split as above. The same is true for paired set comprehension:% @@ -194,7 +194,7 @@ \ simp% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% +\ {\isadigit{1}}{\isachardot}\ prod{\isacharunderscore}case\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% \end{isabelle} Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split} as above. If you are worried about the strange form of the premise: @@ -220,9 +220,9 @@ \begin{isamarkuptxt}% \noindent except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because -\isa{split} occurs in the assumptions. +\isa{prod{\isacharunderscore}case} occurs in the assumptions. -However, splitting \isa{split} is not always a solution, as no \isa{split} +However, splitting \isa{prod{\isacharunderscore}case} is not always a solution, as no \isa{prod{\isacharunderscore}case} may be present in the goal. Consider the following function:% \end{isamarkuptxt}% \isamarkuptrue% @@ -253,7 +253,7 @@ \noindent simplification will do nothing, because the defining equation for \isa{swap} expects a pair. Again, we need to turn \isa{p} -into a pair first, but this time there is no \isa{split} in sight. +into a pair first, but this time there is no \isa{prod{\isacharunderscore}case} in sight. The only thing we can do is to split the term by hand:% \end{isamarkuptxt}% \isamarkuptrue% diff -r df12f798df99 -r ff1137a9c056 src/HOL/Auth/Guard/Guard.thy --- a/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 11:38:51 2010 +0200 @@ -201,14 +201,16 @@ lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" by (induct l, auto) -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" -by (induct l, auto) +lemma mem_cnb_minus: "x \ set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" + by (induct l) auto lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x" +lemma cnb_minus [simp]: "x \ set l ==> cnb (remove l x) = cnb l - crypt_nb x" apply (induct l, auto) -by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp) +apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI) +apply simp +done lemma parts_cnb: "Z:parts (set l) ==> cnb l = (cnb l - crypt_nb Z) + crypt_nb Z" @@ -272,7 +274,7 @@ apply (clarsimp, blast) (* K ~:invKey`Ks *) apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))") -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff) +apply (drule_tac x="decrypt' l' K Y" in spec, simp) apply (subgoal_tac "Crypt K Y:parts (set l)") apply (drule parts_cnb, rotate_tac -1, simp) apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Auth/Guard/GuardK.thy --- a/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 11:38:51 2010 +0200 @@ -197,12 +197,12 @@ lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" by (induct l, auto) -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" +lemma mem_cnb_minus: "x \ set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" by (induct l, auto) lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x" +lemma cnb_minus [simp]: "x \ set l ==> cnb (remove l x) = cnb l - crypt_nb x" apply (induct l, auto) by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp) @@ -268,7 +268,7 @@ apply (clarsimp, blast) (* K ~:invKey`Ks *) apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))") -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff) +apply (drule_tac x="decrypt' l' K Y" in spec, simp) apply (subgoal_tac "Crypt K Y:parts (set l)") apply (drule parts_cnb, rotate_tac -1, simp) apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Bali/Trans.thy --- a/src/HOL/Bali/Trans.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Bali/Trans.thy Tue Jun 29 11:38:51 2010 +0200 @@ -10,7 +10,7 @@ theory Trans imports Evaln begin definition groundVar :: "var \ bool" where -"groundVar v \ (case v of +"groundVar v \ (case v of LVar ln \ True | {accC,statDeclC,stat}e..fn \ \ a. e=Lit a | e1.[e2] \ \ a i. e1= Lit a \ e2 = Lit i @@ -35,19 +35,15 @@ qed definition groundExprs :: "expr list \ bool" where -"groundExprs es \ list_all (\ e. \ v. e=Lit v) es" + "groundExprs es \ (\e \ set es. \v. e = Lit v)" -consts the_val:: "expr \ val" -primrec -"the_val (Lit v) = v" +primrec the_val:: "expr \ val" where + "the_val (Lit v) = v" -consts the_var:: "prog \ state \ var \ (vvar \ state)" -primrec -"the_var G s (LVar ln) =(lvar ln (store s),s)" -the_var_FVar_def: -"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" -the_var_AVar_def: -"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" +primrec the_var:: "prog \ state \ var \ (vvar \ state)" where + "the_var G s (LVar ln) =(lvar ln (store s),s)" +| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" +| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" lemma the_var_FVar_simp[simp]: "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 11:38:51 2010 +0200 @@ -425,7 +425,7 @@ lemma poly_exp_eq_zero: "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \ 0)" -apply (simp only: fun_eq add: all_simps [symmetric]) +apply (simp only: fun_eq add: HOL.all_simps [symmetric]) apply (rule arg_cong [where f = All]) apply (rule ext) apply (induct_tac "n") diff -r df12f798df99 -r ff1137a9c056 src/HOL/Extraction/Euclid.thy --- a/src/HOL/Extraction/Euclid.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Extraction/Euclid.thy Tue Jun 29 11:38:51 2010 +0200 @@ -44,7 +44,7 @@ done lemma prime_eq': "prime (p::nat) = (1 < p \ (\m k. p = m * k \ 1 < m \ m = p))" - by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps) + by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps) lemma not_prime_ex_mk: assumes n: "Suc 0 < n" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Extraction/Warshall.thy --- a/src/HOL/Extraction/Warshall.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Extraction/Warshall.thy Tue Jun 29 11:38:51 2010 +0200 @@ -38,7 +38,7 @@ "\x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \ r y z = T)" by (induct ys) simp+ -theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \ list_all P xs)" +theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \ P x \ list_all P xs" by (induct xs, simp+, iprover) theorem list_all_lemma: diff -r df12f798df99 -r ff1137a9c056 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Jun 29 11:38:51 2010 +0200 @@ -68,7 +68,7 @@ fun mk_abstuple [x] body = abs (x, body) | mk_abstuple (x::xs) body = - Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); + Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body); fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b | mk_fbody a e ((b,_)::xs) = @@ -128,21 +128,21 @@ (*** print translations ***) ML{* -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = +fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) = subst_bound (Syntax.free v, dest_abstuple body) | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) | dest_abstuple trm = trm; -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t +fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t | abs2list (Abs(x,T,t)) = [Free (x, T)] | abs2list _ = []; -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t +fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t | mk_ts (Abs(x,_,t)) = mk_ts t | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) | mk_ts t = [t]; -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = +fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = ((Syntax.free x)::(abs2list t), mk_ts t) | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) | mk_vts t = raise Match; @@ -152,7 +152,7 @@ if t = Bound i then find_ch vts (i-1) xs else (true, (v, subst_bounds (xs, t))); -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true +fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true | is_f (Abs(x,_,t)) = true | is_f t = false; *} diff -r df12f798df99 -r ff1137a9c056 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Jun 29 11:38:51 2010 +0200 @@ -70,7 +70,7 @@ fun mk_abstuple [x] body = abs (x, body) | mk_abstuple (x::xs) body = - Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); + Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body); fun mk_fbody a e [x as (b,_)] = if a=b then e else free b | mk_fbody a e ((b,_)::xs) = @@ -130,21 +130,21 @@ (*** print translations ***) ML{* -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = +fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) = subst_bound (Syntax.free v, dest_abstuple body) | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) | dest_abstuple trm = trm; -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t +fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t | abs2list (Abs(x,T,t)) = [Free (x, T)] | abs2list _ = []; -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t +fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t | mk_ts (Abs(x,_,t)) = mk_ts t | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) | mk_ts t = [t]; -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = +fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = ((Syntax.free x)::(abs2list t), mk_ts t) | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) | mk_vts t = raise Match; @@ -154,7 +154,7 @@ if t = Bound i then find_ch vts (i-1) xs else (true, (v, subst_bounds (xs,t))); -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true +fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true | is_f (Abs(x,_,t)) = true | is_f t = false; *} diff -r df12f798df99 -r ff1137a9c056 src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Tue Jun 29 11:38:51 2010 +0200 @@ -16,7 +16,7 @@ local open HOLogic in (** maps (%x1 ... xn. t) to [x1,...,xn] **) -fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t +fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t | abs2list (Abs (x, T, t)) = [Free (x, T)] | abs2list _ = []; @@ -32,7 +32,7 @@ else let val z = mk_abstupleC w body; val T2 = case z of Abs(_,T,_) => T | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T; - in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) + in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) $ absfree (n, T, z) end end; (** maps [x1,...,xn] to (x1,...,xn) and types**) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 29 11:38:51 2010 +0200 @@ -379,7 +379,7 @@ from this Inl 1(1) exec_f mrec show ?thesis proof (cases "ret_mrec") case (Inl aaa) - from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3) + from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3) show ?thesis apply auto apply (rule rec_case) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Import/HOL/HOL4Base.thy --- a/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 11:38:51 2010 +0200 @@ -3130,7 +3130,7 @@ by (import list EVERY_MEM) lemma EXISTS_MEM: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P l = (EX e::'a::type. e mem l & P e)" + list_ex P l = (EX e::'a::type. e mem l & P e)" by (import list EXISTS_MEM) lemma MEM_APPEND: "ALL (e::'a::type) (l1::'a::type list) l2::'a::type list. @@ -3138,15 +3138,15 @@ by (import list MEM_APPEND) lemma EXISTS_APPEND: "ALL (P::'a::type => bool) (l1::'a::type list) l2::'a::type list. - list_exists P (l1 @ l2) = (list_exists P l1 | list_exists P l2)" + list_ex P (l1 @ l2) = (list_ex P l1 | list_ex P l2)" by (import list EXISTS_APPEND) lemma NOT_EVERY: "ALL (P::'a::type => bool) l::'a::type list. - (~ list_all P l) = list_exists (Not o P) l" + (~ list_all P l) = list_ex (Not o P) l" by (import list NOT_EVERY) lemma NOT_EXISTS: "ALL (P::'a::type => bool) l::'a::type list. - (~ list_exists P l) = list_all (Not o P) l" + (~ list_ex P l) = list_all (Not o P) l" by (import list NOT_EXISTS) lemma MEM_MAP: "ALL (l::'a::type list) (f::'a::type => 'b::type) x::'b::type. @@ -3220,7 +3220,7 @@ lemma EXISTS_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool) P'::'a::type => bool. l1 = l2 & (ALL x::'a::type. x mem l2 --> P x = P' x) --> - list_exists P l1 = list_exists P' l2" + list_ex P l1 = list_ex P' l2" by (import list EXISTS_CONG) lemma EVERY_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool) @@ -4598,7 +4598,7 @@ SCANR f e (x # l) = f x (hd (SCANR f e l)) # SCANR f e l)" by (import rich_list SCANR) -lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l" +lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l" by (import rich_list IS_EL_DEF) definition AND_EL :: "bool list => bool" where @@ -4608,9 +4608,9 @@ by (import rich_list AND_EL_DEF) definition OR_EL :: "bool list => bool" where - "OR_EL == list_exists I" - -lemma OR_EL_DEF: "OR_EL = list_exists I" + "OR_EL == list_ex I" + +lemma OR_EL_DEF: "OR_EL = list_ex I" by (import rich_list OR_EL_DEF) consts @@ -4937,7 +4937,7 @@ by (import rich_list ALL_EL_MAP) lemma SOME_EL_SNOC: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list. - list_exists P (SNOC x l) = (P x | list_exists P l)" + list_ex P (SNOC x l) = (P x | list_ex P l)" by (import rich_list SOME_EL_SNOC) lemma IS_EL_SNOC: "ALL (y::'a::type) (x::'a::type) l::'a::type list. @@ -5080,11 +5080,11 @@ by (import rich_list ALL_EL_FOLDL) lemma SOME_EL_FOLDR: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P l = foldr (%x::'a::type. op | (P x)) l False" + list_ex P l = foldr (%x::'a::type. op | (P x)) l False" by (import rich_list SOME_EL_FOLDR) lemma SOME_EL_FOLDL: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l" + list_ex P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l" by (import rich_list SOME_EL_FOLDL) lemma ALL_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list. @@ -5096,11 +5096,11 @@ by (import rich_list ALL_EL_FOLDL_MAP) lemma SOME_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list. - list_exists x xa = foldr op | (map x xa) False" + list_ex x xa = foldr op | (map x xa) False" by (import rich_list SOME_EL_FOLDR_MAP) lemma SOME_EL_FOLDL_MAP: "ALL (x::'a::type => bool) xa::'a::type list. - list_exists x xa = foldl op | False (map x xa)" + list_ex x xa = foldl op | False (map x xa)" by (import rich_list SOME_EL_FOLDL_MAP) lemma FOLDR_FILTER: "ALL (f::'a::type => 'a::type => 'a::type) (e::'a::type) @@ -5132,12 +5132,12 @@ by (import rich_list ASSOC_FOLDL_FLAT) lemma SOME_EL_MAP: "ALL (P::'b::type => bool) (f::'a::type => 'b::type) l::'a::type list. - list_exists P (map f l) = list_exists (P o f) l" + list_ex P (map f l) = list_ex (P o f) l" by (import rich_list SOME_EL_MAP) lemma SOME_EL_DISJ: "ALL (P::'a::type => bool) (Q::'a::type => bool) l::'a::type list. - list_exists (%x::'a::type. P x | Q x) l = - (list_exists P l | list_exists Q l)" + list_ex (%x::'a::type. P x | Q x) l = + (list_ex P l | list_ex Q l)" by (import rich_list SOME_EL_DISJ) lemma IS_EL_FOLDR: "ALL (x::'a::type) xa::'a::type list. @@ -5579,7 +5579,7 @@ by (import rich_list FLAT_FLAT) lemma SOME_EL_REVERSE: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P (rev l) = list_exists P l" + list_ex P (rev l) = list_ex P l" by (import rich_list SOME_EL_REVERSE) lemma ALL_EL_SEG: "ALL (P::'a::type => bool) l::'a::type list. @@ -5621,29 +5621,29 @@ lemma SOME_EL_SEG: "ALL (m::nat) (k::nat) l::'a::type list. m + k <= length l --> - (ALL P::'a::type => bool. list_exists P (SEG m k l) --> list_exists P l)" + (ALL P::'a::type => bool. list_ex P (SEG m k l) --> list_ex P l)" by (import rich_list SOME_EL_SEG) lemma SOME_EL_FIRSTN: "ALL (m::nat) l::'a::type list. m <= length l --> - (ALL P::'a::type => bool. list_exists P (FIRSTN m l) --> list_exists P l)" + (ALL P::'a::type => bool. list_ex P (FIRSTN m l) --> list_ex P l)" by (import rich_list SOME_EL_FIRSTN) lemma SOME_EL_BUTFIRSTN: "ALL (m::nat) l::'a::type list. m <= length l --> (ALL P::'a::type => bool. - list_exists P (BUTFIRSTN m l) --> list_exists P l)" + list_ex P (BUTFIRSTN m l) --> list_ex P l)" by (import rich_list SOME_EL_BUTFIRSTN) lemma SOME_EL_LASTN: "ALL (m::nat) l::'a::type list. m <= length l --> - (ALL P::'a::type => bool. list_exists P (LASTN m l) --> list_exists P l)" + (ALL P::'a::type => bool. list_ex P (LASTN m l) --> list_ex P l)" by (import rich_list SOME_EL_LASTN) lemma SOME_EL_BUTLASTN: "ALL (m::nat) l::'a::type list. m <= length l --> (ALL P::'a::type => bool. - list_exists P (BUTLASTN m l) --> list_exists P l)" + list_ex P (BUTLASTN m l) --> list_ex P l)" by (import rich_list SOME_EL_BUTLASTN) lemma IS_EL_REVERSE: "ALL (x::'a::type) l::'a::type list. x mem rev l = x mem l" @@ -5657,7 +5657,7 @@ n + m <= length l --> (ALL x::'a::type. x mem SEG n m l --> x mem l)" by (import rich_list IS_EL_SEG) -lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l" +lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l" by (import rich_list IS_EL_SOME_EL) lemma IS_EL_FIRSTN: "ALL (x::nat) xa::'a::type list. diff -r df12f798df99 -r ff1137a9c056 src/HOL/Import/HOL/pair.imp --- a/src/HOL/Import/HOL/pair.imp Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Import/HOL/pair.imp Tue Jun 29 11:38:51 2010 +0200 @@ -10,8 +10,8 @@ "prod" > "Product_Type.*" const_maps - "pair_case" > "Product_Type.split" - "UNCURRY" > "Product_Type.split" + "pair_case" > "Product_Type.prod_case" + "UNCURRY" > "Product_Type.prod_case" "FST" > "Product_Type.fst" "SND" > "Product_Type.snd" "RPROD" > "HOL4Base.pair.RPROD" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Import/HOL4Compat.thy --- a/src/HOL/Import/HOL4Compat.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Import/HOL4Compat.thy Tue Jun 29 11:38:51 2010 +0200 @@ -6,6 +6,7 @@ imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum begin +abbreviation (input) mem (infixl "mem" 55) where "x mem xs \ List.member xs x" no_notation differentiable (infixl "differentiable" 60) no_notation sums (infixr "sums" 80) @@ -326,8 +327,8 @@ qed qed -lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)" - by simp +lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)" + by (simp add: null_def) definition sum :: "nat list \ nat" where "sum l == foldr (op +) l 0" @@ -347,8 +348,8 @@ lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)" by simp -lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))" - by auto +lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))" + by (simp add: member_def) lemma FILTER: "(!P. filter P [] = []) & (!P h t. filter P (h#t) = (if P h then h#filter P t else filter P t))" @@ -373,15 +374,7 @@ lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))" by simp -consts - list_exists :: "['a \ bool,'a list] \ bool" - -primrec - list_exists_Nil: "list_exists P Nil = False" - list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)" - -lemma list_exists_DEF: "(!P. list_exists P [] = False) & - (!P h t. list_exists P (h#t) = (P h | list_exists P t))" +lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))" by simp consts diff -r df12f798df99 -r ff1137a9c056 src/HOL/Induct/Term.thy --- a/src/HOL/Induct/Term.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Induct/Term.thy Tue Jun 29 11:38:51 2010 +0200 @@ -13,18 +13,12 @@ text {* \medskip Substitution function on terms *} -consts - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" - subst_term_list :: - "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" - -primrec +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" + and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where "subst_term f (Var a) = f a" - "subst_term f (App b ts) = App b (subst_term_list f ts)" - - "subst_term_list f [] = []" - "subst_term_list f (t # ts) = - subst_term f t # subst_term_list f ts" +| "subst_term f (App b ts) = App b (subst_term_list f ts)" +| "subst_term_list f [] = []" +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" text {* \medskip A simple theorem about composition of substitutions *} @@ -41,9 +35,9 @@ lemma assumes var: "!!v. P (Var v)" - and app: "!!f ts. list_all P ts ==> P (App f ts)" + and app: "!!f ts. (\t \ set ts. P t) ==> P (App f ts)" shows term_induct2: "P t" - and "list_all P ts" + and "\t \ set ts. P t" apply (induct t and ts) apply (rule var) apply (rule app) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Isar_Examples/Nested_Datatype.thy --- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 11:38:51 2010 +0200 @@ -10,17 +10,14 @@ Var 'a | App 'b "('a, 'b) term list" -consts - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" - subst_term_list :: - "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and + subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where + "subst_term f (Var a) = f a" +| "subst_term f (App b ts) = App b (subst_term_list f ts)" +| "subst_term_list f [] = []" +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" -primrec (subst) - "subst_term f (Var a) = f a" - "subst_term f (App b ts) = App b (subst_term_list f ts)" - "subst_term_list f [] = []" - "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" - +lemmas subst_simps = subst_term_subst_term_list.simps text {* \medskip A simple lemma about composition of substitutions. @@ -44,13 +41,13 @@ next fix b ts assume "?Q ts" then show "?P (App b ts)" - by (simp only: subst.simps) + by (simp only: subst_simps) next show "?Q []" by simp next fix t ts assume "?P t" "?Q ts" then show "?Q (t # ts)" - by (simp only: subst.simps) + by (simp only: subst_simps) qed qed @@ -59,18 +56,18 @@ theorem term_induct' [case_names Var App]: assumes var: "!!a. P (Var a)" - and app: "!!b ts. list_all P ts ==> P (App b ts)" + and app: "!!b ts. (\t \ set ts. P t) ==> P (App b ts)" shows "P t" proof (induct t) fix a show "P (Var a)" by (rule var) next - fix b t ts assume "list_all P ts" + fix b t ts assume "\t \ set ts. P t" then show "P (App b ts)" by (rule app) next - show "list_all P []" by simp + show "\t \ set []. P t" by simp next - fix t ts assume "P t" "list_all P ts" - then show "list_all P (t # ts)" by simp + fix t ts assume "P t" "\t' \ set ts. P t'" + then show "\t' \ set (t # ts). P t'" by simp qed lemma diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Tue Jun 29 11:38:51 2010 +0200 @@ -427,8 +427,7 @@ lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs" - by (simp add: merge_def updates_def split_prod_case - foldr_fold_rev zip_rev zip_map_fst_snd) + by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd) lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \ fst ` set ys" by (induct ys arbitrary: xs) (auto simp add: dom_update) @@ -449,7 +448,7 @@ More_List.fold (\(k, v) m. m(k \ v)) (rev ys) \ map_of" by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq) then show ?thesis - by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq) + by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq) qed corollary merge_conv: @@ -675,8 +674,8 @@ by (rule mapping_eqI) simp lemma is_empty_Mapping [code]: - "Mapping.is_empty (Mapping xs) \ null xs" - by (cases xs) (simp_all add: is_empty_def) + "Mapping.is_empty (Mapping xs) \ List.null xs" + by (cases xs) (simp_all add: is_empty_def null_def) lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (update k v xs)" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Dlist.thy Tue Jun 29 11:38:51 2010 +0200 @@ -122,7 +122,7 @@ next case (insert x xs) then have "\ member (Dlist xs) x" and "P (Dlist xs)" - by (simp_all add: member_def mem_iff) + by (simp_all add: member_def List.member_def) with insrt have "P (insert x (Dlist xs))" . with insert show ?case by (simp add: insert_def distinct_remdups_id) qed @@ -144,7 +144,7 @@ case (Cons x xs) with dxs distinct have "\ member (Dlist xs) x" and "dxs = insert x (Dlist xs)" - by (simp_all add: member_def mem_iff insert_def distinct_remdups_id) + by (simp_all add: member_def List.member_def insert_def distinct_remdups_id) with insert show P . qed qed @@ -205,7 +205,7 @@ lemma is_empty_Set [code]: "Fset.is_empty (Set dxs) \ null dxs" - by (simp add: null_def null_empty member_set) + by (simp add: null_def List.null_def member_set) lemma bot_code [code]: "bot = Set empty" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Enum.thy Tue Jun 29 11:38:51 2010 +0200 @@ -49,8 +49,8 @@ lemma order_fun [code]: fixes f g :: "'a\enum \ 'b\order" shows "f \ g \ list_all (\x. f x \ g x) enum" - and "f < g \ f \ g \ \ list_all (\x. f x = g x) enum" - by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le) + and "f < g \ f \ g \ list_ex (\x. f x \ g x) enum" + by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le) subsection {* Quantifiers *} @@ -58,8 +58,8 @@ lemma all_code [code]: "(\x. P x) \ list_all P enum" by (simp add: list_all_iff enum_all) -lemma exists_code [code]: "(\x. P x) \ \ list_all (Not o P) enum" - by (simp add: list_all_iff enum_all) +lemma exists_code [code]: "(\x. P x) \ list_ex P enum" + by (simp add: list_ex_iff enum_all) subsection {* Default instances *} diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Executable_Set.thy Tue Jun 29 11:38:51 2010 +0200 @@ -50,9 +50,9 @@ by simp lemma [code]: - "x \ Set xs \ member xs x" - "x \ Coset xs \ \ member xs x" - by (simp_all add: mem_iff) + "x \ Set xs \ List.member xs x" + "x \ Coset xs \ \ List.member xs x" + by (simp_all add: member_def) definition is_empty :: "'a set \ bool" where [simp]: "is_empty A \ A = {}" @@ -85,8 +85,8 @@ *} lemma is_empty_Set [code]: - "is_empty (Set xs) \ null xs" - by (simp add: empty_null) + "is_empty (Set xs) \ List.null xs" + by (simp add: null_def) lemma empty_Set [code]: "empty = Set []" @@ -112,11 +112,11 @@ lemma Ball_Set [code]: "Ball (Set xs) P \ list_all P xs" - by (simp add: ball_set) + by (simp add: list_all_iff) lemma Bex_Set [code]: "Bex (Set xs) P \ list_ex P xs" - by (simp add: bex_set) + by (simp add: list_ex_iff) lemma card_Set [code]: "card (Set xs) = length (remdups xs)" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Fset.thy Tue Jun 29 11:38:51 2010 +0200 @@ -51,7 +51,7 @@ lemma member_code [code]: "member (Set xs) = List.member xs" "member (Coset xs) = Not \ List.member xs" - by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def) + by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def) lemma member_image_UNIV [simp]: "member ` UNIV = UNIV" @@ -141,7 +141,7 @@ [simp]: "is_empty A \ More_Set.is_empty (member A)" lemma is_empty_Set [code]: - "is_empty (Set xs) \ null xs" + "is_empty (Set xs) \ List.null xs" by (simp add: is_empty_set) lemma empty_Set [code]: @@ -188,14 +188,14 @@ lemma forall_Set [code]: "forall P (Set xs) \ list_all P xs" - by (simp add: Set_def ball_set) + by (simp add: Set_def list_all_iff) definition exists :: "('a \ bool) \ 'a fset \ bool" where [simp]: "exists P A \ Bex (member A) P" lemma exists_Set [code]: "exists P (Set xs) \ list_ex P xs" - by (simp add: Set_def bex_set) + by (simp add: Set_def list_ex_iff) definition card :: "'a fset \ nat" where [simp]: "card A = Finite_Set.card (member A)" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/More_Set.thy --- a/src/HOL/Library/More_Set.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/More_Set.thy Tue Jun 29 11:38:51 2010 +0200 @@ -37,16 +37,8 @@ subsection {* Basic set operations *} lemma is_empty_set: - "is_empty (set xs) \ null xs" - by (simp add: is_empty_def null_empty) - -lemma ball_set: - "(\x\set xs. P x) \ list_all P xs" - by (rule list_ball_code) - -lemma bex_set: - "(\x\set xs. P x) \ list_ex P xs" - by (rule list_bex_code) + "is_empty (set xs) \ List.null xs" + by (simp add: is_empty_def null_def) lemma empty_set: "{} = set []" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Nat_Bijection.thy --- a/src/HOL/Library/Nat_Bijection.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Nat_Bijection.thy Tue Jun 29 11:38:51 2010 +0200 @@ -213,6 +213,7 @@ termination list_decode apply (relation "measure id", simp_all) apply (drule arg_cong [where f="prod_encode"]) +apply (drule sym) apply (simp add: le_imp_less_Suc le_prod_encode_2) done diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Jun 29 11:38:51 2010 +0200 @@ -18,7 +18,7 @@ section {* Pairs *} -setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *} +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *} section {* Bounded quantifiers *} diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Tue Jun 29 11:38:51 2010 +0200 @@ -1076,7 +1076,7 @@ from this Empty_is_rbt have "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs" by (simp add: `ys = rev xs`) - then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split) + then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev) qed hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Transitive_Closure_Table.thy --- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Jun 29 11:38:51 2010 +0200 @@ -189,7 +189,7 @@ declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] -code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp +code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastsimp subsection {* A simple example *} diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/Univ_Poly.thy --- a/src/HOL/Library/Univ_Poly.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/Univ_Poly.thy Tue Jun 29 11:38:51 2010 +0200 @@ -407,7 +407,7 @@ lemma (in idom) poly_exp_eq_zero[simp]: "(poly (p %^ n) = poly []) = (poly p = poly [] & n \ 0)" -apply (simp only: fun_eq add: all_simps [symmetric]) +apply (simp only: fun_eq add: HOL.all_simps [symmetric]) apply (rule arg_cong [where f = All]) apply (rule ext) apply (induct n) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Tue Jun 29 11:38:51 2010 +0200 @@ -228,7 +228,7 @@ val prenex_simps = map (fn th => th RS sym) ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @ - @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)}); + @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)}); val real_abs_thms1 = @{lemma "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and diff -r df12f798df99 -r ff1137a9c056 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/List.thy Tue Jun 29 11:38:51 2010 +0200 @@ -2352,6 +2352,22 @@ case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) qed +lemma rev_foldl_cons [code]: + "rev xs = foldl (\xs x. x # xs) [] xs" +proof (induct xs) + case Nil then show ?case by simp +next + case Cons + { + fix x xs ys + have "foldl (\xs x. x # xs) ys xs @ [x] + = foldl (\xs x. x # xs) (ys @ [x]) xs" + by (induct xs arbitrary: ys) auto + } + note aux = this + show ?case by (induct xs) (auto simp add: Cons aux) +qed + text{* The ``First Duality Theorem'' in Bird \& Wadler: *} @@ -2509,120 +2525,6 @@ by (simp add: sup_commute) -subsubsection {* List summation: @{const listsum} and @{text"\"}*} - -lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" -by (induct xs) (simp_all add:add_assoc) - -lemma listsum_rev [simp]: - fixes xs :: "'a\comm_monoid_add list" - shows "listsum (rev xs) = listsum xs" -by (induct xs) (simp_all add:add_ac) - -lemma listsum_map_remove1: -fixes f :: "'a \ ('b::comm_monoid_add)" -shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))" -by (induct xs)(auto simp add:add_ac) - -lemma list_size_conv_listsum: - "list_size f xs = listsum (map f xs) + size xs" -by(induct xs) auto - -lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" -by (induct xs) auto - -lemma length_concat: "length (concat xss) = listsum (map length xss)" -by (induct xss) simp_all - -lemma listsum_map_filter: - fixes f :: "'a \ 'b \ comm_monoid_add" - assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" - shows "listsum (map f (filter P xs)) = listsum (map f xs)" -using assms by (induct xs) auto - -text{* For efficient code generation --- - @{const listsum} is not tail recursive but @{const foldl} is. *} -lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" -by(simp add:listsum_foldr foldl_foldr1) - -lemma distinct_listsum_conv_Setsum: - "distinct xs \ listsum xs = Setsum(set xs)" -by (induct xs) simp_all - -lemma listsum_eq_0_nat_iff_nat[simp]: - "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" -by(simp add: listsum) - -lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" -apply(induct ns arbitrary: k) - apply simp -apply(fastsimp simp add:nth_Cons split: nat.split) -done - -lemma listsum_update_nat: "k - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" -apply(induct ns arbitrary:k) - apply (auto split:nat.split) -apply(drule elem_le_listsum_nat) -apply arith -done - -text{* Some syntactic sugar for summing a function over a list: *} - -syntax - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) -syntax (xsymbols) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) -syntax (HTML output) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) - -translations -- {* Beware of argument permutation! *} - "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" - "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" - -lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" - by (induct xs) (simp_all add: left_distrib) - -lemma listsum_0 [simp]: "(\x\xs. 0) = 0" - by (induct xs) (simp_all add: left_distrib) - -text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} -lemma uminus_listsum_map: - fixes f :: "'a \ 'b\ab_group_add" - shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" -by (induct xs) simp_all - -lemma listsum_addf: - fixes f g :: "'a \ 'b::comm_monoid_add" - shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" -by (induct xs) (simp_all add: algebra_simps) - -lemma listsum_subtractf: - fixes f g :: "'a \ 'b::ab_group_add" - shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" -by (induct xs) simp_all - -lemma listsum_const_mult: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. c * f x) = c * (\x\xs. f x)" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_mult_const: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. f x * c) = (\x\xs. f x) * c" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_abs: - fixes xs :: "'a::ordered_ab_group_add_abs list" - shows "\listsum xs\ \ listsum (map abs xs)" -by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) - -lemma listsum_mono: - fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" - shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" -by (induct xs, simp, simp add: add_mono) - - subsubsection {* @{text upt} *} lemma upt_rec[code]: "[i.."}*} + +lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" +by (induct xs) (simp_all add:add_assoc) + +lemma listsum_rev [simp]: + fixes xs :: "'a\comm_monoid_add list" + shows "listsum (rev xs) = listsum xs" +by (induct xs) (simp_all add:add_ac) + +lemma listsum_map_remove1: +fixes f :: "'a \ ('b::comm_monoid_add)" +shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))" +by (induct xs)(auto simp add:add_ac) + +lemma list_size_conv_listsum: + "list_size f xs = listsum (map f xs) + size xs" +by(induct xs) auto + +lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" +by (induct xs) auto + +lemma length_concat: "length (concat xss) = listsum (map length xss)" +by (induct xss) simp_all + +lemma listsum_map_filter: + fixes f :: "'a \ 'b \ comm_monoid_add" + assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" + shows "listsum (map f (filter P xs)) = listsum (map f xs)" +using assms by (induct xs) auto + +text{* For efficient code generation --- + @{const listsum} is not tail recursive but @{const foldl} is. *} +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" +by(simp add:listsum_foldr foldl_foldr1) + +lemma distinct_listsum_conv_Setsum: + "distinct xs \ listsum xs = Setsum(set xs)" +by (induct xs) simp_all + +lemma listsum_eq_0_nat_iff_nat[simp]: + "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" +by(simp add: listsum) + +lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" +apply(induct ns arbitrary: k) + apply simp +apply(fastsimp simp add:nth_Cons split: nat.split) +done + +lemma listsum_update_nat: "k + listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" +apply(induct ns arbitrary:k) + apply (auto split:nat.split) +apply(drule elem_le_listsum_nat) +apply arith +done + +text{* Some syntactic sugar for summing a function over a list: *} + +syntax + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) +syntax (xsymbols) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) +syntax (HTML output) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) + +translations -- {* Beware of argument permutation! *} + "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" + "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" + +lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" + by (induct xs) (simp_all add: left_distrib) + +lemma listsum_0 [simp]: "(\x\xs. 0) = 0" + by (induct xs) (simp_all add: left_distrib) + +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} +lemma uminus_listsum_map: + fixes f :: "'a \ 'b\ab_group_add" + shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" +by (induct xs) simp_all + +lemma listsum_addf: + fixes f g :: "'a \ 'b::comm_monoid_add" + shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" +by (induct xs) (simp_all add: algebra_simps) + +lemma listsum_subtractf: + fixes f g :: "'a \ 'b::ab_group_add" + shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" +by (induct xs) simp_all + +lemma listsum_const_mult: + fixes f :: "'a \ 'b::semiring_0" + shows "(\x\xs. c * f x) = c * (\x\xs. f x)" +by (induct xs, simp_all add: algebra_simps) + +lemma listsum_mult_const: + fixes f :: "'a \ 'b::semiring_0" + shows "(\x\xs. f x * c) = (\x\xs. f x) * c" +by (induct xs, simp_all add: algebra_simps) + +lemma listsum_abs: + fixes xs :: "'a::ordered_ab_group_add_abs list" + shows "\listsum xs\ \ listsum (map abs xs)" +by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) + +lemma listsum_mono: + fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" + shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" +by (induct xs, simp, simp add: add_mono) + +lemma listsum_distinct_conv_setsum_set: + "distinct xs \ listsum (map f xs) = setsum f (set xs)" + by (induct xs) simp_all + +lemma interv_listsum_conv_setsum_set_nat: + "listsum (map f [m.. i = 0 ..< length xs. xs ! i)" + using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) + + subsubsection {* @{const insert} *} lemma in_set_insert [simp]: @@ -4513,9 +4546,266 @@ *) -subsection {* Code generator *} - -subsubsection {* Setup *} +subsection {* Code generation *} + +subsubsection {* Counterparts for set-related operations *} + +definition member :: "'a list \ 'a \ bool" where + [code_post]: "member xs x \ x \ set xs" + +text {* + Only use @{text member} for generating executable code. Otherwise use + @{prop "x \ set xs"} instead --- it is much easier to reason about. +*} + +lemma member_set: + "member = set" + by (simp add: expand_fun_eq member_def mem_def) + +lemma member_rec [code]: + "member (x # xs) y \ x = y \ member xs y" + "member [] y \ False" + by (auto simp add: member_def) + +lemma in_set_member [code_unfold]: + "x \ set xs \ member xs x" + by (simp add: member_def) + +declare INFI_def [code_unfold] +declare SUPR_def [code_unfold] + +declare set_map [symmetric, code_unfold] + +definition list_all :: "('a \ bool) \ 'a list \ bool" where + list_all_iff [code_post]: "list_all P xs \ (\x \ set xs. P x)" + +definition list_ex :: "('a \ bool) \ 'a list \ bool" where + list_ex_iff [code_post]: "list_ex P xs \ (\x \ set xs. P x)" + +text {* + Usually you should prefer @{text "\x\set xs"} and @{text "\x\set xs"} + over @{const list_all} and @{const list_ex} in specifications. +*} + +lemma list_all_simps [simp, code]: + "list_all P (x # xs) \ P x \ list_all P xs" + "list_all P [] \ True" + by (simp_all add: list_all_iff) + +lemma list_ex_simps [simp, code]: + "list_ex P (x # xs) \ P x \ list_ex P xs" + "list_ex P [] \ False" + by (simp_all add: list_ex_iff) + +lemma Ball_set_list_all [code_unfold]: + "Ball (set xs) P \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set_list_ex [code_unfold]: + "Bex (set xs) P \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma list_all_append [simp]: + "list_all P (xs @ ys) \ list_all P xs \ list_all P ys" + by (auto simp add: list_all_iff) + +lemma list_ex_append [simp]: + "list_ex P (xs @ ys) \ list_ex P xs \ list_ex P ys" + by (auto simp add: list_ex_iff) + +lemma list_all_rev [simp]: + "list_all P (rev xs) \ list_all P xs" + by (simp add: list_all_iff) + +lemma list_ex_rev [simp]: + "list_ex P (rev xs) \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma list_all_length: + "list_all P xs \ (\n < length xs. P (xs ! n))" + by (auto simp add: list_all_iff set_conv_nth) + +lemma list_ex_length: + "list_ex P xs \ (\n < length xs. P (xs ! n))" + by (auto simp add: list_ex_iff set_conv_nth) + +lemma list_all_cong [fundef_cong]: + "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_all f xs = list_all g ys" + by (simp add: list_all_iff) + +lemma list_any_cong [fundef_cong]: + "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_ex f xs = list_ex g ys" + by (simp add: list_ex_iff) + +text {* Bounded quantification and summation over nats. *} + +lemma atMost_upto [code_unfold]: + "{..n} = set [0..mnat. P m) \ (\m \ {0..mnat. P m) \ (\m \ {0..m\n\nat. P m) \ (\m \ {0..n}. P m)" + by auto + +lemma ex_nat_less [code_unfold]: + "(\m\n\nat. P m) \ (\m \ {0..n}. P m)" + by auto + +lemma setsum_set_upt_conv_listsum_nat [code_unfold]: + "setsum f (set [m.. bool" where + [code_post]: "null xs \ xs = []" + +text {* + Efficient emptyness check is implemented by @{const null}. +*} + +lemma null_rec [code]: + "null (x # xs) \ False" + "null [] \ True" + by (simp_all add: null_def) + +lemma eq_Nil_null [code_unfold]: + "xs = [] \ null xs" + by (simp add: null_def) + +lemma equal_Nil_null [code_unfold]: + "eq_class.eq xs [] \ null xs" + by (simp add: eq eq_Nil_null) + +definition maps :: "('a \ 'b list) \ 'a list \ 'b list" where + [code_post]: "maps f xs = concat (map f xs)" + +definition map_filter :: "('a \ 'b option) \ 'a list \ 'b list" where + [code_post]: "map_filter f xs = map (the \ f) (filter (\x. f x \ None) xs)" + +text {* + Operations @{const maps} and @{const map_filter} avoid + intermediate lists on execution -- do not use for proving. +*} + +lemma maps_simps [code]: + "maps f (x # xs) = f x @ maps f xs" + "maps f [] = []" + by (simp_all add: maps_def) + +lemma map_filter_simps [code]: + "map_filter f (x # xs) = (case f x of None \ map_filter f xs | Some y \ y # map_filter f xs)" + "map_filter f [] = []" + by (simp_all add: map_filter_def split: option.split) + +lemma concat_map_maps [code_unfold]: + "concat (map f xs) = maps f xs" + by (simp add: maps_def) + +lemma map_filter_map_filter [code_unfold]: + "map f (filter P xs) = map_filter (\x. if P x then Some (f x) else None) xs" + by (simp add: map_filter_def) + +text {* Optimized code for @{text"\i\{a..b::int}"} and @{text"\n:{a.."}. *} + +definition all_interval_nat :: "(nat \ bool) \ nat \ nat \ bool" where + "all_interval_nat P i j \ (\n \ {i.. i \ j \ P i \ all_interval_nat P (Suc i) j" +proof - + have *: "\n. P i \ \n\{Suc i.. i \ n \ n < j \ P n" + proof - + fix n + assume "P i" "\n\{Suc i.. n" "n < j" + then show "P n" by (cases "n = i") simp_all + qed + show ?thesis by (auto simp add: all_interval_nat_def intro: *) +qed + +lemma list_all_iff_all_interval_nat [code_unfold]: + "list_all P [i.. all_interval_nat P i j" + by (simp add: list_all_iff all_interval_nat_def) + +lemma list_ex_iff_not_all_inverval_nat [code_unfold]: + "list_ex P [i.. \ (all_interval_nat (Not \ P) i j)" + by (simp add: list_ex_iff all_interval_nat_def) + +definition all_interval_int :: "(int \ bool) \ int \ int \ bool" where + "all_interval_int P i j \ (\k \ {i..j}. P k)" + +lemma [code]: + "all_interval_int P i j \ i > j \ P i \ all_interval_int P (i + 1) j" +proof - + have *: "\k. P i \ \k\{i+1..j}. P k \ i \ k \ k \ j \ P k" + proof - + fix k + assume "P i" "\k\{i+1..j}. P k" "i \ k" "k \ j" + then show "P k" by (cases "k = i") simp_all + qed + show ?thesis by (auto simp add: all_interval_int_def intro: *) +qed + +lemma list_all_iff_all_interval_int [code_unfold]: + "list_all P [i..j] \ all_interval_int P i j" + by (simp add: list_all_iff all_interval_int_def) + +lemma list_ex_iff_not_all_inverval_int [code_unfold]: + "list_ex P [i..j] \ \ (all_interval_int (Not \ P) i j)" + by (simp add: list_ex_iff all_interval_int_def) + +hide_const (open) member null maps map_filter all_interval_nat all_interval_int + + +subsubsection {* Pretty lists *} use "Tools/list_code.ML" @@ -4578,374 +4868,6 @@ *} -subsubsection {* Generation of efficient code *} - -definition member :: "'a list \ 'a \ bool" where - mem_iff [code_post]: "member xs x \ x \ set xs" - -primrec - null:: "'a list \ bool" -where - "null [] = True" - | "null (x#xs) = False" - -primrec - list_inter :: "'a list \ 'a list \ 'a list" -where - "list_inter [] bs = []" - | "list_inter (a#as) bs = - (if a \ set bs then a # list_inter as bs else list_inter as bs)" - -primrec - list_all :: "('a \ bool) \ ('a list \ bool)" -where - "list_all P [] = True" - | "list_all P (x#xs) = (P x \ list_all P xs)" - -primrec - list_ex :: "('a \ bool) \ 'a list \ bool" -where - "list_ex P [] = False" - | "list_ex P (x#xs) = (P x \ list_ex P xs)" - -primrec - filtermap :: "('a \ 'b option) \ 'a list \ 'b list" -where - "filtermap f [] = []" - | "filtermap f (x#xs) = - (case f x of None \ filtermap f xs - | Some y \ y # filtermap f xs)" - -primrec - map_filter :: "('a \ 'b) \ ('a \ bool) \ 'a list \ 'b list" -where - "map_filter f P [] = []" - | "map_filter f P (x#xs) = - (if P x then f x # map_filter f P xs else map_filter f P xs)" - -primrec - length_unique :: "'a list \ nat" -where - "length_unique [] = 0" - | "length_unique (x#xs) = - (if x \ set xs then length_unique xs else Suc (length_unique xs))" - -primrec - concat_map :: "('a => 'b list) => 'a list => 'b list" -where - "concat_map f [] = []" - | "concat_map f (x#xs) = f x @ concat_map f xs" - -text {* - Only use @{text member} for generating executable code. Otherwise use - @{prop "x : set xs"} instead --- it is much easier to reason about. - The same is true for @{const list_all} and @{const list_ex}: write - @{text "\x\set xs"} and @{text "\x\set xs"} instead because the HOL - quantifiers are aleady known to the automatic provers. In fact, the - declarations in the code subsection make sure that @{text "\"}, - @{text "\x\set xs"} and @{text "\x\set xs"} are implemented - efficiently. - - Efficient emptyness check is implemented by @{const null}. - - The functions @{const filtermap} and @{const map_filter} are just - there to generate efficient code. Do not use - them for modelling and proving. -*} - -lemma rev_foldl_cons [code]: - "rev xs = foldl (\xs x. x # xs) [] xs" -proof (induct xs) - case Nil then show ?case by simp -next - case Cons - { - fix x xs ys - have "foldl (\xs x. x # xs) ys xs @ [x] - = foldl (\xs x. x # xs) (ys @ [x]) xs" - by (induct xs arbitrary: ys) auto - } - note aux = this - show ?case by (induct xs) (auto simp add: Cons aux) -qed - -lemmas in_set_code [code_unfold] = mem_iff [symmetric] - -lemma member_simps [simp, code]: - "member (x # xs) y \ x = y \ member xs y" - "member [] y \ False" - by (auto simp add: mem_iff) - -lemma member_set: - "member = set" - by (simp add: expand_fun_eq mem_iff mem_def) - -abbreviation (input) mem :: "'a \ 'a list \ bool" (infixl "mem" 55) where - "x mem xs \ member xs x" -- "for backward compatibility" - -lemma empty_null: - "xs = [] \ null xs" -by (cases xs) simp_all - -lemma [code_unfold]: - "eq_class.eq xs [] \ null xs" -by (simp add: eq empty_null) - -lemmas null_empty [code_post] = - empty_null [symmetric] - -lemma list_inter_conv: - "set (list_inter xs ys) = set xs \ set ys" -by (induct xs) auto - -lemma list_all_iff [code_post]: - "list_all P xs \ (\x \ set xs. P x)" -by (induct xs) auto - -lemmas list_ball_code [code_unfold] = list_all_iff [symmetric] - -lemma list_all_append [simp]: - "list_all P (xs @ ys) \ (list_all P xs \ list_all P ys)" -by (induct xs) auto - -lemma list_all_rev [simp]: - "list_all P (rev xs) \ list_all P xs" -by (simp add: list_all_iff) - -lemma list_all_length: - "list_all P xs \ (\n < length xs. P (xs ! n))" -unfolding list_all_iff by (auto intro: all_nth_imp_all_set) - -lemma list_all_cong[fundef_cong]: - "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_all f xs = list_all g ys" -by (simp add: list_all_iff) - -lemma list_ex_iff [code_post]: - "list_ex P xs \ (\x \ set xs. P x)" -by (induct xs) simp_all - -lemmas list_bex_code [code_unfold] = - list_ex_iff [symmetric] - -lemma list_ex_length: - "list_ex P xs \ (\n < length xs. P (xs ! n))" -unfolding list_ex_iff set_conv_nth by auto - -lemma list_ex_cong[fundef_cong]: - "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_ex f xs = list_ex g ys" -by (simp add: list_ex_iff) - -lemma filtermap_conv: - "filtermap f xs = map (\x. the (f x)) (filter (\x. f x \ None) xs)" -by (induct xs) (simp_all split: option.split) - -lemma map_filter_conv [simp]: - "map_filter f P xs = map f (filter P xs)" -by (induct xs) auto - -lemma length_remdups_length_unique [code_unfold]: - "length (remdups xs) = length_unique xs" -by (induct xs) simp_all - -lemma concat_map_code[code_unfold]: - "concat(map f xs) = concat_map f xs" -by (induct xs) simp_all - -declare INFI_def [code_unfold] -declare SUPR_def [code_unfold] - -declare set_map [symmetric, code_unfold] - -hide_const (open) length_unique - - -text {* Code for bounded quantification and summation over nats. *} - -lemma atMost_upto [code_unfold]: - "{..n} = set [0..mnat. P m) \ (\m \ {0..mnat. P m) \ (\m \ {0..m\n\nat. P m) \ (\m \ {0..n}. P m)" -by auto - -lemma ex_nat_less [code_unfold]: - "(\m\n\nat. P m) \ (\m \ {0..n}. P m)" -by auto - -lemma setsum_set_distinct_conv_listsum: - "distinct xs \ setsum f (set xs) = listsum (map f xs)" -by (induct xs) simp_all - -lemma setsum_set_upt_conv_listsum [code_unfold]: - "setsum f (set [m.. i = 0 ..< length xs. xs ! i)" -using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"] -by (simp add: map_nth) - -text {* Code for summation over ints. *} - -lemma greaterThanLessThan_upto [code_unfold]: - "{i<..i\{a..b::int}"} and @{text"\n:{a.."}. *} - -function all_from_to_nat :: "(nat \ bool) \ nat \ nat \ bool" where -"all_from_to_nat P i j = - (if i < j then if P i then all_from_to_nat P (i+1) j else False - else True)" -by auto -termination -by (relation "measure(%(P,i,j). j - i)") auto - -declare all_from_to_nat.simps[simp del] - -lemma all_from_to_nat_iff_ball: - "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)" -proof(induct P i j rule:all_from_to_nat.induct) - case (1 P i j) - let ?yes = "i < j & P i" - show ?case - proof (cases) - assume ?yes - hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)" - by(simp add: all_from_to_nat.simps) - also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp - also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R") - proof - assume L: ?L - show ?R - proof clarify - fix n assume n: "n : {i.. bool) \ int \ int \ bool" where -"all_from_to_int P i j = - (if i <= j then if P i then all_from_to_int P (i+1) j else False - else True)" -by auto -termination -by (relation "measure(%(P,i,j). nat(j - i + 1))") auto - -declare all_from_to_int.simps[simp del] - -lemma all_from_to_int_iff_ball: - "all_from_to_int P i j = (ALL n : {i .. j}. P n)" -proof(induct P i j rule:all_from_to_int.induct) - case (1 P i j) - let ?yes = "i <= j & P i" - show ?case - proof (cases) - assume ?yes - hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)" - by(simp add: all_from_to_int.simps) - also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp - also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R") - proof - assume L: ?L - show ?R - proof clarify - fix n assume n: "n : {i..j}" - show "P n" - proof cases - assume "n = i" thus "P n" using L by simp - next - assume "n ~= i" - hence "i+1 <= n" using n by auto - thus "P n" using L n by simp - qed - qed - next - assume R: ?R thus ?L using `?yes` 1 by auto - qed - finally show ?thesis . - next - assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps) - qed -qed - -lemma list_all_iff_all_from_to_int[code_unfold]: - "list_all P [i..j] = all_from_to_int P i j" -by(simp add: all_from_to_int_iff_ball list_all_iff) - -lemma list_ex_iff_not_all_from_to_not_int[code_unfold]: - "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)" -by(simp add: all_from_to_int_iff_ball list_ex_iff) - - subsubsection {* Use convenient predefined operations *} code_const "op @" @@ -4963,12 +4885,18 @@ code_const concat (Haskell "concat") +code_const List.maps + (Haskell "concatMap") + code_const rev (Haskell "reverse") code_const zip (Haskell "zip") +code_const List.null + (Haskell "null") + code_const takeWhile (Haskell "takeWhile") @@ -4981,4 +4909,10 @@ code_const last (Haskell "last") +code_const list_all + (Haskell "all") + +code_const list_ex + (Haskell "any") + end diff -r df12f798df99 -r ff1137a9c056 src/HOL/MicroJava/DFA/LBVComplete.thy --- a/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Jun 29 11:38:51 2010 +0200 @@ -10,17 +10,17 @@ begin definition is_target :: "['s step_type, 's list, nat] \ bool" where - "is_target step phi pc' \ - \pc s'. pc' \ pc+1 \ pc < length phi \ (pc',s') \ set (step pc (phi!pc))" + "is_target step phi pc' \ + (\pc s'. pc' \ pc+1 \ pc < length phi \ (pc',s') \ set (step pc (phi!pc)))" definition make_cert :: "['s step_type, 's list, 's] \ 's certificate" where - "make_cert step phi B \ + "make_cert step phi B = map (\pc. if is_target step phi pc then phi!pc else B) [0..pc. pc' \ pc+1 \ pc' mem (map fst (step pc (phi!pc)))) [0..pc. pc' \ pc+1 \ List.member (map fst (step pc (phi!pc))) pc') [0.. = (f b - f a) \ (f b - f a)" unfolding power2_norm_eq_inner .. - also have "\ = (f b - f a) \ f' x (b - a)" using x unfolding inner_simps by auto + also have "\ = (f b - f a) \ f' x (b - a)" using x unfolding inner_simps by (auto simp add: inner_diff_left) also have "\ \ norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz) finally show ?thesis using False x(1) by(auto simp add: real_mult_left_cancel) next case True thus ?thesis using assms(1) apply(rule_tac x="(a + b) /2" in bexI) by auto qed qed diff -r df12f798df99 -r ff1137a9c056 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jun 29 11:38:51 2010 +0200 @@ -15,7 +15,7 @@ lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" by auto -abbreviation inner_bullet (infix "\" 70) where "x \ y \ inner x y" +notation inner (infix "\" 70) subsection {* A connectedness or intermediate value lemma with several applications. *} @@ -466,8 +466,8 @@ "orthogonal x a \ orthogonal (-x) a" "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a" "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a" - unfolding orthogonal_def inner_simps by auto - + unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto + end lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" diff -r df12f798df99 -r ff1137a9c056 src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Tue Jun 29 11:38:51 2010 +0200 @@ -133,7 +133,7 @@ apply (clarify intro!: Impl_nvalid_0) apply (clarify intro!: Impl_nvalid_Suc) apply (drule nvalids_SucD) -apply (simp only: all_simps) +apply (simp only: HOL.all_simps) apply (erule (1) impE) apply (drule (2) Impl_sound_lemma) apply blast diff -r df12f798df99 -r ff1137a9c056 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 29 11:38:51 2010 +0200 @@ -17,11 +17,11 @@ subsection {* Curry in a Hurry *} lemma "(\f x y. (curry o split) f x y) = (\f x y. (\x. x) f x y)" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = unknown (*none*)] by auto lemma "(\f p. (split o curry) f p) = (\f p. (\x. x) f p)" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = unknown (*none*)] by auto lemma "split (curry f) = f" @@ -61,12 +61,12 @@ by auto lemma "split o curry = (\x. x)" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = unknown (*none*)] apply (rule ext)+ by auto lemma "curry o split = (\x. x)" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = unknown (*none*)] apply (rule ext)+ by auto diff -r df12f798df99 -r ff1137a9c056 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Number_Theory/Primes.thy Tue Jun 29 11:38:51 2010 +0200 @@ -208,22 +208,20 @@ lemma one_not_prime_int [simp]: "~prime (1::int)" by (simp add: prime_int_def) -lemma prime_nat_code[code]: - "prime(p::nat) = (p > 1 & (ALL n : {1<.. p > 1 \ (\n \ {1<.. 1 & (list_all (%n. ~ n dvd p) [2.. p > 1 \ (\n \ set [2.. n dvd p)" +by (auto simp add: prime_nat_code) -lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard] +lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard] -lemma prime_int_code[code]: - "prime(p::int) = (p > 1 & (ALL n : {1<.. p > 1 \ (\n \ {1<.. 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))" -apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto) -apply simp -done + "prime (p::int) \ p > 1 \ (\n \ set [2..p - 1]. ~ n dvd p)" +by (auto simp add: prime_int_code) -lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard] +lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard] lemma two_is_prime_nat [simp]: "prime (2::nat)" by simp diff -r df12f798df99 -r ff1137a9c056 src/HOL/Old_Number_Theory/Pocklington.thy --- a/src/HOL/Old_Number_Theory/Pocklington.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Tue Jun 29 11:38:51 2010 +0200 @@ -1174,7 +1174,8 @@ ultimately show ?case using prime_divprod[OF p] by blast qed -lemma primefact_variant: "primefact ps n \ foldr op * ps 1 = n \ list_all prime ps" by (auto simp add: primefact_def list_all_iff) +lemma primefact_variant: "primefact ps n \ foldr op * ps 1 = n \ list_all prime ps" + by (auto simp add: primefact_def list_all_iff) (* Variant of Lucas theorem. *) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Probability/Borel.thy Tue Jun 29 11:38:51 2010 +0200 @@ -203,7 +203,7 @@ by (metis surj_def) from Fract i j n show ?thesis - by (metis prod.cases prod_case_split) + by (metis prod.cases) qed qed diff -r df12f798df99 -r ff1137a9c056 src/HOL/Probability/Caratheodory.thy --- a/src/HOL/Probability/Caratheodory.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Probability/Caratheodory.thy Tue Jun 29 11:38:51 2010 +0200 @@ -829,7 +829,7 @@ with sbBB [of i] obtain j where "x \ BB i j" by blast thus "\i. x \ split BB (prod_decode i)" - by (metis prod_encode_inverse prod.cases prod_case_split) + by (metis prod_encode_inverse prod.cases) qed have "(f \ C) = (f \ (\(x, y). BB x y)) \ prod_decode" by (rule ext) (auto simp add: C_def) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Product_Type.thy Tue Jun 29 11:38:51 2010 +0200 @@ -163,8 +163,8 @@ subsubsection {* Tuple syntax *} -definition split :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" where - split_prod_case: "split == prod_case" +abbreviation (input) split :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" where + "split \ prod_case" text {* Patterns -- extends pre-defined type @{typ pttrn} used in @@ -185,8 +185,8 @@ translations "(x, y)" == "CONST Pair x y" "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" - "%(x, y, zs). b" == "CONST split (%x (y, zs). b)" - "%(x, y). b" == "CONST split (%x y. b)" + "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)" + "%(x, y). b" == "CONST prod_case (%x y. b)" "_abs (CONST Pair x y) t" => "%(x, y). t" -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...' The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *} @@ -204,7 +204,7 @@ Syntax.const @{syntax_const "_abs"} $ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' end - | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] = + | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] = (* split (%x. (split (%y z. t))) => %(x,y,z). t *) let val Const (@{syntax_const "_abs"}, _) $ @@ -215,7 +215,7 @@ (Syntax.const @{syntax_const "_pattern"} $ x' $ (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t'' end - | split_tr' [Const (@{const_syntax split}, _) $ t] = + | split_tr' [Const (@{const_syntax prod_case}, _) $ t] = (* split (split (%x y z. t)) => %((x, y), z). t *) split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *) | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] = @@ -225,7 +225,7 @@ (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t end | split_tr' _ = raise Match; -in [(@{const_syntax split}, split_tr')] end +in [(@{const_syntax prod_case}, split_tr')] end *} (* print "split f" as "\(x,y). f x y" and "split (\x. f x)" as "\(x,y). f x y" *) @@ -234,7 +234,7 @@ fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match | split_guess_names_tr' _ T [Abs (x, xT, t)] = (case (head_of t) of - Const (@{const_syntax split}, _) => raise Match + Const (@{const_syntax prod_case}, _) => raise Match | _ => let val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; @@ -246,7 +246,7 @@ end) | split_guess_names_tr' _ T [t] = (case head_of t of - Const (@{const_syntax split}, _) => raise Match + Const (@{const_syntax prod_case}, _) => raise Match | _ => let val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; @@ -257,21 +257,12 @@ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' end) | split_guess_names_tr' _ _ _ = raise Match; -in [(@{const_syntax split}, split_guess_names_tr')] end +in [(@{const_syntax prod_case}, split_guess_names_tr')] end *} subsubsection {* Code generator setup *} -lemma split_case_cert: - assumes "CASE \ split f" - shows "CASE (a, b) \ f a b" - using assms by (simp add: split_prod_case) - -setup {* - Code.add_case @{thm split_case_cert} -*} - code_type * (SML infix 2 "*") (OCaml infix 2 "*") @@ -315,7 +306,7 @@ val s' = Codegen.new_name t s; val v = Free (s', T) in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end - | strip_abs_split i (u as Const (@{const_name split}, _) $ t) = + | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) = (case strip_abs_split (i+1) t of (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u) | _ => ([], u)) @@ -357,7 +348,7 @@ | _ => NONE); fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of - (t1 as Const (@{const_name split}, _), t2 :: ts) => + (t1 as Const (@{const_name prod_case}, _), t2 :: ts) => let val ([p], u) = strip_abs_split 1 (t1 $ t2); val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr; @@ -421,7 +412,7 @@ by (simp add: Pair_fst_snd_eq) lemma split_conv [simp, code]: "split f (a, b) = f a b" - by (simp add: split_prod_case) + by (fact prod.cases) lemma splitI: "f a b \ split f (a, b)" by (rule split_conv [THEN iffD2]) @@ -430,11 +421,11 @@ by (rule split_conv [THEN iffD1]) lemma split_Pair [simp]: "(\(x, y). (x, y)) = id" - by (simp add: split_prod_case expand_fun_eq split: prod.split) + by (simp add: expand_fun_eq split: prod.split) lemma split_eta: "(\(x, y). f (x, y)) = f" -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} - by (simp add: split_prod_case expand_fun_eq split: prod.split) + by (simp add: expand_fun_eq split: prod.split) lemma split_comp: "split (f \ g) x = f (g (fst x)) (snd x)" by (cases x) simp @@ -443,7 +434,7 @@ by (cases p) simp lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" - by (simp add: split_prod_case prod_case_unfold) + by (simp add: prod_case_unfold) lemma split_weak_cong: "p = q \ split c p = split c q" -- {* Prevents simplification of @{term c}: much faster *} @@ -529,7 +520,7 @@ | no_args k i (Bound m) = m < k orelse m > k + i | no_args _ _ _ = true; fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE - | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t + | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t | split_pat tp i _ = NONE; fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) @@ -546,12 +537,12 @@ if Pair_pat k i (t $ u) then incr_boundvars k arg else (subst arg k i t $ subst arg k i u) | subst arg k i t = t; - fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) = + fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) = (case split_pat beta_term_pat 1 t of SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f)) | NONE => NONE) | beta_proc _ _ = NONE; - fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) = + fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = (case split_pat eta_term_pat 1 t of SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end)) | NONE => NONE) @@ -598,10 +589,10 @@ done lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" - by (induct p) (auto simp add: split_prod_case) + by (induct p) auto lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" - by (induct p) (auto simp add: split_prod_case) + by (induct p) auto lemma splitE2: "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R" @@ -627,14 +618,14 @@ assumes major: "z \ split c p" and cases: "\x y. p = (x, y) \ z \ c x y \ Q" shows Q - by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+ + by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+ declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!] declare mem_splitE [elim!] splitE' [elim!] splitE [elim!] ML {* local (* filtering with exists_p_split is an essential optimization *) - fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true + fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u | exists_p_split (Abs (_, _, t)) = exists_p_split t | exists_p_split _ = false; @@ -712,13 +703,9 @@ declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] declare prod_caseE' [elim!] prod_caseE [elim!] -lemma prod_case_split: - "prod_case = split" - by (auto simp add: expand_fun_eq) - lemma prod_case_beta: "prod_case f p = f (fst p) (snd p)" - unfolding prod_case_split split_beta .. + by (fact split_beta) lemma prod_cases3 [cases type]: obtains (fields) a b c where "y = (a, b, c)" @@ -762,7 +749,7 @@ lemma split_def: "split = (\c p. c (fst p) (snd p))" - unfolding split_prod_case prod_case_unfold .. + by (fact prod_case_unfold) definition internal_split :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" where "internal_split == split" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Quotient.thy Tue Jun 29 11:38:51 2010 +0200 @@ -764,13 +764,23 @@ subsection {* Methods / Interface *} method_setup lifting = - {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *} + {* Attrib.thms >> (fn thms => fn ctxt => + SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *} {* lifts theorems to quotient types *} method_setup lifting_setup = - {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *} + {* Attrib.thm >> (fn thm => fn ctxt => + SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *} {* sets up the three goals for the quotient lifting procedure *} +method_setup descending = + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *} + {* decends theorems to the raw level *} + +method_setup descending_setup = + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *} + {* sets up the three goals for the decending theorems *} + method_setup regularize = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *} {* proves the regularization goals from the quotient lifting procedure *} diff -r df12f798df99 -r ff1137a9c056 src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Jun 29 11:38:51 2010 +0200 @@ -114,43 +114,6 @@ apply(assumption) done -lemma plus_assoc_raw: - shows "plus_int_raw (plus_int_raw i j) k \ plus_int_raw i (plus_int_raw j k)" - by (cases i, cases j, cases k) (simp) - -lemma plus_sym_raw: - shows "plus_int_raw i j \ plus_int_raw j i" - by (cases i, cases j) (simp) - -lemma plus_zero_raw: - shows "plus_int_raw (0, 0) i \ i" - by (cases i) (simp) - -lemma plus_minus_zero_raw: - shows "plus_int_raw (uminus_int_raw i) i \ (0, 0)" - by (cases i) (simp) - -lemma times_assoc_raw: - shows "times_int_raw (times_int_raw i j) k \ times_int_raw i (times_int_raw j k)" - by (cases i, cases j, cases k) - (simp add: algebra_simps) - -lemma times_sym_raw: - shows "times_int_raw i j \ times_int_raw j i" - by (cases i, cases j) (simp add: algebra_simps) - -lemma times_one_raw: - shows "times_int_raw (1, 0) i \ i" - by (cases i) (simp) - -lemma times_plus_comm_raw: - shows "times_int_raw (plus_int_raw i j) k \ plus_int_raw (times_int_raw i k) (times_int_raw j k)" -by (cases i, cases j, cases k) - (simp add: algebra_simps) - -lemma one_zero_distinct: - shows "\ (0, 0) \ ((1::nat), (0::nat))" - by simp text{* The integers form a @{text comm_ring_1}*} @@ -158,25 +121,25 @@ proof fix i j k :: int show "(i + j) + k = i + (j + k)" - by (lifting plus_assoc_raw) + by (descending) (auto) show "i + j = j + i" - by (lifting plus_sym_raw) + by (descending) (auto) show "0 + i = (i::int)" - by (lifting plus_zero_raw) + by (descending) (auto) show "- i + i = 0" - by (lifting plus_minus_zero_raw) + by (descending) (auto) show "i - j = i + - j" by (simp add: minus_int_def) show "(i * j) * k = i * (j * k)" - by (lifting times_assoc_raw) + by (descending) (auto simp add: algebra_simps) show "i * j = j * i" - by (lifting times_sym_raw) + by (descending) (auto) show "1 * i = i" - by (lifting times_one_raw) + by (descending) (auto) show "(i + j) * k = i * k + j * k" - by (lifting times_plus_comm_raw) + by (descending) (auto simp add: algebra_simps) show "0 \ (1::int)" - by (lifting one_zero_distinct) + by (descending) (auto) qed lemma plus_int_raw_rsp_aux: @@ -211,36 +174,19 @@ by (induct m) (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int) -lemma le_antisym_raw: - shows "le_int_raw i j \ le_int_raw j i \ i \ j" - by (cases i, cases j) (simp) - -lemma le_refl_raw: - shows "le_int_raw i i" - by (cases i) (simp) - -lemma le_trans_raw: - shows "le_int_raw i j \ le_int_raw j k \ le_int_raw i k" - by (cases i, cases j, cases k) (simp) - -lemma le_cases_raw: - shows "le_int_raw i j \ le_int_raw j i" - by (cases i, cases j) - (simp add: linorder_linear) - instance int :: linorder proof fix i j k :: int show antisym: "i \ j \ j \ i \ i = j" - by (lifting le_antisym_raw) + by (descending) (auto) show "(i < j) = (i \ j \ \ j \ i)" by (auto simp add: less_int_def dest: antisym) show "i \ i" - by (lifting le_refl_raw) + by (descending) (auto) show "i \ j \ j \ k \ i \ k" - by (lifting le_trans_raw) + by (descending) (auto) show "i \ j \ j \ i" - by (lifting le_cases_raw) + by (descending) (auto) qed instantiation int :: distrib_lattice @@ -258,15 +204,11 @@ end -lemma le_plus_int_raw: - shows "le_int_raw i j \ le_int_raw (plus_int_raw k i) (plus_int_raw k j)" - by (cases i, cases j, cases k) (simp) - instance int :: ordered_cancel_ab_semigroup_add proof fix i j k :: int show "i \ j \ k + i \ k + j" - by (lifting le_plus_int_raw) + by (descending) (auto) qed abbreviation @@ -296,7 +238,7 @@ fixes k::int shows "0 < k \ \n > 0. k = of_nat n" unfolding less_int_def int_of_nat - by (lifting zero_le_imp_eq_int_raw) + by (descending) (rule zero_le_imp_eq_int_raw) lemma zmult_zless_mono2: fixes i j k::int @@ -365,16 +307,10 @@ shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw" by (auto iff: int_to_nat_raw_def) -lemma nat_le_eq_zle_raw: - assumes a: "less_int_raw (0, 0) w \ le_int_raw (0, 0) z" - shows "(int_to_nat_raw w \ int_to_nat_raw z) = (le_int_raw w z)" - using a - by (cases w, cases z) (auto simp add: int_to_nat_raw_def) - lemma nat_le_eq_zle: fixes w z::"int" shows "0 < w \ 0 \ z \ (int_to_nat w \ int_to_nat z) = (w \ z)" unfolding less_int_def - by (lifting nat_le_eq_zle_raw) + by (descending) (auto simp add: int_to_nat_raw_def) end diff -r df12f798df99 -r ff1137a9c056 src/HOL/Quotient_Examples/Quotient_Message.thy --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Jun 29 11:38:51 2010 +0200 @@ -32,7 +32,7 @@ text{*Proving that it is an equivalence relation*} lemma msgrel_refl: "X \ X" -by (induct X, (blast intro: msgrel.intros)+) +by (induct X) (auto intro: msgrel.intros) theorem equiv_msgrel: "equivp msgrel" proof (rule equivpI) @@ -263,68 +263,47 @@ subsection{*Injectivity Properties of Some Constructors*} -lemma NONCE_imp_eq: - shows "NONCE m \ NONCE n \ m = n" - by (drule msgrel_imp_eq_freenonces, simp) - text{*Can also be proved using the function @{term nonces}*} lemma Nonce_Nonce_eq [iff]: shows "(Nonce m = Nonce n) = (m = n)" proof assume "Nonce m = Nonce n" - then show "m = n" by (lifting NONCE_imp_eq) + then show "m = n" + by (descending) (drule msgrel_imp_eq_freenonces, simp) next assume "m = n" then show "Nonce m = Nonce n" by simp qed -lemma MPAIR_imp_eqv_left: - shows "MPAIR X Y \ MPAIR X' Y' \ X \ X'" - by (drule msgrel_imp_eqv_freeleft) (simp) - lemma MPair_imp_eq_left: assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'" - using eq by (lifting MPAIR_imp_eqv_left) - -lemma MPAIR_imp_eqv_right: - shows "MPAIR X Y \ MPAIR X' Y' \ Y \ Y'" - by (drule msgrel_imp_eqv_freeright) (simp) + using eq + by (descending) (drule msgrel_imp_eqv_freeleft, simp) lemma MPair_imp_eq_right: shows "MPair X Y = MPair X' Y' \ Y = Y'" - by (lifting MPAIR_imp_eqv_right) + by (descending) (drule msgrel_imp_eqv_freeright, simp) theorem MPair_MPair_eq [iff]: shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) -lemma NONCE_neqv_MPAIR: - shows "\(NONCE m \ MPAIR X Y)" - by (auto dest: msgrel_imp_eq_freediscrim) - theorem Nonce_neq_MPair [iff]: shows "Nonce N \ MPair X Y" - by (lifting NONCE_neqv_MPAIR) + by (descending) (auto dest: msgrel_imp_eq_freediscrim) text{*Example suggested by a referee*} -lemma CRYPT_NONCE_neq_NONCE: - shows "\(CRYPT K (NONCE M) \ NONCE N)" - by (auto dest: msgrel_imp_eq_freediscrim) - theorem Crypt_Nonce_neq_Nonce: shows "Crypt K (Nonce M) \ Nonce N" - by (lifting CRYPT_NONCE_neq_NONCE) + by (descending) (auto dest: msgrel_imp_eq_freediscrim) text{*...and many similar results*} -lemma CRYPT2_NONCE_neq_NONCE: - shows "\(CRYPT K (CRYPT K' (NONCE M)) \ NONCE N)" - by (auto dest: msgrel_imp_eq_freediscrim) theorem Crypt2_Nonce_neq_Nonce: shows "Crypt K (Crypt K' (Nonce M)) \ Nonce N" - by (lifting CRYPT2_NONCE_neq_NONCE) + by (descending) (auto dest: msgrel_imp_eq_freediscrim) theorem Crypt_Crypt_eq [iff]: shows "(Crypt K X = Crypt K X') = (X=X')" diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 29 11:38:51 2010 +0200 @@ -2080,7 +2080,7 @@ list_abs (outer, Const (@{const_name Image}, uncurried_T --> set_T --> set_T) $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T) - $ (Const (@{const_name split}, curried_T --> uncurried_T) + $ (Const (@{const_name prod_case}, curried_T --> uncurried_T) $ list_comb (Const step_x, outer_bounds))) $ list_comb (Const base_x, outer_bounds) |> ap_curry tuple_arg_Ts tuple_T) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Jun 29 11:38:51 2010 +0200 @@ -2015,7 +2015,7 @@ | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t) | split_lambda t _ = raise (TERM ("split_lambda", [t])) -fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t +fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t | strip_split_abs (Abs (_, _, t)) = strip_split_abs t | strip_split_abs t = t diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Jun 29 11:38:51 2010 +0200 @@ -179,7 +179,7 @@ |> maps (fn (res, (names, prems)) => flatten' (betapply (g, res)) (names, prems)) end) - | Const (@{const_name split}, _) => + | Const (@{const_name prod_case}, _) => (let val (_, g :: res :: args) = strip_comb t val [res1, res2] = Name.variant_list names ["res1", "res2"] diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Jun 29 11:38:51 2010 +0200 @@ -92,7 +92,7 @@ fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = let val rty = fastype_of rconst - val qty = derive_qtyp qtys rty false ctxt + val qty = derive_qtyp qtys rty ctxt val lhs = Free (qconst_name, qty) in quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Jun 29 11:38:51 2010 +0200 @@ -11,10 +11,13 @@ val injection_tac: Proof.context -> int -> tactic val all_injection_tac: Proof.context -> int -> tactic val clean_tac: Proof.context -> int -> tactic - val procedure_tac: Proof.context -> thm list -> int -> tactic + + val descend_procedure_tac: Proof.context -> int -> tactic + val descend_tac: Proof.context -> int -> tactic + + val lift_procedure_tac: Proof.context -> thm -> int -> tactic val lift_tac: Proof.context -> thm list -> int -> tactic - val quotient_tac: Proof.context -> int -> tactic - val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic + val lifted: typ list -> Proof.context -> thm -> thm val lifted_attrib: attribute end; @@ -615,76 +618,82 @@ SOME (cterm_of thy inj_goal)] lifting_procedure_thm end -(* the tactic leaves three subgoals to be proved *) -fun procedure_tac ctxt rthm = + +(** descending as tactic **) + +fun descend_procedure_tac ctxt = Object_Logic.full_atomize_tac THEN' gen_frees_tac ctxt THEN' SUBGOAL (fn (goal, i) => - case rthm of - [] => let val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) - val rtrm = derive_qtrm qtys goal true ctxt - val rule = procedure_inst ctxt rtrm goal + val rtrm = derive_rtrm qtys goal ctxt + val rule = procedure_inst ctxt rtrm goal in rtac rule i - end - | [rthm'] => - let - val rthm'' = atomize_thm rthm' - val rule = procedure_inst ctxt (prop_of rthm'') goal - in - (rtac rule THEN' rtac rthm'') i - end - | _ => error "more than one raw theorem given") + end) + +fun descend_tac ctxt = +let + val mk_tac_raw = + descend_procedure_tac ctxt + THEN' RANGE + [Object_Logic.rulify_tac THEN' (K all_tac), + regularize_tac ctxt, + all_injection_tac ctxt, + clean_tac ctxt] +in + Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw +end -(* Automatic Proofs *) +(** lifting as tactic **) + +(* the tactic leaves three subgoals to be proved *) +fun lift_procedure_tac ctxt rthm = + Object_Logic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' SUBGOAL (fn (goal, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') goal + in + (rtac rule THEN' rtac rthm') i + end) fun lift_tac ctxt rthms = let fun mk_tac rthm = - procedure_tac ctxt [rthm] - THEN' RANGE - [regularize_tac ctxt, - all_injection_tac ctxt, - clean_tac ctxt]; - val mk_tac_raw = - procedure_tac ctxt [] + lift_procedure_tac ctxt rthm THEN' RANGE - [fn _ => all_tac, - regularize_tac ctxt, - all_injection_tac ctxt, - clean_tac ctxt] + [ regularize_tac ctxt, + all_injection_tac ctxt, + clean_tac ctxt ] in - simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) - THEN' - (case rthms of - [] => mk_tac_raw - | _ => RANGE (map mk_tac rthms)) + Goal.conjunction_tac THEN' RANGE (map mk_tac rthms) end + +(** lifting as attribute **) + fun lifted qtys ctxt thm = let (* When the theorem is atomized, eta redexes are contracted, so we do it both in the original theorem *) val thm' = Drule.eta_contraction_rule thm val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt - val goal = derive_qtrm qtys (prop_of thm'') false ctxt' + val goal = derive_qtrm qtys (prop_of thm'') ctxt' in Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1)) |> singleton (ProofContext.export ctxt' ctxt) end; -(* An attribute which automatically constructs the qthm - using all quotients defined so far. -*) val lifted_attrib = Thm.rule_attribute (fn context => - let - val ctxt = Context.proof_of context - val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) - in - lifted qtys ctxt - end) + let + val ctxt = Context.proof_of context + val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) + in + lifted qtys ctxt + end) end; (* structure *) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Jun 29 11:38:51 2010 +0200 @@ -26,8 +26,10 @@ val inj_repabs_trm: Proof.context -> term * term -> term val inj_repabs_trm_chk: Proof.context -> term * term -> term - val derive_qtyp: typ list -> typ -> bool -> Proof.context -> typ - val derive_qtrm: typ list -> term -> bool -> Proof.context -> term + val derive_qtyp: typ list -> typ -> Proof.context -> typ + val derive_qtrm: typ list -> term -> Proof.context -> term + val derive_rtyp: typ list -> typ -> Proof.context -> typ + val derive_rtrm: typ list -> term -> Proof.context -> term end; structure Quotient_Term: QUOTIENT_TERM = @@ -560,12 +562,12 @@ end end - | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), - ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => + | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), + ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) - | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)), - ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) => + | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)), + ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) => regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) | (t1 $ t2, t1' $ t2') => @@ -690,16 +692,15 @@ (*** Wrapper for automatically transforming an rthm into a qthm ***) -(* subst_rty takes a list of (rty, qty) substitution pairs - and replaces all occurences of rty in the given type - by an appropriate qty +(* substitutions functions for r/q-types and + r/q-constants, respectively *) -fun subst_rtyp ctxt ty_subst rty = +fun subst_typ ctxt ty_subst rty = case rty of Type (s, rtys) => let val thy = ProofContext.theory_of ctxt - val rty' = Type (s, map (subst_rtyp ctxt ty_subst) rtys) + val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys) fun matches [] = rty' | matches ((rty, qty)::tail) = @@ -711,23 +712,18 @@ end | _ => rty -(* subst_rtrm takes a list of (rconst, qconst) substitution pairs, - as well as (rty, qty) substitution pairs, and replaces all - occurences of rconst and rty by appropriate instances of - qconst and qty -*) -fun subst_rtrm ctxt ty_subst trm_subst rtrm = +fun subst_trm ctxt ty_subst trm_subst rtrm = case rtrm of - t1 $ t2 => (subst_rtrm ctxt ty_subst trm_subst t1) $ (subst_rtrm ctxt ty_subst trm_subst t2) - | Abs (x, ty, t) => Abs (x, subst_rtyp ctxt ty_subst ty, subst_rtrm ctxt ty_subst trm_subst t) - | Free(n, ty) => Free(n, subst_rtyp ctxt ty_subst ty) - | Var(n, ty) => Var(n, subst_rtyp ctxt ty_subst ty) + t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2) + | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t) + | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty) + | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty) | Bound i => Bound i | Const (a, ty) => let val thy = ProofContext.theory_of ctxt - fun matches [] = Const (a, subst_rtyp ctxt ty_subst ty) + fun matches [] = Const (a, subst_typ ctxt ty_subst ty) | matches ((rconst, qconst)::tail) = case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of NONE => matches tail @@ -736,44 +732,55 @@ matches trm_subst end -(* generates type substitutions out of the - types involved in a quotient +(* generate type and term substitutions out of the + qtypes involved in a quotient; the direction flag + indicates in which direction the substitutions work: + + true: quotient -> raw + false: raw -> quotient *) -fun get_ty_subst qtys reverse ctxt = +fun mk_ty_subst qtys direction ctxt = Quotient_Info.quotdata_dest ctxt |> map (fn x => (#rtyp x, #qtyp x)) |> filter (fn (_, qty) => member (op =) qtys qty) - |> map (fn (x, y) => if reverse then (y, x) else (x, y)) + |> map (if direction then swap else I) -(* generates term substitutions out of the qconst - definitions and relations in a quotient -*) -fun get_trm_subst qtys reverse ctxt = +fun mk_trm_subst qtys direction ctxt = let - val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys reverse ctxt) - fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt) + val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) + fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 val const_substs = Quotient_Info.qconsts_dest ctxt |> map (fn x => (#rconst x, #qconst x)) - |> map (fn (x, y) => if reverse then (y, x) else (x, y)) + |> map (if direction then swap else I) val rel_substs = Quotient_Info.quotdata_dest ctxt |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) - |> map (fn (x, y) => if reverse then (y, x) else (x, y)) + |> map (if direction then swap else I) in filter proper (const_substs @ rel_substs) end + (* derives a qtyp and qtrm out of a rtyp and rtrm, respectively *) -fun derive_qtyp qtys rty unlift ctxt = - subst_rtyp ctxt (get_ty_subst qtys unlift ctxt) rty +fun derive_qtyp qtys rty ctxt = + subst_typ ctxt (mk_ty_subst qtys false ctxt) rty + +fun derive_qtrm qtys rtrm ctxt = + subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm -fun derive_qtrm qtys rtrm unlift ctxt = - subst_rtrm ctxt (get_ty_subst qtys unlift ctxt) (get_trm_subst qtys unlift ctxt) rtrm +(* derives a rtyp and rtrm out of a qtyp and qtrm, + respectively +*) +fun derive_rtyp qtys qty ctxt = + subst_typ ctxt (mk_ty_subst qtys true ctxt) qty + +fun derive_rtrm qtys qtrm ctxt = + subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm end; (* structure *) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/TFL/usyntax.ML --- a/src/HOL/Tools/TFL/usyntax.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/TFL/usyntax.ML Tue Jun 29 11:38:51 2010 +0200 @@ -196,7 +196,7 @@ local fun mk_uncurry (xt, yt, zt) = - Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt) + Const(@{const_name prod_case}, (xt --> yt --> zt) --> prod_ty xt yt --> zt) fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N} | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false @@ -276,7 +276,7 @@ | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; -local fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t +local fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} then t else raise Match) in fun dest_pabs used tm = diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/hologic.ML Tue Jun 29 11:38:51 2010 +0200 @@ -315,12 +315,12 @@ end; fun split_const (A, B, C) = - Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C); + Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C); fun mk_split t = (case Term.fastype_of t of T as (Type ("fun", [A, Type ("fun", [B, C])])) => - Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t + Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t | _ => raise TERM ("mk_split: bad body type", [t])); (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) @@ -427,7 +427,7 @@ val strip_psplits = let fun strip [] qs Ts t = (t, rev Ts, qs) - | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) = + | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) = strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t | strip (p :: ps) qs Ts t = strip ps qs diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Tue Jun 29 11:38:51 2010 +0200 @@ -374,7 +374,7 @@ fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; fun mk_split T = Sign.mk_const thy - (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]); + (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]); fun mk_scomp_split T t t' = mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t'))); @@ -414,7 +414,7 @@ fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; fun mk_split T = Sign.mk_const thy - (@{const_name split}, [T, @{typ "unit => term"}, + (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]); fun mk_scomp_split T t t' = mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t diff -r df12f798df99 -r ff1137a9c056 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Tools/refute.ML Tue Jun 29 11:38:51 2010 +0200 @@ -2234,7 +2234,7 @@ (* sanity check: every element of terms' must also be *) (* present in terms *) val _ = - if List.all (member (op =) terms) terms' then () + if forall (member (op =) terms) terms' then () else raise REFUTE ("IDT_constructor_interpreter", "element has disappeared") @@ -2957,7 +2957,7 @@ (* "lfp(f) == Inter({u. f(u) <= u})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) = - List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) | is_subset (_, _) = raise REFUTE ("lfp_interpreter", @@ -3012,7 +3012,7 @@ (* "gfp(f) == Union({u. u <= f(u)})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) = - List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) | is_subset (_, _) = raise REFUTE ("gfp_interpreter", diff -r df12f798df99 -r ff1137a9c056 src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Word/Num_Lemmas.thy Tue Jun 29 11:38:51 2010 +0200 @@ -11,8 +11,8 @@ lemma contentsI: "y = {x} ==> contents y = x" unfolding contents_def by auto -- {* FIXME move *} -lemmas split_split = prod.split [unfolded prod_case_split] -lemmas split_split_asm = prod.split_asm [unfolded prod_case_split] +lemmas split_split = prod.split +lemmas split_split_asm = prod.split_asm lemmas split_splits = split_split split_split_asm lemmas funpow_0 = funpow.simps(1) diff -r df12f798df99 -r ff1137a9c056 src/HOL/Word/WordShift.thy --- a/src/HOL/Word/WordShift.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/Word/WordShift.thy Tue Jun 29 11:38:51 2010 +0200 @@ -988,8 +988,10 @@ apply (erule bin_nth_uint_imp)+ done -lemmas test_bit_split = - test_bit_split' [THEN mp, simplified all_simps, standard] +lemma test_bit_split: + "word_split c = (a, b) \ + (\n\nat. b !! n \ n < size b \ c !! n) \ (\m\nat. a !! m \ m < size a \ c !! (m + size b))" + by (simp add: test_bit_split') lemma test_bit_split_eq: "word_split c = (a, b) <-> ((ALL n::nat. b !! n = (n < size b & c !! n)) & diff -r df12f798df99 -r ff1137a9c056 src/HOL/ex/Execute_Choice.thy --- a/src/HOL/ex/Execute_Choice.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/ex/Execute_Choice.thy Tue Jun 29 11:38:51 2010 +0200 @@ -66,7 +66,7 @@ shows [code]: "valuesum (Mapping []) = 0" and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \ Mapping.keys (Mapping (x # xs))) in the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" - by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping) + by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def) text {* As a side effect the precondition disappears (but note this has nothing to do with choice!). diff -r df12f798df99 -r ff1137a9c056 src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/ex/Meson_Test.thy Tue Jun 29 11:38:51 2010 +0200 @@ -16,7 +16,7 @@ below and constants declared in HOL! *} -hide_const (open) subset member quotient union inter sum +hide_const (open) subset quotient union inter sum text {* Test data for the MESON proof procedure diff -r df12f798df99 -r ff1137a9c056 src/HOL/ex/Recdefs.thy --- a/src/HOL/ex/Recdefs.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOL/ex/Recdefs.thy Tue Jun 29 11:38:51 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Recdefs.thy - ID: $Id$ Author: Konrad Slind and Lawrence C Paulson Copyright 1996 University of Cambridge @@ -44,7 +43,7 @@ text {* Not handled automatically: too complicated. *} consts variant :: "nat * nat list => nat" recdef (permissive) variant "measure (\(n,ns). size (filter (\y. n \ y) ns))" - "variant (x, L) = (if x mem L then variant (Suc x, L) else x)" + "variant (x, L) = (if x \ set L then variant (Suc x, L) else x)" consts gcd :: "nat * nat => nat" recdef gcd "measure (\(x, y). x + y)" diff -r df12f798df99 -r ff1137a9c056 src/HOLCF/IOA/meta_theory/TLS.thy --- a/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jun 29 11:38:51 2010 +0200 @@ -86,7 +86,7 @@ "(mkfin (a>>s)) = (a>>(mkfin s))" -lemmas [simp del] = ex_simps all_simps split_paired_Ex +lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} diff -r df12f798df99 -r ff1137a9c056 src/HOLCF/IOA/meta_theory/Traces.thy --- a/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jun 29 11:38:51 2010 +0200 @@ -192,7 +192,7 @@ "Traces A == (traces A,asig_of A)" -lemmas [simp del] = ex_simps all_simps split_paired_Ex +lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex declare Let_def [simp] declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} diff -r df12f798df99 -r ff1137a9c056 src/HOLCF/ex/Focus_ex.thy --- a/src/HOLCF/ex/Focus_ex.thy Tue Jun 29 11:29:31 2010 +0200 +++ b/src/HOLCF/ex/Focus_ex.thy Tue Jun 29 11:38:51 2010 +0200 @@ -204,7 +204,7 @@ done lemma lemma4: "is_g(g) --> def_g(g)" -apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps") +apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps}) addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *}) apply (rule impI) apply (erule exE)