37613

1 
theory Inductive_Predicate


2 
imports Setup


3 
begin


4 


5 
(*<*)

38441

6 
hide_const %invisible append

37613

7 

38441

8 
inductive %invisible append where

37613

9 
"append [] ys ys"

38811

10 
 "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"

38441

11 


12 
lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"


13 
by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)

37613

14 
(*>*)

38441

15 


16 
section {* Inductive Predicates \label{sec:inductive} *}


17 

37613

18 
text {*

38508

19 
The @{text "predicate compiler"} is an extension of the code generator

38441

20 
which turns inductive specifications into equational ones, from


21 
which in turn executable code can be generated. The mechanisms of


22 
this compiler are described in detail in


23 
\cite{BerghoferBulwahnHaftmann:2009:TPHOL}.


24 


25 
Consider the simple predicate @{const append} given by these two


26 
introduction rules:

37613

27 
*}

38441

28 


29 
text %quote {*


30 
@{thm append.intros(1)[of ys]} \\


31 
@{thm append.intros(2)[of xs ys zs x]}


32 
*}


33 

37613

34 
text {*

38441

35 
\noindent To invoke the compiler, simply use @{command_def "code_pred"}:

37613

36 
*}


37 

38441

38 
code_pred %quote append .


39 


40 
text {*


41 
\noindent The @{command "code_pred"} command takes the name of the


42 
inductive predicate and then you put a period to discharge a trivial


43 
correctness proof. The compiler infers possible modes for the


44 
predicate and produces the derived code equations. Modes annotate


45 
which (parts of the) arguments are to be taken as input, and which


46 
output. Modes are similar to types, but use the notation @{text "i"}


47 
for input and @{text "o"} for output.


48 


49 
For @{term "append"}, the compiler can infer the following modes:


50 
\begin{itemize}


51 
\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}


52 
\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}


53 
\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}


54 
\end{itemize}


55 
You can compute sets of predicates using @{command_def "values"}:


56 
*}


57 


58 
values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"


59 


60 
text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}


61 


62 
values %quote "{(xs, ys). append xs ys [(2::nat),3]}"


63 


64 
text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}

37613

65 


66 
text {*

38441

67 
\noindent If you are only interested in the first elements of the


68 
set comprehension (with respect to a depthfirst search on the


69 
introduction rules), you can pass an argument to @{command "values"}


70 
to specify the number of elements you want:


71 
*}

37613

72 

38441

73 
values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"


74 
values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"


75 

37613

76 
text {*

38441

77 
\noindent The @{command "values"} command can only compute set


78 
comprehensions for which a mode has been inferred.


79 


80 
The code equations for a predicate are made available as theorems with


81 
the suffix @{text "equation"}, and can be inspected with:

37613

82 
*}

38441

83 


84 
thm %quote append.equation


85 


86 
text {*


87 
\noindent More advanced options are described in the following subsections.


88 
*}


89 


90 
subsection {* Alternative names for functions *}


91 

37613

92 
text {*

38441

93 
By default, the functions generated from a predicate are named after


94 
the predicate with the mode mangled into the name (e.g., @{text


95 
"append_i_i_o"}). You can specify your own names as follows:

37613

96 
*}

38441

97 

38811

98 
code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,


99 
o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,


100 
i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .

37613

101 

38441

102 
subsection {* Alternative introduction rules *}


103 

37613

104 
text {*

38441

105 
Sometimes the introduction rules of an predicate are not executable


106 
because they contain nonexecutable constants or specific modes


107 
could not be inferred. It is also possible that the introduction


108 
rules yield a function that loops forever due to the execution in a


109 
depthfirst search manner. Therefore, you can declare alternative


110 
introduction rules for predicates with the attribute @{attribute


111 
"code_pred_intro"}. For example, the transitive closure is defined


112 
by:

37613

113 
*}

38441

114 

37613

115 
text %quote {*

38441

116 
@{thm tranclp.intros(1)[of r a b]} \\


117 
@{thm tranclp.intros(2)[of r a b c]}

37613

118 
*}

38441

119 

37613

120 
text {*

38441

121 
\noindent These rules do not suit well for executing the transitive


122 
closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as


123 
the second rule will cause an infinite loop in the recursive call.


124 
This can be avoided using the following alternative rules which are


125 
declared to the predicate compiler by the attribute @{attribute


126 
"code_pred_intro"}:

37613

127 
*}

38441

128 

37613

129 
lemma %quote [code_pred_intro]:


130 
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"


131 
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"


132 
by auto

38441

133 

37613

