--- 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
--- 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}\\
--- /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 \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
+\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
+\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> 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 \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> 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 \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
+ "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> 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 \<Longrightarrow> lexord r (xs, ys)"
+(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
+
+lemma %quote [code_pred_intro]:
+ "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
+ \<Longrightarrow> 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: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
+ assume 2: "\<And> r' xs' ys' u a v b w. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' (a, b) \<Longrightarrow> thesis"
+ {
+ assume "\<exists>a v. ys = xs @ a # v"
+ from this 1 have thesis
+ by (fastsimp simp add: append)
+ } moreover
+ {
+ assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> 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 \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "succ 0 (Suc 0)"
+| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
+
+code_pred succ .
+
+text {*
+\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
+ @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> 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 \<Rightarrow> o \<Rightarrow> 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
--- 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}
--- 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 \<in> set xs \<longleftrightarrow> member xs x" by (fact in_set_code)
+ "x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
text {*
\item eliminating superfluous constants:
@@ -188,7 +188,7 @@
*}
lemma %quote [code_unfold]:
- "xs = [] \<longleftrightarrow> List.null xs" by (fact empty_null)
+ "xs = [] \<longleftrightarrow> 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 \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
-\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
-\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> 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 \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> 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 \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
- "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> 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 \<Longrightarrow> lexord r (xs, ys)"
-(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
-
-lemma %quote [code_pred_intro]:
- "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
- \<Longrightarrow> 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: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
- assume 2: "\<And> r' xs' ys' u a v b w. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' (a, b) \<Longrightarrow> thesis"
- {
- assume "\<exists>a v. ys = xs @ a # v"
- from this 1 have thesis
- by (fastsimp simp add: append)
- } moreover
- {
- assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> 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 \<Rightarrow> nat \<Rightarrow> bool"
-where
- "succ 0 (Suc 0)"
-| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
-
-code_pred succ .
-
-text {*
-\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
- @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> 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 \<Rightarrow> o \<Rightarrow> 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
--- 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";
--- /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:
--- 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;\\
--- 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}
--- 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
--- 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;
--- 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 ([], []);
--- 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}
--- 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%
--- 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 \<in> 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 \<in> 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)
--- 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 \<in> 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 \<in> 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)
--- 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 \<Rightarrow> bool" where
-"groundVar v \<equiv> (case v of
+"groundVar v \<longleftrightarrow> (case v of
LVar ln \<Rightarrow> True
| {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
| e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
@@ -35,19 +35,15 @@
qed
definition groundExprs :: "expr list \<Rightarrow> bool" where
-"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
+ "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
-consts the_val:: "expr \<Rightarrow> val"
-primrec
-"the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val" where
+ "the_val (Lit v) = v"
-consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> 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 \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> 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"
--- 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 \<noteq> 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")
--- 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 \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> 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"
--- 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 @@
"\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
by (induct ys) simp+
-theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
+theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
by (induct xs, simp+, iprover)
theorem list_all_lemma:
--- 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;
*}
--- 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;
*}
--- 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**)
--- 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)
--- 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.
--- 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"
--- 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 \<equiv> 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 \<Rightarrow> 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 \<Rightarrow> bool,'a list] \<Rightarrow> 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
--- 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. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
shows term_induct2: "P t"
- and "list_all P ts"
+ and "\<forall>t \<in> set ts. P t"
apply (induct t and ts)
apply (rule var)
apply (rule app)
--- 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. (\<forall>t \<in> 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 "\<forall>t \<in> set ts. P t"
then show "P (App b ts)" by (rule app)
next
- show "list_all P []" by simp
+ show "\<forall>t \<in> 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" "\<forall>t' \<in> set ts. P t'"
+ then show "\<forall>t' \<in> set (t # ts). P t'" by simp
qed
lemma
--- 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 \<union> fst ` set ys"
by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -449,7 +448,7 @@
More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> 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) \<longleftrightarrow> null xs"
- by (cases xs) (simp_all add: is_empty_def)
+ "Mapping.is_empty (Mapping xs) \<longleftrightarrow> 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)"
--- 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 "\<not> 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 "\<not> 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) \<longleftrightarrow> 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"
--- 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\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
- and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>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 \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> 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]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
by (simp add: list_all_iff enum_all)
-lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
- by (simp add: list_all_iff enum_all)
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
+ by (simp add: list_ex_iff enum_all)
subsection {* Default instances *}
--- 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 \<in> Set xs \<longleftrightarrow> member xs x"
- "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
- by (simp_all add: mem_iff)
+ "x \<in> Set xs \<longleftrightarrow> List.member xs x"
+ "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
+ by (simp_all add: member_def)
definition is_empty :: "'a set \<Rightarrow> bool" where
[simp]: "is_empty A \<longleftrightarrow> A = {}"
@@ -85,8 +85,8 @@
*}
lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> null xs"
- by (simp add: empty_null)
+ "is_empty (Set xs) \<longleftrightarrow> 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 \<longleftrightarrow> list_all P xs"
- by (simp add: ball_set)
+ by (simp add: list_all_iff)
lemma Bex_Set [code]:
"Bex (Set xs) P \<longleftrightarrow> 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)"
--- 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 \<circ> 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 \<longleftrightarrow> More_Set.is_empty (member A)"
lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> null xs"
+ "is_empty (Set xs) \<longleftrightarrow> 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) \<longleftrightarrow> list_all P xs"
- by (simp add: Set_def ball_set)
+ by (simp add: Set_def list_all_iff)
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
[simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
lemma exists_Set [code]:
"exists P (Set xs) \<longleftrightarrow> list_ex P xs"
- by (simp add: Set_def bex_set)
+ by (simp add: Set_def list_ex_iff)
definition card :: "'a fset \<Rightarrow> nat" where
[simp]: "card A = Finite_Set.card (member A)"
--- 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) \<longleftrightarrow> null xs"
- by (simp add: is_empty_def null_empty)
-
-lemma ball_set:
- "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
- by (rule list_ball_code)
-
-lemma bex_set:
- "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
- by (rule list_bex_code)
+ "is_empty (set xs) \<longleftrightarrow> List.null xs"
+ by (simp add: is_empty_def null_def)
lemma empty_set:
"{} = set []"
--- 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
--- 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 *}
--- 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
--- 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 *}
--- 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 \<noteq> 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)
--- 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
--- 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 (\<lambda>xs x. x # xs) [] xs"
+proof (induct xs)
+ case Nil then show ?case by simp
+next
+ case Cons
+ {
+ fix x xs ys
+ have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
+ = foldl (\<lambda>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"\<Sum>"}*}
-
-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\<Colon>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 \<Rightarrow> ('b::comm_monoid_add)"
-shows "x : set xs \<Longrightarrow> 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 \<Rightarrow> 'b \<Colon> comm_monoid_add"
- assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> listsum xs = Setsum(set xs)"
-by (induct xs) simp_all
-
-lemma listsum_eq_0_nat_iff_nat[simp]:
- "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
-by(simp add: listsum)
-
-lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> 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<size ns \<Longrightarrow>
- 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\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-
-translations -- {* Beware of argument permutation! *}
- "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
- "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
-
-lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
- by (induct xs) (simp_all add: left_distrib)
-
-lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>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 \<Rightarrow> 'b\<Colon>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 \<Rightarrow> 'b::comm_monoid_add"
- shows "(\<Sum>x\<leftarrow>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 \<Rightarrow> 'b::ab_group_add"
- shows "(\<Sum>x\<leftarrow>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 \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
-by (induct xs, simp_all add: algebra_simps)
-
-lemma listsum_mult_const:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>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 "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
-by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
-
-lemma listsum_mono:
- fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
- shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
-by (induct xs, simp, simp add: add_mono)
-
-
subsubsection {* @{text upt} *}
lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
@@ -2961,6 +2863,137 @@
qed
+subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
+
+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\<Colon>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 \<Rightarrow> ('b::comm_monoid_add)"
+shows "x : set xs \<Longrightarrow> 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 \<Rightarrow> 'b \<Colon> comm_monoid_add"
+ assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> listsum xs = Setsum(set xs)"
+by (induct xs) simp_all
+
+lemma listsum_eq_0_nat_iff_nat[simp]:
+ "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
+by(simp add: listsum)
+
+lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> 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<size ns \<Longrightarrow>
+ 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\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax (HTML output)
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+
+translations -- {* Beware of argument permutation! *}
+ "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+ "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+
+lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
+ by (induct xs) (simp_all add: left_distrib)
+
+lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>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 \<Rightarrow> 'b\<Colon>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 \<Rightarrow> 'b::comm_monoid_add"
+ shows "(\<Sum>x\<leftarrow>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 \<Rightarrow> 'b::ab_group_add"
+ shows "(\<Sum>x\<leftarrow>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 \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_mult_const:
+ fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>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 "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
+
+lemma listsum_mono:
+ fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
+ shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
+by (induct xs, simp, simp add: add_mono)
+
+lemma listsum_distinct_conv_setsum_set:
+ "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
+ by (induct xs) simp_all
+
+lemma interv_listsum_conv_setsum_set_nat:
+ "listsum (map f [m..<n]) = setsum f (set [m..<n])"
+ by (simp add: listsum_distinct_conv_setsum_set)
+
+lemma interv_listsum_conv_setsum_set_int:
+ "listsum (map f [k..l]) = setsum f (set [k..l])"
+ by (simp add: listsum_distinct_conv_setsum_set)
+
+text {* General equivalence between @{const listsum} and @{const setsum} *}
+lemma listsum_setsum_nth:
+ "listsum xs = (\<Sum> 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 \<Rightarrow> 'a \<Rightarrow> bool" where
+ [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
+
+text {*
+ Only use @{text member} for generating executable code. Otherwise use
+ @{prop "x \<in> 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 \<longleftrightarrow> x = y \<or> member xs y"
+ "member [] y \<longleftrightarrow> False"
+ by (auto simp add: member_def)
+
+lemma in_set_member [code_unfold]:
+ "x \<in> set xs \<longleftrightarrow> 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 \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+ list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
+
+definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+ list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
+
+text {*
+ Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
+ over @{const list_all} and @{const list_ex} in specifications.
+*}
+
+lemma list_all_simps [simp, code]:
+ "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
+ "list_all P [] \<longleftrightarrow> True"
+ by (simp_all add: list_all_iff)
+
+lemma list_ex_simps [simp, code]:
+ "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"
+ "list_ex P [] \<longleftrightarrow> False"
+ by (simp_all add: list_ex_iff)
+
+lemma Ball_set_list_all [code_unfold]:
+ "Ball (set xs) P \<longleftrightarrow> list_all P xs"
+ by (simp add: list_all_iff)
+
+lemma Bex_set_list_ex [code_unfold]:
+ "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
+ by (simp add: list_ex_iff)
+
+lemma list_all_append [simp]:
+ "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"
+ by (auto simp add: list_all_iff)
+
+lemma list_ex_append [simp]:
+ "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"
+ by (auto simp add: list_ex_iff)
+
+lemma list_all_rev [simp]:
+ "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
+ by (simp add: list_all_iff)
+
+lemma list_ex_rev [simp]:
+ "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"
+ by (simp add: list_ex_iff)
+
+lemma list_all_length:
+ "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
+ by (auto simp add: list_all_iff set_conv_nth)
+
+lemma list_ex_length:
+ "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
+ by (auto simp add: list_ex_iff set_conv_nth)
+
+lemma list_all_cong [fundef_cong]:
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
+ by (simp add: list_all_iff)
+
+lemma list_any_cong [fundef_cong]:
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> 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..<Suc n]"
+ by auto
+
+lemma atLeast_upt [code_unfold]:
+ "{..<n} = set [0..<n]"
+ by auto
+
+lemma greaterThanLessThan_upt [code_unfold]:
+ "{n<..<m} = set [Suc n..<m]"
+ by auto
+
+lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
+
+lemma greaterThanAtMost_upt [code_unfold]:
+ "{n<..m} = set [Suc n..<Suc m]"
+ by auto
+
+lemma atLeastAtMost_upt [code_unfold]:
+ "{n..m} = set [n..<Suc m]"
+ by auto
+
+lemma all_nat_less_eq [code_unfold]:
+ "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
+ by auto
+
+lemma ex_nat_less_eq [code_unfold]:
+ "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
+ by auto
+
+lemma all_nat_less [code_unfold]:
+ "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
+ by auto
+
+lemma ex_nat_less [code_unfold]:
+ "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
+ by auto
+
+lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
+ "setsum f (set [m..<n]) = listsum (map f [m..<n])"
+ by (simp add: interv_listsum_conv_setsum_set_nat)
+
+text {* Summation over ints. *}
+
+lemma greaterThanLessThan_upto [code_unfold]:
+ "{i<..<j::int} = set [i+1..j - 1]"
+by auto
+
+lemma atLeastLessThan_upto [code_unfold]:
+ "{i..<j::int} = set [i..j - 1]"
+by auto
+
+lemma greaterThanAtMost_upto [code_unfold]:
+ "{i<..j::int} = set [i+1..j]"
+by auto
+
+lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
+
+lemma setsum_set_upto_conv_listsum_int [code_unfold]:
+ "setsum f (set [i..j::int]) = listsum (map f [i..j])"
+ by (simp add: interv_listsum_conv_setsum_set_int)
+
+
+subsubsection {* Optimizing by rewriting *}
+
+definition null :: "'a list \<Rightarrow> bool" where
+ [code_post]: "null xs \<longleftrightarrow> xs = []"
+
+text {*
+ Efficient emptyness check is implemented by @{const null}.
+*}
+
+lemma null_rec [code]:
+ "null (x # xs) \<longleftrightarrow> False"
+ "null [] \<longleftrightarrow> True"
+ by (simp_all add: null_def)
+
+lemma eq_Nil_null [code_unfold]:
+ "xs = [] \<longleftrightarrow> null xs"
+ by (simp add: null_def)
+
+lemma equal_Nil_null [code_unfold]:
+ "eq_class.eq xs [] \<longleftrightarrow> null xs"
+ by (simp add: eq eq_Nil_null)
+
+definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+ [code_post]: "maps f xs = concat (map f xs)"
+
+definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+ [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> 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 \<Rightarrow> map_filter f xs | Some y \<Rightarrow> 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 (\<lambda>x. if P x then Some (f x) else None) xs"
+ by (simp add: map_filter_def)
+
+text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
+and similiarly for @{text"\<exists>"}. *}
+
+definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
+
+lemma [code]:
+ "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
+proof -
+ have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
+ proof -
+ fix n
+ assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> 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..<j] \<longleftrightarrow> 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..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"
+ by (simp add: list_ex_iff all_interval_nat_def)
+
+definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
+ "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"
+
+lemma [code]:
+ "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
+proof -
+ have *: "\<And>k. P i \<Longrightarrow> \<forall>k\<in>{i+1..j}. P k \<Longrightarrow> i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> P k"
+ proof -
+ fix k
+ assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> 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] \<longleftrightarrow> 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] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> 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 \<Rightarrow> 'a \<Rightarrow> bool" where
- mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
-
-primrec
- null:: "'a list \<Rightarrow> bool"
-where
- "null [] = True"
- | "null (x#xs) = False"
-
-primrec
- list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "list_inter [] bs = []"
- | "list_inter (a#as) bs =
- (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
-
-primrec
- list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
-where
- "list_all P [] = True"
- | "list_all P (x#xs) = (P x \<and> list_all P xs)"
-
-primrec
- list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-where
- "list_ex P [] = False"
- | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
-
-primrec
- filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
-where
- "filtermap f [] = []"
- | "filtermap f (x#xs) =
- (case f x of None \<Rightarrow> filtermap f xs
- | Some y \<Rightarrow> y # filtermap f xs)"
-
-primrec
- map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> nat"
-where
- "length_unique [] = 0"
- | "length_unique (x#xs) =
- (if x \<in> 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 "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>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 "\<in>"},
- @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>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 (\<lambda>xs x. x # xs) [] xs"
-proof (induct xs)
- case Nil then show ?case by simp
-next
- case Cons
- {
- fix x xs ys
- have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
- = foldl (\<lambda>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 \<longleftrightarrow> x = y \<or> member xs y"
- "member [] y \<longleftrightarrow> 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 \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
- "x mem xs \<equiv> member xs x" -- "for backward compatibility"
-
-lemma empty_null:
- "xs = [] \<longleftrightarrow> null xs"
-by (cases xs) simp_all
-
-lemma [code_unfold]:
- "eq_class.eq xs [] \<longleftrightarrow> 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 \<inter> set ys"
-by (induct xs) auto
-
-lemma list_all_iff [code_post]:
- "list_all P xs \<longleftrightarrow> (\<forall>x \<in> 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) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
-by (induct xs) auto
-
-lemma list_all_rev [simp]:
- "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
-by (simp add: list_all_iff)
-
-lemma list_all_length:
- "list_all P xs \<longleftrightarrow> (\<forall>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 \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
-by (simp add: list_all_iff)
-
-lemma list_ex_iff [code_post]:
- "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> 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 \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
-unfolding list_ex_iff set_conv_nth by auto
-
-lemma list_ex_cong[fundef_cong]:
- "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
-by (simp add: list_ex_iff)
-
-lemma filtermap_conv:
- "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> 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..<Suc n]"
-by auto
-
-lemma atLeast_upt [code_unfold]:
- "{..<n} = set [0..<n]"
-by auto
-
-lemma greaterThanLessThan_upt [code_unfold]:
- "{n<..<m} = set [Suc n..<m]"
-by auto
-
-lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
-
-lemma greaterThanAtMost_upt [code_unfold]:
- "{n<..m} = set [Suc n..<Suc m]"
-by auto
-
-lemma atLeastAtMost_upt [code_unfold]:
- "{n..m} = set [n..<Suc m]"
-by auto
-
-lemma all_nat_less_eq [code_unfold]:
- "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
-by auto
-
-lemma ex_nat_less_eq [code_unfold]:
- "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
-by auto
-
-lemma all_nat_less [code_unfold]:
- "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
-by auto
-
-lemma ex_nat_less [code_unfold]:
- "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
-by auto
-
-lemma setsum_set_distinct_conv_listsum:
- "distinct xs \<Longrightarrow> 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..<n]) = listsum (map f [m..<n])"
-by (rule setsum_set_distinct_conv_listsum) simp
-
-text {* General equivalence between @{const listsum} and @{const setsum} *}
-lemma listsum_setsum_nth:
- "listsum xs = (\<Sum> 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<..<j::int} = set [i+1..j - 1]"
-by auto
-
-lemma atLeastLessThan_upto [code_unfold]:
- "{i..<j::int} = set [i..j - 1]"
-by auto
-
-lemma greaterThanAtMost_upto [code_unfold]:
- "{i<..j::int} = set [i+1..j]"
-by auto
-
-lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
-
-lemma setsum_set_upto_conv_listsum [code_unfold]:
- "setsum f (set [i..j::int]) = listsum (map f [i..j])"
-by (rule setsum_set_distinct_conv_listsum) simp
-
-
-text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
-and similiarly for @{text"\<exists>"}. *}
-
-function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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..<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_nat.simps)
- qed
-qed
-
-
-lemma list_all_iff_all_from_to_nat[code_unfold]:
- "list_all P [i..<j] = all_from_to_nat P i j"
-by(simp add: all_from_to_nat_iff_ball list_all_iff)
-
-lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
- "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
-by(simp add: all_from_to_nat_iff_ball list_ex_iff)
-
-
-function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 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
--- 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] \<Rightarrow> bool" where
- "is_target step phi pc' \<equiv>
- \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
+ "is_target step phi pc' \<longleftrightarrow>
+ (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))"
definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where
- "make_cert step phi B \<equiv>
+ "make_cert step phi B =
map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
lemma [code]:
"is_target step phi pc' =
- list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
-by (force simp: list_ex_iff is_target_def mem_iff)
+ list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]"
+by (force simp: list_ex_iff member_def is_target_def)
locale lbvc = lbv +
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Jun 29 11:29:31 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Jun 29 11:38:51 2010 +0200
@@ -323,7 +323,7 @@
let val VarAbs = Syntax.variant_abs(s,tp,trm);
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
end
- | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
+ | get_decls sign Clist ((Const (@{const_name prod_case}, _)) $ trm) = get_decls sign Clist trm
| get_decls sign Clist trm = (Clist,trm);
fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
@@ -389,7 +389,7 @@
val t2 = t1 $ ParamDeclTerm
in t2 end;
-fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
+fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name prod_case}, _) $ _)) = true
| is_fundef (Const("==", _) $ _ $ Abs _) = true
| is_fundef _ = false;
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jun 29 11:29:31 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jun 29 11:38:51 2010 +0200
@@ -707,7 +707,7 @@
case False
have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
- also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
+ also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by (auto simp add: inner_diff_left)
also have "\<dots> \<le> 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
--- 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 "\<bullet>" 70) where "x \<bullet> y \<equiv> inner x y"
+notation inner (infix "\<bullet>" 70)
subsection {* A connectedness or intermediate value lemma with several applications. *}
@@ -466,8 +466,8 @@
"orthogonal x a \<Longrightarrow> orthogonal (-x) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> 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 \<longleftrightarrow> orthogonal y x"
--- 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
--- 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 "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
by auto
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
by auto
lemma "split (curry f) = f"
@@ -61,12 +61,12 @@
by auto
lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
apply (rule ext)+
by auto
lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
apply (rule ext)+
by auto
--- 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}. ~(n dvd p)))"
-apply(simp add: Ball_def)
+lemma prime_nat_code [code]:
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+apply (simp add: Ball_def)
apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
done
lemma prime_nat_simp:
- "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
-apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
-apply(simp add:nat_number One_nat_def)
-done
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> 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}. ~(n dvd p)))" (is "?L = ?R")
+lemma prime_int_code [code]:
+ "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
proof
assume "?L" thus "?R"
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
@@ -232,12 +230,10 @@
qed
lemma prime_int_simp:
- "prime(p::int) = (p > 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) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> 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
--- 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 \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" by (auto simp add: primefact_def list_all_iff)
+lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
+ by (auto simp add: primefact_def list_all_iff)
(* Variant of Lucas theorem. *)
--- 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
--- 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 \<in> BB i j"
by blast
thus "\<exists>i. x \<in> 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 \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
--- 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 \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- split_prod_case: "split == prod_case"
+abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+ "split \<equiv> 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 "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(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 \<equiv> split f"
- shows "CASE (a, b) \<equiv> 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 \<Longrightarrow> split f (a, b)"
by (rule split_conv [THEN iffD2])
@@ -430,11 +421,11 @@
by (rule split_conv [THEN iffD1])
lemma split_Pair [simp]: "(\<lambda>(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: "(\<lambda>(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 \<circ> 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 \<Longrightarrow> 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 \<in> split c p"
and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> 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 = (\<lambda>c p. c (fst p) (snd p))"
- unfolding split_prod_case prod_case_unfold ..
+ by (fact prod_case_unfold)
definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
"internal_split == split"
--- 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 *}
--- 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 \<approx> 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 \<approx> plus_int_raw j i"
- by (cases i, cases j) (simp)
-
-lemma plus_zero_raw:
- shows "plus_int_raw (0, 0) i \<approx> i"
- by (cases i) (simp)
-
-lemma plus_minus_zero_raw:
- shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
- by (cases i) (simp)
-
-lemma times_assoc_raw:
- shows "times_int_raw (times_int_raw i j) k \<approx> 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 \<approx> 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 \<approx> i"
- by (cases i) (simp)
-
-lemma times_plus_comm_raw:
- shows "times_int_raw (plus_int_raw i j) k \<approx> 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 "\<not> (0, 0) \<approx> ((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 \<noteq> (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 \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> 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 \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
- by (cases i, cases j, cases k) (simp)
-
-lemma le_cases_raw:
- shows "le_int_raw i j \<or> 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 \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
- by (lifting le_antisym_raw)
+ by (descending) (auto)
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
by (auto simp add: less_int_def dest: antisym)
show "i \<le> i"
- by (lifting le_refl_raw)
+ by (descending) (auto)
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
- by (lifting le_trans_raw)
+ by (descending) (auto)
show "i \<le> j \<or> j \<le> 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 \<Longrightarrow> 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 \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting le_plus_int_raw)
+ by (descending) (auto)
qed
abbreviation
@@ -296,7 +238,7 @@
fixes k::int
shows "0 < k \<Longrightarrow> \<exists>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 \<or> le_int_raw (0, 0) z"
- shows "(int_to_nat_raw w \<le> 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 \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
+ by (descending) (auto simp add: int_to_nat_raw_def)
end
--- 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 \<sim> 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 \<sim> NONCE n \<Longrightarrow> 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 \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> 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 \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> 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' \<Longrightarrow> 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 "\<not>(NONCE m \<sim> MPAIR X Y)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
theorem Nonce_neq_MPair [iff]:
shows "Nonce N \<noteq> 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 "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
theorem Crypt_Nonce_neq_Nonce:
shows "Crypt K (Nonce M) \<noteq> 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 "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
theorem Crypt2_Nonce_neq_Nonce:
shows "Crypt K (Crypt K' (Nonce M)) \<noteq> 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')"
--- 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)
--- 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
--- 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"]
--- 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
--- 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 *)
--- 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 *)
--- 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 =
--- 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
--- 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
--- 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",
--- 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)
--- 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) \<Longrightarrow>
+ (\<forall>n\<Colon>nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m\<Colon>nat. a !! m \<longleftrightarrow> m < size a \<and> 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)) &
--- 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 \<in> 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!).
--- 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
--- 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 (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
- "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
+ "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
consts gcd :: "nat * nat => nat"
recdef gcd "measure (\<lambda>(x, y). x + y)"
--- 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") *}
--- 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") *}
--- 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)