equal
deleted
inserted
replaced
1 theory Ind_Code |
1 theory Ind_Code |
2 imports "../Base" "../FirstSteps" Ind_General_Scheme |
2 imports "../Base" "../FirstSteps" Ind_Interface Ind_General_Scheme |
3 begin |
3 begin |
4 |
4 |
5 section {* The Gory Details\label{sec:code} *} |
5 section {* The Gory Details\label{sec:code} *} |
6 |
6 |
7 text {* |
7 text {* |
796 recursive premises have preconditions. The introduction rule |
796 recursive premises have preconditions. The introduction rule |
797 of the accessible part is such a rule. |
797 of the accessible part is such a rule. |
798 *} |
798 *} |
799 |
799 |
800 lemma accpartI: |
800 lemma accpartI: |
801 shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
801 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
802 apply(tactic {* expand_tac @{thms accpart_def} *}) |
802 apply(tactic {* expand_tac @{thms accpart_def} *}) |
803 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *}) |
803 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *}) |
804 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *}) |
804 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *}) |
805 |
805 |
806 txt {* |
806 txt {* |
877 With these two functions we can now also prove the introduction |
877 With these two functions we can now also prove the introduction |
878 rule for the accessible part. |
878 rule for the accessible part. |
879 *} |
879 *} |
880 |
880 |
881 lemma accpartI: |
881 lemma accpartI: |
882 shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
882 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
883 apply(tactic {* expand_tac @{thms accpart_def} *}) |
883 apply(tactic {* expand_tac @{thms accpart_def} *}) |
884 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *}) |
884 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *}) |
885 done |
885 done |
886 |
886 |
887 text {* |
887 text {* |
1056 (OuterParse.enum1 "|" |
1056 (OuterParse.enum1 "|" |
1057 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
1057 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
1058 |
1058 |
1059 ML{*val specification = |
1059 ML{*val specification = |
1060 spec_parser >> |
1060 spec_parser >> |
1061 (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*} |
1061 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*} |
1062 |
1062 |
1063 ML{*val _ = OuterSyntax.local_theory "simple_inductive" |
1063 ML{*val _ = OuterSyntax.local_theory "simple_inductive" |
1064 "define inductive predicates" |
1064 "define inductive predicates" |
1065 OuterKeyword.thy_decl specification*} |
1065 OuterKeyword.thy_decl specification*} |
1066 |
1066 |
1081 \item exercise about the test for the intro rules |
1081 \item exercise about the test for the intro rules |
1082 \end{itemize} |
1082 \end{itemize} |
1083 |
1083 |
1084 *} |
1084 *} |
1085 |
1085 |
|
1086 (* |
1086 simple_inductive |
1087 simple_inductive |
1087 Even and Odd |
1088 Even and Odd |
1088 where |
1089 where |
1089 Even0: "Even 0" |
1090 Even0: "Even 0" |
1090 | EvenS: "Odd n \<Longrightarrow> Even (Suc n)" |
1091 | EvenS: "Odd n \<Longrightarrow> Even (Suc n)" |
1098 thm Even.induct |
1099 thm Even.induct |
1099 thm Odd.induct |
1100 thm Odd.induct |
1100 |
1101 |
1101 thm Even_def |
1102 thm Even_def |
1102 thm Odd_def |
1103 thm Odd_def |
1103 |
1104 *) |
|
1105 |
|
1106 (* |
1104 text {* |
1107 text {* |
1105 Second, we want that the user can specify fixed parameters. |
1108 Second, we want that the user can specify fixed parameters. |
1106 Remember in the previous section we stated that the user can give the |
1109 Remember in the previous section we stated that the user can give the |
1107 specification for the transitive closure of a relation @{text R} as |
1110 specification for the transitive closure of a relation @{text R} as |
1108 *} |
1111 *} |
1109 |
1112 *) |
|
1113 |
|
1114 (* |
1110 simple_inductive |
1115 simple_inductive |
1111 trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
1116 trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
1112 where |
1117 where |
1113 base: "trcl\<iota>\<iota> R x x" |
1118 base: "trcl\<iota>\<iota> R x x" |
1114 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z" |
1119 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z" |
1115 |
1120 *) |
|
1121 |
|
1122 (* |
1116 text {* |
1123 text {* |
1117 Note that there is no locale given in this specification---the parameter |
1124 Note that there is no locale given in this specification---the parameter |
1118 @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but |
1125 @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but |
1119 stays fixed throughout the specification. The problem with this way of |
1126 stays fixed throughout the specification. The problem with this way of |
1120 stating the specification for the transitive closure is that it derives the |
1127 stating the specification for the transitive closure is that it derives the |
1130 \end{center} |
1137 \end{center} |
1131 |
1138 |
1132 But this does not correspond to the induction principle we derived by hand, which |
1139 But this does not correspond to the induction principle we derived by hand, which |
1133 was |
1140 was |
1134 |
1141 |
1135 \begin{center}\small |
1142 |
1136 \mprset{flushleft} |
1143 %\begin{center}\small |
1137 \mbox{\inferrule{ |
1144 %\mprset{flushleft} |
1138 @{thm_style prem1 trcl_induct[no_vars]}\\\\ |
1145 %\mbox{\inferrule{ |
1139 @{thm_style prem2 trcl_induct[no_vars]}\\\\ |
1146 % @ { thm_style prem1 trcl_induct[no_vars]}\\\\ |
1140 @{thm_style prem3 trcl_induct[no_vars]}} |
1147 % @ { thm_style prem2 trcl_induct[no_vars]}\\\\ |
1141 {@{thm_style concl trcl_induct[no_vars]}}} |
1148 % @ { thm_style prem3 trcl_induct[no_vars]}} |
1142 \end{center} |
1149 % {@ { thm_style concl trcl_induct[no_vars]}}} |
|
1150 %\end{center} |
1143 |
1151 |
1144 The difference is that in the one derived by hand the relation @{term R} is not |
1152 The difference is that in the one derived by hand the relation @{term R} is not |
1145 a parameter of the proposition @{term P} to be proved and it is also not universally |
1153 a parameter of the proposition @{term P} to be proved and it is also not universally |
1146 qunatified in the second and third premise. The point is that the parameter @{term R} |
1154 qunatified in the second and third premise. The point is that the parameter @{term R} |
1147 stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' |
1155 stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' |
1149 In order to recognise such parameters, we have to extend the specification |
1157 In order to recognise such parameters, we have to extend the specification |
1150 to include a mechanism to state fixed parameters. The user should be able |
1158 to include a mechanism to state fixed parameters. The user should be able |
1151 to write |
1159 to write |
1152 |
1160 |
1153 *} |
1161 *} |
1154 |
1162 *) |
1155 (* |
1163 (* |
1156 simple_inductive |
1164 simple_inductive |
1157 trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
1165 trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
1158 where |
1166 where |
1159 base: "trcl'' R x x" |
1167 base: "trcl'' R x x" |
1162 simple_inductive |
1170 simple_inductive |
1163 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
1171 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
1164 where |
1172 where |
1165 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
1173 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
1166 *) |
1174 *) |
1167 |
1175 (*<*)end(*>*) |
1168 end |
|