134 
text {*

38441

135 
\noindent After declaring all alternative rules for the transitive


136 
closure, you invoke @{command "code_pred"} as usual. As you have


137 
declared alternative rules for the predicate, you are urged to prove


138 
that these introduction rules are complete, i.e., that you can


139 
derive an elimination rule for the alternative rules:

37613

140 
*}

38441

141 

37613

142 
code_pred %quote tranclp


143 
proof 


144 
case tranclp

38441

145 
from this converse_tranclpE [OF this(1)] show thesis by metis

37613

146 
qed

38441

147 

37613

148 
text {*

38441

149 
\noindent Alternative rules can also be used for constants that have


150 
not been defined inductively. For example, the lexicographic order


151 
which is defined as:

37613

152 
*}

38441

153 


154 
text %quote {*


155 
@{thm [display] lexord_def[of "r"]}

37613

156 
*}

38441

157 


158 
text {*


159 
\noindent To make it executable, you can derive the following two


160 
rules and prove the elimination rule:


161 
*}


162 

37613

163 
lemma %quote [code_pred_intro]:


164 
"append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"


165 
(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)


166 


167 
lemma %quote [code_pred_intro]:


168 
"append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)


169 
\<Longrightarrow> lexord r (xs, ys)"


170 
(*<*)unfolding lexord_def Collect_def append mem_def apply simp

38441

171 
apply (rule disjI2) by auto(*>*)

37613

172 


173 
code_pred %quote lexord

38441

174 
(*<*)proof 

37613

175 
fix r xs ys


176 
assume lexord: "lexord r (xs, ys)"


177 
assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"


178 
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"


179 
{


180 
assume "\<exists>a v. ys = xs @ a # v"


181 
from this 1 have thesis


182 
by (fastsimp simp add: append)


183 
} moreover


184 
{


185 
assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"


186 
from this 2 have thesis by (fastsimp simp add: append mem_def)


187 
} moreover


188 
note lexord


189 
ultimately show thesis


190 
unfolding lexord_def


191 
by (fastsimp simp add: Collect_def)

38441

192 
qed(*>*)


193 


194 


195 
subsection {* Options for values *}


196 

37613

197 
text {*

38441

198 
In the presence of higherorder predicates, multiple modes for some


199 
predicate could be inferred that are not disambiguated by the


200 
pattern of the set comprehension. To disambiguate the modes for the


201 
arguments of a predicate, you can state the modes explicitly in the


202 
@{command "values"} command. Consider the simple predicate @{term


203 
"succ"}:

37613

204 
*}

38441

205 


206 
inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where

37613

207 
"succ 0 (Suc 0)"


208 
 "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"


209 

38441

210 
code_pred %quote succ .

37613

211 


212 
text {*

38441

213 
\noindent For this, the predicate compiler can infer modes @{text "o


214 
\<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and


215 
@{text "i \<Rightarrow> i \<Rightarrow> bool"}. The invocation of @{command "values"}


216 
@{text "{n. tranclp succ 10 n}"} loops, as multiple modes for the


217 
predicate @{text "succ"} are possible and here the first mode @{text


218 
"o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,


219 
you can declare the mode for the argument between the @{command


220 
"values"} and the number of elements.

37613

221 
*}

38441

222 

39065

223 
values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)


224 
values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"

37613

225 

38441

226 


227 
subsection {* Embedding into functional code within Isabelle/HOL *}


228 

37613

229 
text {*

38441

230 
To embed the computation of an inductive predicate into functions


231 
that are defined in Isabelle/HOL, you have a number of options:


232 


233 
\begin{itemize}


234 


235 
\item You want to use the firstorder predicate with the mode


236 
where all arguments are input. Then you can use the predicate directly, e.g.


237 


238 
\begin{quote}


239 
@{text "valid_suffix ys zs = "} \\


240 
@{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}


241 
\end{quote}


242 


243 
\item If you know that the execution returns only one value (it is


244 
deterministic), then you can use the combinator @{term


245 
"Predicate.the"}, e.g., a functional concatenation of lists is


246 
defined with


247 


248 
\begin{quote}


249 
@{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}


250 
\end{quote}


251 


252 
Note that if the evaluation does not return a unique value, it


253 
raises a runtime error @{term "not_unique"}.


254 


255 
\end{itemize}

37613

256 
*}

38441

257 


258 


259 
subsection {* Further Examples *}


260 


261 
text {*


262 
Further examples for compiling inductive predicates can be found in


263 
the @{text "HOL/ex/Predicate_Compile_ex,thy"} theory file. There are


264 
also some examples in the Archive of Formal Proofs, notably in the


265 
@{text "POPLmarkdeBruijn"} and the @{text "FeatherweightJava"}


266 
sessions.

37613

267 
*}

38441

268 

37613

269 
end
