595 [ |
594 [ |
596 (strip_tac 1), |
595 (strip_tac 1), |
597 (rtac disjI1 1), |
596 (rtac disjI1 1), |
598 (rtac unique_void2 1) |
597 (rtac unique_void2 1) |
599 ]); |
598 ]); |
|
599 |
|
600 qed_goalw "flat_eq" Fix.thy [is_flat_def] |
|
601 "[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[ |
|
602 (cut_facts_tac prems 1), |
|
603 (fast_tac (HOL_cs addIs [refl_less]) 1)]); |
|
604 |
|
605 (* ------------------------------------------------------------------------ *) |
|
606 (* lemmata for improved admissibility introdution rule *) |
|
607 (* ------------------------------------------------------------------------ *) |
|
608 |
|
609 qed_goal "infinite_chain_adm_lemma" Porder.thy |
|
610 "[|is_chain Y; !i. P (Y i); \ |
|
611 \ (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\ |
|
612 \ |] ==> P (lub (range Y))" |
|
613 (fn prems => [ |
|
614 cut_facts_tac prems 1, |
|
615 case_tac "finite_chain Y" 1, |
|
616 eresolve_tac prems 2, atac 2, atac 2, |
|
617 rewtac finite_chain_def, |
|
618 safe_tac HOL_cs, |
|
619 etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]); |
|
620 |
|
621 qed_goal "increasing_chain_adm_lemma" Porder.thy |
|
622 "[|is_chain Y; !i. P (Y i); \ |
|
623 \ (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\ |
|
624 \ ==> P (lub (range Y))) |] ==> P (lub (range Y))" |
|
625 (fn prems => [ |
|
626 cut_facts_tac prems 1, |
|
627 etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1, |
|
628 rewtac finite_chain_def, |
|
629 safe_tac HOL_cs, |
|
630 etac swap 1, |
|
631 rewtac max_in_chain_def, |
|
632 resolve_tac prems 1, atac 1, atac 1, |
|
633 fast_tac (HOL_cs addDs [le_imp_less_or_eq] |
|
634 addEs [chain_mono RS mp]) 1]); |
|
635 |
|
636 qed_goalw "admI" Fix.thy [adm_def] |
|
637 "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\ |
|
638 \ ==> P(lub (range Y))) ==> adm P" |
|
639 (fn prems => [ |
|
640 strip_tac 1, |
|
641 etac increasing_chain_adm_lemma 1, atac 1, |
|
642 eresolve_tac prems 1, atac 1, atac 1]); |
|
643 |
600 |
644 |
601 (* ------------------------------------------------------------------------ *) |
645 (* ------------------------------------------------------------------------ *) |
602 (* continuous isomorphisms are strict *) |
646 (* continuous isomorphisms are strict *) |
603 (* a prove for embedding projection pairs is similar *) |
647 (* a prove for embedding projection pairs is similar *) |
604 (* ------------------------------------------------------------------------ *) |
648 (* ------------------------------------------------------------------------ *) |
898 |
942 |
899 (* ------------------------------------------------------------------------ *) |
943 (* ------------------------------------------------------------------------ *) |
900 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas *) |
944 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas *) |
901 (* ------------------------------------------------------------------------ *) |
945 (* ------------------------------------------------------------------------ *) |
902 |
946 |
903 qed_goal "adm_disj_lemma1" Pcpo.thy |
947 local |
904 "[| is_chain Y; !n.P (Y n) | Q(Y n)|]\ |
948 |
905 \ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))" |
949 val adm_disj_lemma1 = prove_goal Pcpo.thy |
|
950 "[| is_chain Y; !n.P (Y n) | Q(Y n)|]\ |
|
951 \ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))" |
906 (fn prems => |
952 (fn prems => |
907 [ |
953 [ |
908 (cut_facts_tac prems 1), |
954 (cut_facts_tac prems 1), |
909 (fast_tac HOL_cs 1) |
955 (fast_tac HOL_cs 1) |
910 ]); |
956 ]); |
911 |
957 |
912 qed_goal "adm_disj_lemma2" Fix.thy |
958 val adm_disj_lemma2 = prove_goal Fix.thy |
913 "[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\ |
959 "[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\ |
914 \ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))" |
960 \ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))" |
915 (fn prems => |
961 (fn prems => |
916 [ |
962 [ |
917 (cut_facts_tac prems 1), |
963 (cut_facts_tac prems 1), |
918 (etac exE 1), |
964 (etac exE 1), |
919 (etac conjE 1), |
965 (etac conjE 1), |
955 (Asm_simp_tac 1), |
1001 (Asm_simp_tac 1), |
956 (Asm_simp_tac 1), |
1002 (Asm_simp_tac 1), |
957 (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1) |
1003 (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1) |
958 ]); |
1004 ]); |
959 |
1005 |
960 qed_goal "adm_disj_lemma4" Fix.thy |
1006 val adm_disj_lemma4 = prove_goal Fix.thy |
961 "[| ! j. i < j --> Q(Y(j)) |] ==>\ |
1007 "[| ! j. i < j --> Q(Y(j)) |] ==>\ |
962 \ ! n. Q( if n < Suc i then Y(Suc i) else Y n)" |
1008 \ ! n. Q( if n < Suc i then Y(Suc i) else Y n)" |
963 (fn prems => |
1009 (fn prems => |
964 [ |
1010 [ |
965 (cut_facts_tac prems 1), |
1011 (cut_facts_tac prems 1), |
966 (rtac allI 1), |
1012 (rtac allI 1), |
967 (res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1), |
1013 (res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1), |
968 (res_inst_tac[("s","Y(Suc(i))"),("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1), |
1014 (res_inst_tac[("s","Y(Suc(i))"), |
|
1015 ("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1), |
969 (Asm_simp_tac 1), |
1016 (Asm_simp_tac 1), |
970 (etac allE 1), |
1017 (etac allE 1), |
971 (rtac mp 1), |
1018 (rtac mp 1), |
972 (atac 1), |
1019 (atac 1), |
973 (Asm_simp_tac 1), |
1020 (Asm_simp_tac 1), |
974 (res_inst_tac[("s","Y(n)"),("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1), |
1021 (res_inst_tac[("s","Y(n)"), |
|
1022 ("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1), |
975 (Asm_simp_tac 1), |
1023 (Asm_simp_tac 1), |
976 (hyp_subst_tac 1), |
1024 (hyp_subst_tac 1), |
977 (dtac spec 1), |
1025 (dtac spec 1), |
978 (rtac mp 1), |
1026 (rtac mp 1), |
979 (atac 1), |
1027 (atac 1), |
980 (Asm_simp_tac 1), |
1028 (Asm_simp_tac 1), |
981 (res_inst_tac [("s","Y(n)"),("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1), |
1029 (res_inst_tac [("s","Y(n)"), |
|
1030 ("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")]ssubst 1), |
982 (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1), |
1031 (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1), |
983 (rtac iffI 1), |
1032 (rtac iffI 1), |
984 (etac FalseE 2), |
1033 (etac FalseE 2), |
985 (rtac notE 1), |
1034 (rtac notE 1), |
986 (etac less_not_sym 1), |
1035 (etac less_not_sym 1), |
990 (rtac mp 1), |
1039 (rtac mp 1), |
991 (atac 1), |
1040 (atac 1), |
992 (etac Suc_lessD 1) |
1041 (etac Suc_lessD 1) |
993 ]); |
1042 ]); |
994 |
1043 |
995 qed_goal "adm_disj_lemma5" Fix.thy |
1044 val adm_disj_lemma5 = prove_goal Fix.thy |
996 "[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\ |
1045 "[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\ |
997 \ lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))" |
1046 \ lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))" |
998 (fn prems => |
1047 (fn prems => |
999 [ |
1048 [ |
1000 (cut_facts_tac prems 1), |
1049 (cut_facts_tac prems 1), |
1001 (rtac lub_equal2 1), |
1050 (rtac lub_equal2 1), |
1002 (atac 2), |
1051 (atac 2), |
1014 (atac 1), |
1063 (atac 1), |
1015 (rtac (if_False RS ssubst) 1), |
1064 (rtac (if_False RS ssubst) 1), |
1016 (rtac refl 1) |
1065 (rtac refl 1) |
1017 ]); |
1066 ]); |
1018 |
1067 |
1019 qed_goal "adm_disj_lemma6" Fix.thy |
1068 val adm_disj_lemma6 = prove_goal Fix.thy |
1020 "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\ |
1069 "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\ |
1021 \ ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))" |
1070 \ ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))" |
1022 (fn prems => |
1071 (fn prems => |
1023 [ |
1072 [ |
1024 (cut_facts_tac prems 1), |
1073 (cut_facts_tac prems 1), |
1025 (etac exE 1), |
1074 (etac exE 1), |
1026 (res_inst_tac [("x","%m.if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1), |
1075 (res_inst_tac [("x","%m.if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1), |
1034 (rtac adm_disj_lemma5 1), |
1083 (rtac adm_disj_lemma5 1), |
1035 (atac 1), |
1084 (atac 1), |
1036 (atac 1) |
1085 (atac 1) |
1037 ]); |
1086 ]); |
1038 |
1087 |
1039 |
1088 val adm_disj_lemma7 = prove_goal Fix.thy |
1040 qed_goal "adm_disj_lemma7" Fix.thy |
1089 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
1041 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
1090 \ is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))" |
1042 \ is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))" |
|
1043 (fn prems => |
1091 (fn prems => |
1044 [ |
1092 [ |
1045 (cut_facts_tac prems 1), |
1093 (cut_facts_tac prems 1), |
1046 (rtac is_chainI 1), |
1094 (rtac is_chainI 1), |
1047 (rtac allI 1), |
1095 (rtac allI 1), |
1058 (etac exE 1), |
1106 (etac exE 1), |
1059 (rtac (LeastI RS conjunct2) 1), |
1107 (rtac (LeastI RS conjunct2) 1), |
1060 (atac 1) |
1108 (atac 1) |
1061 ]); |
1109 ]); |
1062 |
1110 |
1063 qed_goal "adm_disj_lemma8" Fix.thy |
1111 val adm_disj_lemma8 = prove_goal Fix.thy |
1064 "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))" |
1112 "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))" |
1065 (fn prems => |
1113 (fn prems => |
1066 [ |
1114 [ |
1067 (cut_facts_tac prems 1), |
1115 (cut_facts_tac prems 1), |
1068 (strip_tac 1), |
1116 (strip_tac 1), |
1069 (etac allE 1), |
1117 (etac allE 1), |
1070 (etac exE 1), |
1118 (etac exE 1), |
1071 (etac (LeastI RS conjunct2) 1) |
1119 (etac (LeastI RS conjunct2) 1) |
1072 ]); |
1120 ]); |
1073 |
1121 |
1074 qed_goal "adm_disj_lemma9" Fix.thy |
1122 val adm_disj_lemma9 = prove_goal Fix.thy |
1075 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
1123 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
1076 \ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))" |
1124 \ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))" |
1077 (fn prems => |
1125 (fn prems => |
1078 [ |
1126 [ |
1079 (cut_facts_tac prems 1), |
1127 (cut_facts_tac prems 1), |
1080 (rtac antisym_less 1), |
1128 (rtac antisym_less 1), |
1081 (rtac lub_mono 1), |
1129 (rtac lub_mono 1), |
1100 (rtac (chain_mono RS mp) 1), |
1148 (rtac (chain_mono RS mp) 1), |
1101 (atac 1), |
1149 (atac 1), |
1102 (rtac lessI 1) |
1150 (rtac lessI 1) |
1103 ]); |
1151 ]); |
1104 |
1152 |
1105 qed_goal "adm_disj_lemma10" Fix.thy |
1153 val adm_disj_lemma10 = prove_goal Fix.thy |
1106 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
1154 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
1107 \ ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))" |
1155 \ ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))" |
1108 (fn prems => |
1156 (fn prems => |
1109 [ |
1157 [ |
1110 (cut_facts_tac prems 1), |
1158 (cut_facts_tac prems 1), |
1111 (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1), |
1159 (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1), |
1112 (rtac conjI 1), |
1160 (rtac conjI 1), |
1119 (rtac adm_disj_lemma9 1), |
1167 (rtac adm_disj_lemma9 1), |
1120 (atac 1), |
1168 (atac 1), |
1121 (atac 1) |
1169 (atac 1) |
1122 ]); |
1170 ]); |
1123 |
1171 |
1124 |
1172 val adm_disj_lemma12 = prove_goal Fix.thy |
1125 qed_goal "adm_disj_lemma11" Fix.thy |
1173 "[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))" |
|
1174 (fn prems => |
|
1175 [ |
|
1176 (cut_facts_tac prems 1), |
|
1177 (etac adm_disj_lemma2 1), |
|
1178 (etac adm_disj_lemma6 1), |
|
1179 (atac 1) |
|
1180 ]); |
|
1181 |
|
1182 in |
|
1183 |
|
1184 val adm_lemma11 = prove_goal Fix.thy |
1126 "[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))" |
1185 "[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))" |
1127 (fn prems => |
1186 (fn prems => |
1128 [ |
1187 [ |
1129 (cut_facts_tac prems 1), |
1188 (cut_facts_tac prems 1), |
1130 (etac adm_disj_lemma2 1), |
1189 (etac adm_disj_lemma2 1), |
1131 (etac adm_disj_lemma10 1), |
1190 (etac adm_disj_lemma10 1), |
1132 (atac 1) |
1191 (atac 1) |
1133 ]); |
1192 ]); |
1134 |
1193 |
1135 qed_goal "adm_disj_lemma12" Fix.thy |
1194 val adm_disj = prove_goal Fix.thy |
1136 "[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))" |
|
1137 (fn prems => |
|
1138 [ |
|
1139 (cut_facts_tac prems 1), |
|
1140 (etac adm_disj_lemma2 1), |
|
1141 (etac adm_disj_lemma6 1), |
|
1142 (atac 1) |
|
1143 ]); |
|
1144 |
|
1145 qed_goal "adm_disj" Fix.thy |
|
1146 "[| adm P; adm Q |] ==> adm(%x.P x | Q x)" |
1195 "[| adm P; adm Q |] ==> adm(%x.P x | Q x)" |
1147 (fn prems => |
1196 (fn prems => |
1148 [ |
1197 [ |
1149 (cut_facts_tac prems 1), |
1198 (cut_facts_tac prems 1), |
1150 (rtac (adm_def2 RS iffD2) 1), |
1199 (rtac (adm_def2 RS iffD2) 1), |
1155 (rtac disjI2 1), |
1204 (rtac disjI2 1), |
1156 (etac adm_disj_lemma12 1), |
1205 (etac adm_disj_lemma12 1), |
1157 (atac 1), |
1206 (atac 1), |
1158 (atac 1), |
1207 (atac 1), |
1159 (rtac disjI1 1), |
1208 (rtac disjI1 1), |
1160 (etac adm_disj_lemma11 1), |
1209 (etac adm_lemma11 1), |
1161 (atac 1), |
1210 (atac 1), |
1162 (atac 1) |
1211 (atac 1) |
1163 ]); |
1212 ]); |
1164 |
1213 |
|
1214 end; |
|
1215 |
|
1216 bind_thm("adm_lemma11",adm_lemma11); |
|
1217 bind_thm("adm_disj",adm_disj); |
1165 |
1218 |
1166 qed_goal "adm_imp" Fix.thy |
1219 qed_goal "adm_imp" Fix.thy |
1167 "[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)" |
1220 "[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)" |
1168 (fn prems => |
1221 (fn prems => |
1169 [ |
1222 [ |
1185 fast_tac HOL_cs 2, |
1237 fast_tac HOL_cs 2, |
1186 etac ssubst 1, |
1238 etac ssubst 1, |
1187 etac adm_disj 1, |
1239 etac adm_disj 1, |
1188 atac 1]); |
1240 atac 1]); |
1189 |
1241 |
1190 qed_goalw "admI" Fix.thy [adm_def] |
|
1191 "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\ |
|
1192 \ ==> P(lub (range Y))) ==> adm P" |
|
1193 (fn prems => [ |
|
1194 strip_tac 1, |
|
1195 case_tac "finite_chain Y" 1, |
|
1196 rewtac finite_chain_def, |
|
1197 safe_tac HOL_cs, |
|
1198 dtac lub_finch1 1, |
|
1199 atac 1, |
|
1200 dtac thelubI 1, |
|
1201 etac ssubst 1, |
|
1202 etac spec 1, |
|
1203 etac swap 1, |
|
1204 rewtac max_in_chain_def, |
|
1205 resolve_tac prems 1, atac 1, atac 1, |
|
1206 fast_tac (HOL_cs addDs [le_imp_less_or_eq] |
|
1207 addEs [chain_mono RS mp]) 1]); |
|
1208 |
|
1209 val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, |
1242 val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, |
1210 adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less |
1243 adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less]; |
1211 ]; |
1244 |
1212 |
|