1028 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1028 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1029 |
1029 |
1030 prove list_induct_tr: trm_r |
1030 prove list_induct_tr: trm_r |
1031 apply (atomize(full)) |
1031 apply (atomize(full)) |
1032 apply (simp only: id_def[symmetric]) |
1032 apply (simp only: id_def[symmetric]) |
1033 |
|
1034 (* APPLY_RSP_TAC *) |
1033 (* APPLY_RSP_TAC *) |
1035 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]} @{context} 1 *}) |
1034 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
1035 apply (rule FUN_QUOTIENT) |
|
1036 apply (rule FUN_QUOTIENT) |
|
1037 apply (rule QUOTIENT_fset) |
|
1038 apply (rule IDENTITY_QUOTIENT) |
|
1039 apply (rule IDENTITY_QUOTIENT) |
|
1040 apply (rule IDENTITY_QUOTIENT) |
1036 prefer 2 |
1041 prefer 2 |
1037 apply (rule IDENTITY_QUOTIENT) |
|
1038 prefer 3 |
|
1039 (* ABS_REP_RSP_TAC *) |
1042 (* ABS_REP_RSP_TAC *) |
1040 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]} @{context} 1 *}) |
1043 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1041 prefer 2 |
1044 apply (rule FUN_QUOTIENT) |
|
1045 apply (rule FUN_QUOTIENT) |
|
1046 apply (rule QUOTIENT_fset) |
|
1047 apply (rule IDENTITY_QUOTIENT) |
|
1048 apply (rule IDENTITY_QUOTIENT) |
1042 (* LAMBDA_RES_TAC *) |
1049 (* LAMBDA_RES_TAC *) |
1043 apply (simp only: FUN_REL.simps) |
1050 apply (simp only: FUN_REL.simps) |
1044 apply (rule allI) |
1051 apply (rule allI) |
1045 apply (rule allI) |
1052 apply (rule allI) |
1046 apply (rule impI) |
1053 apply (rule impI) |
1055 (* MK_COMB_TAC *) |
1062 (* MK_COMB_TAC *) |
1056 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1063 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1057 (* REFL_TAC *) |
1064 (* REFL_TAC *) |
1058 apply (simp) |
1065 apply (simp) |
1059 (* APPLY_RSP_TAC *) |
1066 (* APPLY_RSP_TAC *) |
1060 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1067 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1061 apply (rule QUOTIENT_fset) |
1068 apply (rule QUOTIENT_fset) |
1062 apply (rule IDENTITY_QUOTIENT) |
1069 apply (rule IDENTITY_QUOTIENT) |
1063 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1070 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1064 prefer 2 |
1071 apply (rule FUN_QUOTIENT) |
|
1072 apply (rule QUOTIENT_fset) |
|
1073 apply (rule IDENTITY_QUOTIENT) |
1065 apply (simp only: FUN_REL.simps) |
1074 apply (simp only: FUN_REL.simps) |
|
1075 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
|
1076 apply (rule QUOTIENT_fset) |
|
1077 (* MINE *) |
|
1078 apply (rule list_eq_refl ) |
|
1079 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
1080 apply (rule FUN_QUOTIENT) |
|
1081 apply (rule QUOTIENT_fset) |
|
1082 apply (rule IDENTITY_QUOTIENT) |
|
1083 apply (rule IDENTITY_QUOTIENT) |
|
1084 (* TODO don't know how to handle ho_respects *) |
1066 prefer 2 |
1085 prefer 2 |
1067 (* ABS_REP_RSP *) |
1086 (* ABS_REP_RSP *) |
1068 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1087 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1069 apply (rule QUOTIENT_fset) |
1088 apply (rule FUN_QUOTIENT) |
1070 (* MINE *) |
1089 apply (rule QUOTIENT_fset) |
1071 apply (rule list_eq_refl ) |
1090 apply (rule IDENTITY_QUOTIENT) |
1072 prefer 2 |
|
1073 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *}) |
|
1074 prefer 2 |
|
1075 apply (rule IDENTITY_QUOTIENT) |
|
1076 (* 2: ho_respects *) |
|
1077 prefer 3 |
|
1078 (* ABS_REP_RSP *) |
|
1079 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1080 prefer 2 |
|
1081 (* LAMBDA_RSP *) |
1091 (* LAMBDA_RSP *) |
1082 apply (simp only: FUN_REL.simps) |
1092 apply (simp only: FUN_REL.simps) |
1083 apply (rule allI) |
1093 apply (rule allI) |
1084 apply (rule allI) |
1094 apply (rule allI) |
1085 apply (rule impI) |
1095 apply (rule impI) |
1088 (* MK_COMB_TAC *) |
1098 (* MK_COMB_TAC *) |
1089 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1099 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1090 (* REFL_TAC *) |
1100 (* REFL_TAC *) |
1091 apply (simp) |
1101 apply (simp) |
1092 (* APPLY_RSP *) |
1102 (* APPLY_RSP *) |
1093 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1103 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1094 apply (rule QUOTIENT_fset) |
1104 apply (rule QUOTIENT_fset) |
1095 apply (rule IDENTITY_QUOTIENT) |
1105 apply (rule IDENTITY_QUOTIENT) |
1096 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1106 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1097 prefer 2 |
1107 apply (rule FUN_QUOTIENT) |
|
1108 apply (rule QUOTIENT_fset) |
|
1109 apply (rule IDENTITY_QUOTIENT) |
1098 (* MINE *) |
1110 (* MINE *) |
1099 apply (simp only: FUN_REL.simps) |
1111 apply (simp only: FUN_REL.simps) |
1100 prefer 2 |
1112 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1101 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
|
1102 apply (rule QUOTIENT_fset) |
1113 apply (rule QUOTIENT_fset) |
1103 (* FIRST_ASSUM MATCH_ACCEPT_TAC *) |
1114 (* FIRST_ASSUM MATCH_ACCEPT_TAC *) |
1104 apply (assumption) |
1115 apply (assumption) |
1105 prefer 2 |
|
1106 (* MK_COMB_TAC *) |
1116 (* MK_COMB_TAC *) |
1107 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1117 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1108 (* REFL_TAC *) |
1118 (* REFL_TAC *) |
1109 apply (simp) |
1119 apply (simp) |
1110 (* W(C (curry op THEN) (G... *) |
1120 (* W(C (curry op THEN) (G... *) |
1111 apply (rule ext) |
1121 apply (rule ext) |
1112 (* APPLY_RSP *) |
1122 (* APPLY_RSP *) |
1113 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1123 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1114 apply (rule QUOTIENT_fset) |
1124 apply (rule QUOTIENT_fset) |
1115 apply (rule IDENTITY_QUOTIENT) |
1125 apply (rule IDENTITY_QUOTIENT) |
1116 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1126 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1117 prefer 2 |
1127 apply (rule FUN_QUOTIENT) |
|
1128 apply (rule QUOTIENT_fset) |
|
1129 apply (rule IDENTITY_QUOTIENT) |
1118 apply (simp only: FUN_REL.simps) |
1130 apply (simp only: FUN_REL.simps) |
1119 prefer 2 |
1131 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1120 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
|
1121 apply (rule QUOTIENT_fset) |
1132 apply (rule QUOTIENT_fset) |
1122 (* APPLY_RSP *) |
1133 (* APPLY_RSP *) |
1123 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]} @{context} 1 *}) |
1134 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1124 apply (rule QUOTIENT_fset) |
1135 apply (rule QUOTIENT_fset) |
1125 apply (rule QUOTIENT_fset) |
1136 apply (rule QUOTIENT_fset) |
1126 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]} @{context} 1 *}) |
1137 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1127 apply (rule IDENTITY_QUOTIENT) |
1138 apply (rule IDENTITY_QUOTIENT) |
|
1139 apply (rule FUN_QUOTIENT) |
|
1140 apply (rule QUOTIENT_fset) |
|
1141 apply (rule QUOTIENT_fset) |
1128 (* CONS respects *) |
1142 (* CONS respects *) |
1129 prefer 2 |
|
1130 apply (simp add: FUN_REL.simps) |
1143 apply (simp add: FUN_REL.simps) |
1131 apply (rule allI) |
1144 apply (rule allI) |
1132 apply (rule allI) |
1145 apply (rule allI) |
1133 apply (rule allI) |
1146 apply (rule allI) |
1134 apply (rule impI) |
1147 apply (rule impI) |
1135 apply (rule cons_preserves) |
1148 apply (rule cons_preserves) |
1136 apply (assumption) |
1149 apply (assumption) |
|
1150 apply (simp) |
|
1151 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
|
1152 apply (rule QUOTIENT_fset) |
|
1153 apply (assumption) |
1137 prefer 2 |
1154 prefer 2 |
1138 apply (simp) |
1155 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
1156 apply (rule FUN_QUOTIENT) |
|
1157 apply (rule QUOTIENT_fset) |
|
1158 apply (rule IDENTITY_QUOTIENT) |
|
1159 apply (rule IDENTITY_QUOTIENT) |
1139 prefer 2 |
1160 prefer 2 |
1140 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1161 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1141 apply (rule QUOTIENT_fset) |
1162 apply (rule FUN_QUOTIENT) |
1142 apply (assumption) |
1163 apply (rule QUOTIENT_fset) |
1143 prefer 8 |
1164 apply (rule IDENTITY_QUOTIENT) |
1144 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =)" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *}) |
|
1145 prefer 2 |
|
1146 apply (rule IDENTITY_QUOTIENT) |
|
1147 prefer 3 |
|
1148 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1149 prefer 2 |
|
1150 sorry |
1165 sorry |
1151 |
1166 |
1152 prove list_induct_t: trm |
1167 prove list_induct_t: trm |
1153 apply (simp only: list_induct_tr[symmetric]) |
1168 apply (simp only: list_induct_tr[symmetric]) |
1154 apply (tactic {* rtac thm 1 *}) |
1169 apply (tactic {* rtac thm 1 *}) |