equal
deleted
inserted
replaced
106 form |
106 form |
107 |
107 |
108 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"} |
108 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"} |
109 |
109 |
110 where in the @{text "rules"}-part every @{text pred} is replaced by a fresh |
110 where in the @{text "rules"}-part every @{text pred} is replaced by a fresh |
111 meta-variable @{text "?P"}. |
111 schematic variable @{text "?P"}. |
112 |
112 |
113 In order to derive an induction principle for the predicate @{text "pred"}, |
113 In order to derive an induction principle for the predicate @{text "pred"}, |
114 we first transform @{text ind} into the object logic and fix the meta-variables. |
114 we first transform @{text ind} into the object logic and fix the schematic variables. |
115 Hence we have to prove a formula of the form |
115 Hence we have to prove a formula of the form |
116 |
116 |
117 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"} |
117 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"} |
118 |
118 |
119 If we assume @{text "pred zs"} and unfold its definition, then we have an |
119 If we assume @{text "pred zs"} and unfold its definition, then we have an |