--- a/NEWS Fri Dec 16 18:12:48 2022 +0100
+++ b/NEWS Fri Dec 16 20:14:41 2022 +0100
@@ -30,6 +30,10 @@
irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
+ - Added predicates sym_on and symp_on and redefined sym and
+ symp to be abbreviations. Lemmas sym_def and symp_def are explicitly
+ provided for backward compatibility but their usage is discouraged.
+ Minor INCOMPATIBILITY.
- Added predicates antisym_on and antisymp_on and redefined antisym and
antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are
explicitly provided for backward compatibility but their usage is
@@ -75,6 +79,13 @@
preorder.reflp_on_ge[simp]
preorder.reflp_on_le[simp]
reflp_on_conversp[simp]
+ sym_onD
+ sym_onI
+ sym_on_subset
+ symp_onD
+ symp_onI
+ symp_on_subset
+ symp_on_sym_on_eq[pred_set_conv]
totalI
totalp_on_converse[simp]
totalp_on_singleton[simp]
--- a/src/Doc/Codegen/Introduction.thy Fri Dec 16 18:12:48 2022 +0100
+++ b/src/Doc/Codegen/Introduction.thy Fri Dec 16 20:14:41 2022 +0100
@@ -222,6 +222,9 @@
dramatically by applying refinement techniques, which are
introduced in \secref{sec:refinement}.
+ \item How to define partial functions such that code can be generated
+ is explained in \secref{sec:partial}.
+
\item Inductive predicates can be turned executable using an
extension of the code generator \secref{sec:inductive}.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Codegen/Partial_Functions.thy Fri Dec 16 20:14:41 2022 +0100
@@ -0,0 +1,255 @@
+theory Partial_Functions
+imports Main "HOL-Library.Monad_Syntax"
+begin
+
+section \<open>Partial Functions \label{sec:partial}\<close>
+
+text \<open>We demonstrate three approaches to defining executable partial recursive functions.
+The main points are the definitions of the functions and the inductive proofs about them.
+
+Our concrete example represents a typical termination problem: following a data structure that
+may contain cycles. We want to follow a mapping from \<open>nat\<close> to \<open>nat\<close> to the end
+(until we leave its domain). The mapping is represented by a list \<open>ns :: nat list\<close>
+that maps \<open>n\<close> to \<open>ns ! n\<close>.
+The details of the example are in some sense irrelevant but make the exposition more realistic.
+However, we hide most proofs or show only the characteristic opening.\<close>
+
+text \<open>The list representation of the mapping can be abstracted to a relation.
+The order @{term "(ns!n, n)"} is the order that @{const wf} expects.\<close>
+
+definition rel :: "nat list \<Rightarrow> (nat * nat) set" where
+"rel ns = set(zip ns [0..<length ns])"
+
+lemma finite_rel[simp]: "finite(rel ns)"
+(*<*)by(simp add: rel_def)(*>*)
+
+text \<open>This relation should be acyclic
+ to guarantee termination of the partial functions defined below.\<close>
+
+
+subsection \<open>Tail recursion\<close>
+
+text \<open>If a function is tail-recursive, an executable definition is easy:\<close>
+
+partial_function (tailrec) follow :: "nat list \<Rightarrow> nat \<Rightarrow> nat" where
+"follow ns n = (if n < length ns then follow ns (ns!n) else n)"
+
+text \<open>Informing the code generator:\<close>
+
+declare follow.simps[code]
+
+text \<open>Now @{const follow} is executable:\<close>
+
+value "follow [1,2,3] 0"
+
+text \<open>For proofs about @{const follow} we need a @{const wf} relation on @{term "(ns,n)"} pairs
+that decreases with each recursive call. The first component stays the same but must be acyclic.
+The second component must decrease w.r.t @{const rel}:\<close>
+
+definition "rel_follow = same_fst (acyclic o rel) rel"
+
+lemma wf_follow: "wf rel_follow"
+(*<*)
+by (auto intro: wf_same_fst simp: rel_follow_def finite_acyclic_wf)
+
+text \<open>A more explicit formulation of \<open>rel_follow\<close>:
+The first component stays the same but must be acyclic.
+The second component decreases w.r.t \<open>rel\<close>:\<close>
+
+lemma rel_follow_step:
+ "\<lbrakk> m < length ms; acyclic (rel ms) \<rbrakk> \<Longrightarrow> ((ms, ms ! m), (ms, m)) \<in> rel_follow"
+by(force simp: rel_follow_def rel_def in_set_zip)
+(*>*)
+
+text \<open>This is how you start an inductive proof about @{const follow} along @{const rel_follow}:\<close>
+
+lemma "acyclic(rel ms) \<Longrightarrow> follow ms m = n \<Longrightarrow> length ms \<le> n"
+proof (induction "(ms,m)" arbitrary: m n rule: wf_induct_rule[OF wf_follow])
+(*<*)
+ case 1
+ thus ?case using follow.simps rel_follow_step by fastforce
+qed
+(*>*)
+
+
+subsection \<open>Option\<close>
+
+text \<open>If the function is not tail-recursive, not all is lost: if we rewrite it to return an \<open>option\<close>
+type, it can still be defined. In this case @{term "Some x"} represents the result \<open>x\<close>
+and @{term None} represents represents nontermination.
+For example, counting the length of the chain represented by \<open>ns\<close> can be defined like this:\<close>
+
+partial_function (option) count :: "nat list \<Rightarrow> nat \<Rightarrow> nat option" where
+"count ns n
+= (if n < length ns then do {k \<leftarrow> count ns (ns!n); Some (k+1)} else Some 0)"
+
+text \<open>We use a Haskell-like \<open>do\<close> notation (import @{theory "HOL-Library.Monad_Syntax"})
+to abbreviate the clumsy explicit
+
+\noindent
+@{term "case count ns (ns!n) of Some k \<Rightarrow> Some(k+1) | None \<Rightarrow> None"}.
+
+\noindent
+The branch \<open>None \<Rightarrow> None\<close> represents the requirement
+that nontermination of a recursive call must lead to nontermination of the function.
+
+Now we can prove that @{const count} terminates for all acyclic maps:\<close>
+
+lemma "acyclic(rel ms) \<Longrightarrow> \<exists>k. count ms m = Some k"
+proof (induction "(ms,m)" arbitrary: ms m rule: wf_induct_rule[OF wf_follow])
+(*<*)
+ case 1
+ thus ?case
+ by (metis bind.bind_lunit count.simps rel_follow_step)
+qed
+(*>*)
+
+
+subsection \<open>Subtype\<close>
+
+text \<open>In this approach we define a new type that contains only elements on which the function
+in question terminates.
+In our example that is the subtype of all \<open>ns :: nat list\<close> such that @{term "rel ns"} is acyclic.
+Then @{const follow} can be defined as a total function on that subtype.\<close>
+
+text \<open>The subtype is not empty:\<close>
+
+lemma acyclic_rel_Nil: "acyclic(rel [])"
+(*<*)by (simp add: rel_def acyclic_def)(*>*)
+
+text \<open>Definition of subtype \<open>acyc\<close>:\<close>
+
+typedef acyc = "{ns. acyclic(rel ns)}"
+morphisms rep_acyc abs_acyc
+using acyclic_rel_Nil by auto
+
+text \<open>This defines two functions \<open>rep_acyc :: acyc \<Rightarrow> nat list\<close> and \<open>abs_acyc :: nat list \<Rightarrow> acyc\<close>.
+Function @{const abs_acyc} is only defined on acyclic lists and not executable for that reason.\<close>
+
+setup_lifting type_definition_acyc
+
+text \<open>This is how @{const follow} can be defined on @{typ acyc}:\<close>
+
+function follow2 :: "acyc \<Rightarrow> nat \<Rightarrow> nat" where
+"follow2 ac n
+= (let ns = rep_acyc ac in if n < length ns then follow2 ac (ns!n) else n)"
+by pat_completeness auto
+
+text \<open>Now we prepare for termination proof.
+ Relation \<open>rel_follow2\<close> is almost identical to @{const rel_follow}.\<close>
+
+definition "rel_follow2 = same_fst (acyclic o rel o rep_acyc) (rel o rep_acyc)"
+
+lemma wf_follow2: "wf rel_follow2"
+(*<*)
+by (auto intro: wf_same_fst simp add: rel_follow2_def finite_acyclic_wf)
+
+text \<open>A more explicit formulation of \<open>rel_follow2\<close>:\<close>
+
+lemma rel_follow2_step:
+ "\<lbrakk> ns = rep_acyc ac; m < length ns; acyclic (rel ns) \<rbrakk> \<Longrightarrow> ((ac, ns ! m), (ac, m)) \<in> rel_follow2"
+by(force simp add: rel_follow2_def rel_def in_set_zip)
+(*>*)
+
+text \<open>Here comes the actual termination proof:\<close>
+
+termination follow2
+proof
+ show "wf rel_follow2"
+(*<*) by (auto intro: wf_same_fst simp add: rel_follow2_def finite_acyclic_wf)(*>*)
+
+next
+ show "\<And>ac n ns. \<lbrakk> ns = rep_acyc ac; n < length ns \<rbrakk>
+ \<Longrightarrow> ((ac, ns ! n), (ac, n)) \<in> rel_follow2"
+(*<*) using rel_follow2_step rep_acyc by simp(*>*)
+
+qed
+
+text \<open>Inductive proofs about @{const follow2} can now simply use computation induction:\<close>
+
+lemma "follow2 ac m = n \<Longrightarrow> length (rep_acyc ac) \<le> n"
+proof (induction ac m arbitrary: n rule: follow2.induct)
+(*<*)
+ case 1
+ thus ?case by (metis (full_types) follow2.simps linorder_not_le)
+qed
+(*>*)
+
+text \<open>A complication with the subtype approach is that injection into the subtype
+(function \<open>abs_acyc\<close> in our example) is not executable. But to call @{const follow2},
+we need an argument of type \<open>acyc\<close> and we need to obtain it in an executable manner.
+There are two approaches.\<close>
+
+text \<open>In the first approach we check wellformedness (i.e. acyclicity) explicitly.
+This check needs to be executable (which @{const acyclic} and @{const rel} are).
+If the check fails, @{term "[]"} is returned (which is acyclic).\<close>
+
+lift_definition is_acyc :: "nat list \<Rightarrow> acyc" is
+ "\<lambda>ns. if acyclic(rel ns) then ns else []"
+(*<*)by (auto simp: acyclic_rel_Nil)(*>*)
+
+text \<open>This works because we can easily prove that for any \<open>ns\<close>,
+ the \<open>\<lambda>\<close>-term produces an acyclic list.
+But it requires the possibly expensive check @{prop "acyclic(rel ns)"}.\<close>
+
+definition "follow_test ns n = follow2 (is_acyc ns) n"
+
+text \<open>The relation is acyclic (a chain):\<close>
+
+value "follow_test [1,2,3] 1"
+
+text \<open>In the second approach, wellformedness of the argument is guaranteed by construction.
+In our example \<open>[1..<n+1]\<close> represents an acyclic chain \<open>i \<mapsto> i+1\<close>\<close>
+
+lemma acyclic_chain: "acyclic (rel [1..<n+1])"
+(*<*)
+apply(induction n)
+ apply (simp add: rel_def acyclic_def)
+apply (auto simp add: rel_def)
+by (metis atLeast_upt lessI lessThan_iff order_less_asym' rtranclE set_zip_rightD)
+(*>*)
+
+text \<open>\<close>
+lift_definition acyc_chain :: "nat \<Rightarrow> acyc" is "\<lambda>n. [1..<n+1]"
+(*<*)by (use acyclic_chain in auto)(*>*)
+
+text \<open>\<close>
+definition "follow_chain m n = follow2 (acyc_chain m) n"
+
+value "follow_chain 5 1"
+
+text \<open>The subtype approach requires neither tail-recursion nor \<open>option\<close> but you cannot easily modify
+arguments of the subtype except via existing functions on the subtype. Otherwise you need to inject
+some value into the subtype and that injection is not computable.
+\<close>
+(*<*)
+text \<open>The problem with subtypes: the Abs function must not be used explicitly.
+This can be avoided by using \<open>lift_definition\<close>. Example:\<close>
+
+typedef nat1 = "{n::nat. n > 0}"
+by auto
+print_theorems
+
+setup_lifting type_definition_nat1
+
+(* just boiler plate *)
+lift_definition mk1 :: "nat \<Rightarrow> nat1" is
+ "\<lambda>n. if n>0 then n else 1"
+by auto
+
+lift_definition g :: "nat1 \<Rightarrow> nat1" is
+"\<lambda>n. if n \<ge> 2 then n-1 else n"
+by auto
+print_theorems
+text \<open>This generates
+ \<open>g.rep_eq: Rep_nat1 (g x) = (if 2 \<le> Rep_nat1 x then Rep_nat1 x - 1 else Rep_nat1 x)\<close>
+which is acceptable as an abstract code eqn. The manual definition of
+ \<open>g n1 = (let n = Rep_nat1 n1 in if 2 \<le> n then Abs_nat1 (n - 1) else Abs_nat1 n)\<close>
+looks non-executable but \<open>g.rep_eq\<close> can be derived from it.\<close>
+
+value "g (mk1 3)"
+
+text \<open>However, this trick does not work when passing an Abs-term as an argument,
+eg in a recursive call, because the Abs-term is `hidden' by the function call.\<close>
+(*>*)
+end
\ No newline at end of file
--- a/src/Doc/Codegen/document/root.tex Fri Dec 16 18:12:48 2022 +0100
+++ b/src/Doc/Codegen/document/root.tex Fri Dec 16 20:14:41 2022 +0100
@@ -15,7 +15,7 @@
\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
+\author{\emph{Florian Haftmann}\\ with contributions by Lukas Bulwahn and Tobias Nipkow}
\begin{document}
@@ -35,6 +35,7 @@
\input{Introduction.tex}
\input{Foundations.tex}
\input{Refinement.tex}
+\input{Partial_Functions.tex}
\input{Inductive_Predicate.tex}
\input{Evaluation.tex}
\input{Computations.tex}
--- a/src/Doc/Functions/Functions.thy Fri Dec 16 18:12:48 2022 +0100
+++ b/src/Doc/Functions/Functions.thy Fri Dec 16 20:14:41 2022 +0100
@@ -750,7 +750,7 @@
termination by (relation "{}") simp
-section \<open>Partiality\<close>
+section \<open>Partiality \label{sec:partiality}\<close>
text \<open>
In HOL, all functions are total. A function \<^term>\<open>f\<close> applied to
--- a/src/Doc/Functions/document/intro.tex Fri Dec 16 18:12:48 2022 +0100
+++ b/src/Doc/Functions/document/intro.tex Fri Dec 16 20:14:41 2022 +0100
@@ -43,8 +43,6 @@
to existing principles.
-
-
The new \cmd{function} command, and its short form \cmd{fun} have mostly
replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
a few of technical issues around \cmd{recdef}, and allow definitions
@@ -52,6 +50,10 @@
In addition there is also the \cmd{partial\_function} command
(see \cite{isabelle-isar-ref}) that supports the definition of partial
-and tail recursive functions.
+and tail recursive functions. This command is particulary relevant if one wants to
+generate executable code. This is covered in detail in the Code Generation
+tutorial~\cite{Haftmann-codegen}.
+The approach to partial function presented in Section~\ref{sec:partiality}
+of this tutorial does not support code generation.
--- a/src/Doc/ROOT Fri Dec 16 18:12:48 2022 +0100
+++ b/src/Doc/ROOT Fri Dec 16 20:14:41 2022 +0100
@@ -26,6 +26,7 @@
Introduction
Foundations
Refinement
+ Partial_Functions
Inductive_Predicate
Evaluation
Computations
--- a/src/Doc/manual.bib Fri Dec 16 18:12:48 2022 +0100
+++ b/src/Doc/manual.bib Fri Dec 16 20:14:41 2022 +0100
@@ -827,6 +827,10 @@
%H
+@manual{Haftmann-codegen,author={Florian Haftmann},
+title={Code generation from {Isabelle/HOL} theories},
+note={\url{http://isabelle.in.tum.de/doc/codegen.pdf}}}
+
@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
title = {Data Refinement in {Isabelle/HOL}},
--- a/src/HOL/Relation.thy Fri Dec 16 18:12:48 2022 +0100
+++ b/src/HOL/Relation.thy Fri Dec 16 20:14:41 2022 +0100
@@ -361,20 +361,48 @@
subsubsection \<open>Symmetry\<close>
-definition sym :: "'a rel \<Rightarrow> bool"
- where "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
+definition sym_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+ "sym_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
+
+abbreviation sym :: "'a rel \<Rightarrow> bool" where
+ "sym \<equiv> sym_on UNIV"
+
+definition symp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "symp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. R x y \<longrightarrow> R y x)"
-definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)"
+abbreviation symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "symp \<equiv> symp_on UNIV"
+
+lemma sym_def[no_atp]: "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
+ by (simp add: sym_on_def)
+
+lemma symp_def[no_atp]: "symp R \<longleftrightarrow> (\<forall>x y. R x y \<longrightarrow> R y x)"
+ by (simp add: symp_on_def)
+
+text \<open>@{thm [source] sym_def} and @{thm [source] symp_def} are for backward compatibility.\<close>
-lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
- by (simp add: sym_def symp_def)
+lemma symp_on_sym_on_eq[pred_set_conv]: "symp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym_on A r"
+ by (simp add: sym_on_def symp_on_def)
+
+lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
+
+lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
+ by (auto simp: sym_on_def)
+
+lemma symp_on_subset: "symp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> symp_on B R"
+ by (auto simp: symp_on_def)
-lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
- by (unfold sym_def) iprover
+lemma sym_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r) \<Longrightarrow> sym_on A r"
+ by (simp add: sym_on_def)
+
+lemma symI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r) \<Longrightarrow> sym r"
+ by (simp add: sym_onI)
-lemma sympI [intro?]: "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
- by (fact symI [to_pred])
+lemma symp_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x) \<Longrightarrow> symp_on A R"
+ by (rule sym_onI[to_pred])
+
+lemma sympI [intro?]: "(\<And>x y. R x y \<Longrightarrow> R y x) \<Longrightarrow> symp R"
+ by (rule symI[to_pred])
lemma symE:
assumes "sym r" and "(b, a) \<in> r"
@@ -386,15 +414,17 @@
obtains "r a b"
using assms by (rule symE [to_pred])
-lemma symD [dest?]:
- assumes "sym r" and "(b, a) \<in> r"
- shows "(a, b) \<in> r"
- using assms by (rule symE)
+lemma sym_onD: "sym_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+ by (simp add: sym_on_def)
+
+lemma symD [dest?]: "sym r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+ by (simp add: sym_onD)
-lemma sympD [dest?]:
- assumes "symp r" and "r b a"
- shows "r a b"
- using assms by (rule symD [to_pred])
+lemma symp_onD: "symp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x"
+ by (rule sym_onD[to_pred])
+
+lemma sympD [dest?]: "symp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+ by (rule symD[to_pred])
lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
by (fast intro: symI elim: symE)
--- a/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 16 18:12:48 2022 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 16 20:14:41 2022 +0100
@@ -399,7 +399,7 @@
fun mk_pred name R =
Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
val mk_reflp = mk_pred \<^const_abbrev>\<open>reflp\<close>;
-val mk_symp = mk_pred \<^const_name>\<open>symp\<close>;
+val mk_symp = mk_pred \<^const_abbrev>\<open>symp\<close>;
val mk_transp = mk_pred \<^const_name>\<open>transp\<close>;
fun mk_trans thm1 thm2 = trans OF [thm1, thm2];