60 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> |
60 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> |
61 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$> |
61 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$> |
62 \<Longrightarrow> pred ts"} |
62 \<Longrightarrow> pred ts"} |
63 \end{isabelle} |
63 \end{isabelle} |
64 |
64 |
65 For the purposes here, we will assume the @{text rules} have |
65 For the purposes here, we will assume the @{text rules} have this format and |
66 this format and omit any code that actually tests this. Therefore ``things'' |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |
67 can go horribly wrong, if the @{text "rules"} are not of this |
67 wrong, if the @{text "rules"} are not of this form.\footnote{FIXME: Exercise |
68 form.\footnote{FIXME: Exercise to test this format.} The @{text As} and |
68 to test this format.} The @{text As} and @{text Bs} in a @{text "rule"} |
69 @{text Bs} in a @{text "rule"} stand for formulae not involving the inductive |
69 stand for formulae not involving the inductive predicates @{text "preds"}; |
70 predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred |
70 the instances @{text "pred ss"} and @{text "pred ts"} can stand for |
71 ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and |
71 different predicates, like @{text "pred\<^isub>1 ss"} and @{text |
72 @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the |
72 "pred\<^isub>2 ts"}, in case mutual recursive predicates are defined; the |
73 arguments of these predicates. Every formula left of @{text [quotes] |
73 terms @{text ss} and @{text ts} are the arguments of these predicates. Every |
74 "\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified |
74 formula left of @{text [quotes] "\<Longrightarrow> pred ts"} is a premise of the rule. The |
75 variables @{text "xs"} are usually omitted in the user's input. The |
75 outermost quantified variables @{text "xs"} are usually omitted in the |
76 quantification for the variables @{text "ys"} is local with respect to |
76 user's input. The quantification for the variables @{text "ys"} is local |
77 one recursive premise and must be given. Some examples of @{text "rule"}s |
77 with respect to one recursive premise and must be given. Some examples of |
78 are |
78 @{text "rule"}s are |
|
79 |
79 |
80 |
80 @{thm [display] fresh_var[no_vars]} |
81 @{thm [display] fresh_var[no_vars]} |
81 |
82 |
82 which has only a single non-recursive premise, whereas |
83 which has only a single non-recursive premise, whereas |
83 |
84 |
157 and need to show |
158 and need to show |
158 |
159 |
159 @{text [display] "pred ts"} |
160 @{text [display] "pred ts"} |
160 |
161 |
161 In the last step we removed some quantifiers and moved the precondition @{text "orules"} |
162 In the last step we removed some quantifiers and moved the precondition @{text "orules"} |
162 into the assumtion. The @{text "orules"} stand for all introduction rules that are given |
163 into the assumption. The @{text "orules"} stand for all introduction rules that are given |
163 by the user. We apply the @{text orule} that corresponds to introduction rule we are |
164 by the user. We apply the @{text orule} that corresponds to introduction rule we are |
164 proving. After lifting to the meta-connectives, this introduction rule must necessarily |
165 proving. After transforming the object connectives into meta-connectives, this introduction |
165 be of the form |
166 rule must necessarily be of the form |
166 |
167 |
167 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
168 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
168 |
169 |
169 When we apply this rule we end up in the goal state where we have to prove |
170 When we apply this rule we end up in the goal state where we have to prove |
170 goals of the form |
171 goals of the form |