1100 |
1100 |
1101 term "f ---> g" |
1101 term "f ---> g" |
1102 term "f ===> g" |
1102 term "f ===> g" |
1103 |
1103 |
1104 definition |
1104 definition |
1105 "rfall p m = (\<forall>x. (p x \<longrightarrow> m x))" |
1105 "res_forall p m = (\<forall>x. (x \<in> p \<longrightarrow> m x))" |
1106 |
1106 |
1107 term "ABS_fset" |
1107 definition |
1108 term "I" |
1108 "res_exists p m = (\<exists>x. (x \<in> p \<and> m x))" |
1109 |
1109 |
1110 term "(REP_fset ---> I) ---> I" |
1110 (* The definition is total??? *) |
1111 lemma "rfall (Respects ((op \<approx>) ===> (op =))) |
1111 definition |
|
1112 "x IN p ==> (res_abstract p m x = m x)" |
|
1113 |
|
1114 lemma "(res_forall (Respects ((op \<approx>) ===> (op =))) |
1112 (((REP_fset ---> id) ---> id) |
1115 (((REP_fset ---> id) ---> id) |
1113 (((ABS_fset ---> id) ---> id) |
1116 (((ABS_fset ---> id) ---> id) |
1114 (\<lambda>P. |
1117 (\<lambda>P. |
1115 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1118 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1116 (REP_fset (ABS_fset [])) \<and> |
1119 (REP_fset (ABS_fset [])) \<and> |
1117 rfall (Respects (op \<approx>)) |
1120 res_forall (Respects (op \<approx>)) |
1118 ((ABS_fset ---> id) |
1121 ((ABS_fset ---> id) |
1119 ((REP_fset ---> id) |
1122 ((REP_fset ---> id) |
1120 (\<lambda>t. |
1123 (\<lambda>t. |
1121 ((ABS_fset ---> id) |
1124 ((ABS_fset ---> id) |
1122 ((REP_fset ---> id) P) |
1125 ((REP_fset ---> id) P) |
1123 (REP_fset (ABS_fset t))) --> |
1126 (REP_fset (ABS_fset t))) \<longrightarrow> |
1124 (!h. |
1127 (!h. |
1125 (ABS_fset ---> id) |
1128 (ABS_fset ---> id) |
1126 ((REP_fset ---> id) P) |
1129 ((REP_fset ---> id) P) |
1127 (REP_fset |
1130 (REP_fset |
1128 (ABS_fset |
1131 (ABS_fset |
1129 (h # |
1132 (h # |
1130 REP_fset |
1133 REP_fset |
1131 (ABS_fset t)))))))) --> |
1134 (ABS_fset t)))))))) \<longrightarrow> |
1132 rfall (Respects (op \<approx>)) |
1135 res_forall (Respects (op \<approx>)) |
1133 ((ABS_fset ---> id) |
1136 ((ABS_fset ---> id) |
1134 ((REP_fset ---> id) |
1137 ((REP_fset ---> id) |
1135 (\<lambda>l. |
1138 (\<lambda>l. |
1136 (ABS_fset ---> id) |
1139 (ABS_fset ---> id) |
1137 ((REP_fset ---> id) P) |
1140 ((REP_fset ---> id) P) |
1138 (REP_fset (ABS_fset l))))))))" |
1141 (REP_fset (ABS_fset l)))))))))" |
1139 |
1142 term " (\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1140 apply (unfold rfall_def) |
1143 thm LAMBDA_PRS1[symmetric] |
|
1144 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
|
1145 apply (unfold res_forall_def) |
1141 apply (unfold id_def) |
1146 apply (unfold id_def) |
1142 apply (simp add: FUN_MAP_I) |
1147 apply (simp add: FUN_MAP_I) |
|
1148 apply (simp add:IN_RESPECTS) |
1143 apply (simp add: QUOT_TYPE_I_fset.thm10) |
1149 apply (simp add: QUOT_TYPE_I_fset.thm10) |
1144 . |
1150 apply (simp add:list_eq_refl) |
|
1151 |
|
1152 |
|
1153 |
|
1154 apply (simp add: QUOT_TYPE_I_fset.R_trans2) |
|
1155 |
|
1156 apply (rule ext) |
|
1157 apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
1158 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} ) |
|
1159 apply (simp add:cons_preserves) |
|
1160 |
|
1161 |
1145 |
1162 |
1146 (*prove aaa: {* (Thm.term_of cgoal2) *} |
1163 (*prove aaa: {* (Thm.term_of cgoal2) *} |
1147 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1164 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1148 apply (atomize(full)) |
1165 apply (atomize(full)) |
1149 apply (tactic {* foo_tac' @{context} 1 *}) |
1166 apply (tactic {* foo_tac' @{context} 1 *}) |