equal
deleted
inserted
replaced
68 @{thm [display] accpartI[no_vars]} |
68 @{thm [display] accpartI[no_vars]} |
69 |
69 |
70 has a single recursive premise that has a precondition. As usual all |
70 has a single recursive premise that has a precondition. As usual all |
71 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
71 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
72 |
72 |
73 The code of the inductive package falls roughly in tree parts: the first |
73 The output of the inductive package will be definitions for the predicates, |
74 deals with the definitions, the second with the induction principles and |
74 induction principles and introduction rules. For the definitions we need to have the |
75 the third with the introduction rules. |
75 @{text rules} in a form where the meta-quantifiers and meta-implications are |
76 |
76 replaced by their object logic equivalents. Therefore an @{text "orule"} is |
77 For the definitions we need to have the @{text rules} in a form where |
77 of the form |
78 the meta-quantifiers and meta-implications are replaced by their object |
|
79 logic equivalents. Therefore an @{text "orule"} is of the form |
|
80 |
78 |
81 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
79 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
82 |
80 |
83 A definition for the predicate @{text "pred"} has then the form |
81 A definition for the predicate @{text "pred"} has then the form |
84 |
82 |
109 |
107 |
110 This can be done by instantiating the @{text "\<forall>preds"}-quantification |
108 This can be done by instantiating the @{text "\<forall>preds"}-quantification |
111 with the @{text "Ps"}. Then we are done since we are left with a simple |
109 with the @{text "Ps"}. Then we are done since we are left with a simple |
112 identity. |
110 identity. |
113 |
111 |
114 Although the user declares introduction rules @{text rules}, they must |
112 Although the user declares the introduction rules @{text rules}, they must |
115 also be derived from the @{text defs}. These derivations are a bit involved. |
113 also be derived from the @{text defs}. These derivations are a bit involved. |
116 Assuming we want to prove the introduction rule |
114 Assuming we want to prove the introduction rule |
117 |
115 |
118 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
116 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
119 |
117 |
120 then we can have assumptions of the form |
118 then we have assumptions of the form |
121 |
119 |
122 \begin{isabelle} |
120 \begin{isabelle} |
123 (i)~~@{text "As"}\\ |
121 (i)~~@{text "As"}\\ |
124 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
122 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
125 \end{isabelle} |
123 \end{isabelle} |
141 @{text [display] "pred ts"} |
139 @{text [display] "pred ts"} |
142 |
140 |
143 In the last step we removed some quantifiers and moved the precondition @{text "orules"} |
141 In the last step we removed some quantifiers and moved the precondition @{text "orules"} |
144 into the assumtion. The @{text "orules"} stand for all introduction rules that are given |
142 into the assumtion. The @{text "orules"} stand for all introduction rules that are given |
145 by the user. We apply the @{text orule} that corresponds to introduction rule we are |
143 by the user. We apply the @{text orule} that corresponds to introduction rule we are |
146 proving. This introduction rule must necessarily be of the form |
144 proving. After lifting to the meta-connectives, this introduction rule must necessarily |
|
145 be of the form |
147 |
146 |
148 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
147 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
149 |
148 |
150 When we apply this rule we end up in the goal state where we have to prove |
149 When we apply this rule we end up in the goal state where we have to prove |
151 goals of the form |
150 goals of the form |
165 |
164 |
166 Instantiating the universal quantifiers and then resolving with the assumptions |
165 Instantiating the universal quantifiers and then resolving with the assumptions |
167 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
166 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
168 This completes the proof for introduction rules. |
167 This completes the proof for introduction rules. |
169 |
168 |
170 What remains is to implement the reasoning outlined in this section. We do this |
169 What remains is to implement in Isabelle the reasoning outlined in this section. |
171 next. For building testcases, we use the shorthands for |
170 We will describe the code in the next section. For building testcases, we use the shorthands for |
172 @{text "even/odd"}, @{term "fresh"} and @{term "accpart"} |
171 @{text "even/odd"}, @{term "fresh"} and @{term "accpart"} |
173 given in Figure~\ref{fig:shorthands}. |
172 defined in Figure~\ref{fig:shorthands}. |
174 *} |
173 *} |
175 |
174 |
176 |
175 |
177 text_raw{* |
176 text_raw{* |
178 \begin{figure}[p] |
177 \begin{figure}[p] |