1109 |
1109 |
1110 (* The definition is total??? *) |
1110 (* The definition is total??? *) |
1111 definition |
1111 definition |
1112 "x IN p ==> (res_abstract p m x = m x)" |
1112 "x IN p ==> (res_abstract p m x = m x)" |
1113 |
1113 |
|
1114 print_theorems |
|
1115 thm res_abstract_def |
|
1116 |
|
1117 (*TODO*) |
|
1118 term "\<forall>x. x \<in> S \<longrightarrow> P x" |
|
1119 term "\<forall>x \<in> S. P x" |
|
1120 |
|
1121 |
1114 lemma "(res_forall (Respects ((op \<approx>) ===> (op =))) |
1122 lemma "(res_forall (Respects ((op \<approx>) ===> (op =))) |
1115 (((REP_fset ---> id) ---> id) |
1123 (((REP_fset ---> id) ---> id) |
1116 (((ABS_fset ---> id) ---> id) |
1124 (((ABS_fset ---> id) ---> id) |
1117 (\<lambda>P. |
1125 (\<lambda>P. |
1118 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1126 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1136 ((ABS_fset ---> id) |
1144 ((ABS_fset ---> id) |
1137 ((REP_fset ---> id) |
1145 ((REP_fset ---> id) |
1138 (\<lambda>l. |
1146 (\<lambda>l. |
1139 (ABS_fset ---> id) |
1147 (ABS_fset ---> id) |
1140 ((REP_fset ---> id) P) |
1148 ((REP_fset ---> id) P) |
1141 (REP_fset (ABS_fset l)))))))))" |
1149 (REP_fset (ABS_fset l))))))))) |
1142 term " (\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1150 |
|
1151 = res_forall (Respects ((op \<approx>) ===> (op =))) |
|
1152 (\<lambda>P. ((P []) \<and> (res_forall (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
|
1153 (res_forall (Respects (op \<approx>)) (\<lambda>l. P l)))" |
|
1154 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1143 thm LAMBDA_PRS1[symmetric] |
1155 thm LAMBDA_PRS1[symmetric] |
1144 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1156 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1145 apply (unfold res_forall_def) |
1157 apply (unfold res_forall_def) |
|
1158 apply (simp only: IN_RESPECTS) |
|
1159 apply (simp only:list_eq_refl) |
1146 apply (unfold id_def) |
1160 apply (unfold id_def) |
1147 apply (simp add: FUN_MAP_I) |
1161 (*apply (simp only: FUN_MAP_I)*) |
|
1162 apply (simp) |
|
1163 apply (simp only: QUOT_TYPE_I_fset.thm10) |
|
1164 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1165 |
|
1166 .. |
1148 apply (simp add:IN_RESPECTS) |
1167 apply (simp add:IN_RESPECTS) |
1149 apply (simp add: QUOT_TYPE_I_fset.thm10) |
1168 |
1150 apply (simp add:list_eq_refl) |
|
1151 |
1169 |
1152 |
1170 |
1153 |
1171 |
1154 apply (simp add: QUOT_TYPE_I_fset.R_trans2) |
1172 apply (simp add: QUOT_TYPE_I_fset.R_trans2) |
1155 |
1173 |