1136 Toplevel.program (fn () => |
1136 Toplevel.program (fn () => |
1137 cterm_of @{theory} goal |
1137 cterm_of @{theory} goal |
1138 ); |
1138 ); |
1139 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1139 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1140 *} |
1140 *} |
1141 ML {* @{term "\<exists>x. P x"} *} |
|
1142 |
|
1143 term "f ---> g" |
|
1144 term "f ===> g" |
|
1145 |
1141 |
1146 definition |
1142 definition |
1147 "res_forall p m = (\<forall>x. (x \<in> p \<longrightarrow> m x))" |
1143 "x IN p ==> (Babs p m x = m x)" |
1148 |
|
1149 definition |
|
1150 "res_exists p m = (\<exists>x. (x \<in> p \<and> m x))" |
|
1151 |
|
1152 (* The definition is total??? *) |
|
1153 definition |
|
1154 "x IN p ==> (res_abstract p m x = m x)" |
|
1155 |
1144 |
1156 print_theorems |
1145 print_theorems |
1157 thm res_abstract_def |
1146 thm Babs_def |
1158 |
1147 |
1159 (*TODO*) |
1148 lemma "(Ball (Respects ((op \<approx>) ===> (op =))) |
1160 term "\<forall>x. x \<in> S \<longrightarrow> P x" |
|
1161 term "\<forall>x \<in> S. P x" |
|
1162 |
|
1163 |
|
1164 lemma "(res_forall (Respects ((op \<approx>) ===> (op =))) |
|
1165 (((REP_fset ---> id) ---> id) |
1149 (((REP_fset ---> id) ---> id) |
1166 (((ABS_fset ---> id) ---> id) |
1150 (((ABS_fset ---> id) ---> id) |
1167 (\<lambda>P. |
1151 (\<lambda>P. |
1168 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1152 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1169 (REP_fset (ABS_fset [])) \<and> |
1153 (REP_fset (ABS_fset [])) \<and> |
1170 res_forall (Respects (op \<approx>)) |
1154 Ball (Respects (op \<approx>)) |
1171 ((ABS_fset ---> id) |
1155 ((ABS_fset ---> id) |
1172 ((REP_fset ---> id) |
1156 ((REP_fset ---> id) |
1173 (\<lambda>t. |
1157 (\<lambda>t. |
1174 ((ABS_fset ---> id) |
1158 ((ABS_fset ---> id) |
1175 ((REP_fset ---> id) P) |
1159 ((REP_fset ---> id) P) |
1180 (REP_fset |
1164 (REP_fset |
1181 (ABS_fset |
1165 (ABS_fset |
1182 (h # |
1166 (h # |
1183 REP_fset |
1167 REP_fset |
1184 (ABS_fset t)))))))) \<longrightarrow> |
1168 (ABS_fset t)))))))) \<longrightarrow> |
1185 res_forall (Respects (op \<approx>)) |
1169 Ball (Respects (op \<approx>)) |
1186 ((ABS_fset ---> id) |
1170 ((ABS_fset ---> id) |
1187 ((REP_fset ---> id) |
1171 ((REP_fset ---> id) |
1188 (\<lambda>l. |
1172 (\<lambda>l. |
1189 (ABS_fset ---> id) |
1173 (ABS_fset ---> id) |
1190 ((REP_fset ---> id) P) |
1174 ((REP_fset ---> id) P) |
1191 (REP_fset (ABS_fset l))))))))) |
1175 (REP_fset (ABS_fset l))))))))) |
1192 |
1176 |
1193 = res_forall (Respects ((op \<approx>) ===> (op =))) |
1177 = Ball (Respects ((op \<approx>) ===> (op =))) |
1194 (\<lambda>P. ((P []) \<and> (res_forall (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1178 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1195 (res_forall (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1179 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1196 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1180 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1197 thm LAMBDA_PRS1[symmetric] |
1181 thm LAMBDA_PRS1[symmetric] |
1198 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1182 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1199 apply (unfold res_forall_def) |
1183 apply (unfold Ball_def) |
1200 apply (simp only: IN_RESPECTS) |
1184 apply (simp only: IN_RESPECTS) |
1201 apply (simp only:list_eq_refl) |
1185 apply (simp only:list_eq_refl) |
1202 apply (unfold id_def) |
1186 apply (unfold id_def) |
1203 (*apply (simp only: FUN_MAP_I)*) |
1187 (*apply (simp only: FUN_MAP_I)*) |
1204 apply (simp) |
1188 apply (simp) |