@@ -566,22 +566,6 @@ Proof
566566 \\ first_assum (irule_at Any)
567567 \\ simp [v_ok_def])
568568 \\ Cases_on ‘∃cmp. op = FP_cmp cmp’ \\ gs []
569- >- (
570- rw [do_app_cases] \\ gs [SF SFY_ss]
571- \\ first_assum (irule_at Any)
572- \\ simp [Boolv_def]
573- \\ rw [v_ok_def])
574- \\ Cases_on ‘∃bop. op = Real_bop bop’ \\ gs []
575- >- (
576- rw [do_app_cases] \\ gs [SF SFY_ss]
577- \\ first_assum (irule_at Any)
578- \\ simp [v_ok_def])
579- \\ Cases_on ‘∃uop. op = Real_uop uop’ \\ gs []
580- >- (
581- rw [do_app_cases] \\ gs [SF SFY_ss]
582- \\ first_assum (irule_at Any)
583- \\ simp [v_ok_def])
584- \\ Cases_on ‘∃cmp. op = Real_cmp cmp’ \\ gs []
585569 >- (
586570 rw [do_app_cases] \\ gs [SF SFY_ss]
587571 \\ first_assum (irule_at Any)
@@ -647,11 +631,6 @@ Proof
647631 \\ first_assum (irule_at Any)
648632 \\ simp [v_ok_def])
649633 \\ Cases_on ‘op = FpToWord’ \\ gs[]
650- >- (
651- rw[do_app_cases] \\ gs [SF SFY_ss]
652- \\ first_assum (irule_at Any)
653- \\ simp [v_ok_def])
654- \\ Cases_on ‘op = RealFromFP’ \\ gs[]
655634 >- (
656635 rw[do_app_cases] \\ gs [SF SFY_ss]
657636 \\ first_assum (irule_at Any)
@@ -675,30 +654,6 @@ Proof
675654 \\ strip_tac \\ gs []
676655 \\ rpt CASE_TAC \\ gs []
677656 \\ first_assum (irule_at Any) \\ gs [])
678- >~ [‘Icing’] >- (
679- gvs [AllCaseEqs()]
680- \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]
681- \\ rename1 ‘EVERY (v_ok ctxt1)’
682- \\ qexists_tac ‘ctxt1’ \\ gs [astTheory.isFpBool_def]
683- \\ drule do_app_ok \\ gs []
684- \\ disch_then drule_all \\ simp []
685- \\ strip_tac \\ gs []
686- \\ rpt CASE_TAC \\ gs[do_fprw_def] \\ rveq
687- \\ first_assum (irule_at Any)
688- \\ gs [shift_fp_opts_def, Boolv_def,
689- CaseEqs[" option" " semanticPrimitives$result" " list" " v"
690- \\ rveq \\ gs[v_ok_def]
691- \\ COND_CASES_TAC \\ gs[v_ok_def])
692- >~ [‘Reals’] >- (
693- gvs [AllCaseEqs()]
694- \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]
695- \\ rename1 ‘EVERY (v_ok ctxt1)’
696- \\ qexists_tac ‘ctxt1’ \\ gs [shift_fp_opts_def]
697- \\ drule do_app_ok \\ gs []
698- \\ disch_then drule_all \\ simp []
699- \\ strip_tac \\ gs []
700- \\ rpt CASE_TAC \\ gs []
701- \\ first_assum (irule_at Any) \\ gs [])
702657QED
703658
704659Theorem evaluate_v_ok_Opapp:
@@ -889,125 +844,6 @@ Proof
889844 rw [evaluate_def]
890845QED
891846
892- Theorem STRING_TYPE_do_fpoptimise:
893- STRING_TYPE m v ⇒
894- do_fpoptimise annot [v] = [v]
895- Proof
896- Cases_on ‘m’
897- \\ gs[ml_translatorTheory.STRING_TYPE_def, do_fpoptimise_def]
898- QED
899-
900- Theorem LIST_TYPE_TYPE_TYPE_do_fpoptimise:
901- ∀ l v annot.
902- (∀ ty v. MEM ty l ⇒ TYPE_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]) ∧
903- LIST_TYPE TYPE_TYPE l v ⇒
904- do_fpoptimise annot [v] = [v]
905- Proof
906- Induct_on ‘l’ \\ rw[ml_translatorTheory.LIST_TYPE_def]
907- \\ gs [do_fpoptimise_def]
908- \\ last_x_assum irule \\ metis_tac[]
909- QED
910-
911- Theorem TYPE_TYPE_do_fpoptimise:
912- ∀ ty v. TYPE_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]
913- Proof
914- ho_match_mp_tac TYPE_TYPE_ind \\ rw[TYPE_TYPE_def]
915- \\ gs[do_fpoptimise_def]
916- \\ imp_res_tac STRING_TYPE_do_fpoptimise \\ gs[]
917- \\ drule LIST_TYPE_TYPE_TYPE_do_fpoptimise \\ gs[]
918- QED
919-
920- Theorem TERM_TYPE_do_fpoptimise:
921- ∀ v ty. TERM_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]
922- Proof
923- Induct_on ‘ty’ \\ rw[TERM_TYPE_def] \\ res_tac \\ gs[do_fpoptimise_def]
924- \\ imp_res_tac TYPE_TYPE_do_fpoptimise
925- \\ imp_res_tac STRING_TYPE_do_fpoptimise \\ gs []
926- QED
927-
928- Theorem LIST_TYPE_TERM_TYPE_do_fpoptimise:
929- ∀ l v annot. LIST_TYPE TERM_TYPE l v ⇒ do_fpoptimise annot [v] = [v]
930- Proof
931- Induct_on ‘l’ \\ gs[ml_translatorTheory.LIST_TYPE_def, do_fpoptimise_def]
932- \\ rpt strip_tac \\ rveq
933- \\ imp_res_tac TERM_TYPE_do_fpoptimise
934- \\ gs[do_fpoptimise_def]
935- QED
936-
937- Theorem THM_TYPE_do_fpoptimise:
938- ∀ v ty. THM_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]
939- Proof
940- Induct_on ‘ty’ \\ rw [THM_TYPE_def]
941- \\ imp_res_tac TERM_TYPE_do_fpoptimise
942- \\ imp_res_tac LIST_TYPE_TERM_TYPE_do_fpoptimise
943- \\ gs [do_fpoptimise_def]
944- QED
945-
946- Theorem inferred_do_fpoptimise:
947- ∀ ctxt v.
948- inferred ctxt v ⇒
949- ∀ xs vs annot.
950- v = Conv (SOME xs) vs ⇒
951- inferred ctxt (Conv (SOME xs) (do_fpoptimise annot vs))
952- Proof
953- ho_match_mp_tac inferred_ind \\ rw[]
954- >- gs[kernel_funs_def]
955- >- (imp_res_tac TYPE_TYPE_do_fpoptimise \\ gs [do_fpoptimise_def]
956- \\ gs[inferred_cases, SF SFY_ss])
957- >- (imp_res_tac TERM_TYPE_do_fpoptimise \\ gs [do_fpoptimise_def]
958- \\ gs [inferred_cases, SF SFY_ss])
959- >- (imp_res_tac THM_TYPE_do_fpoptimise \\ gs [do_fpoptimise_def]
960- \\ gs [inferred_cases, SF SFY_ss])
961- QED
962-
963- Theorem EVERY_v_ok_do_fpoptimise:
964- ∀ annot vs ctxt.
965- EVERY (v_ok ctxt) vs ⇒
966- EVERY (v_ok ctxt) (do_fpoptimise annot vs)
967- Proof
968- ho_match_mp_tac do_fpoptimise_ind \\ rpt conj_tac
969- \\ gs[do_fpoptimise_def, v_ok_def] \\ rpt strip_tac
970- \\ gs[] \\ Cases_on ‘st’ \\ gs[]
971- \\ imp_res_tac kernel_vals_Conv \\ simp[]
972- \\ qpat_x_assum ‘kernel_vals _ _’ $ assume_tac o SIMP_RULE std_ss [Once v_ok_cases]
973- \\ gs[]
974- >- (simp [Once v_ok_cases]
975- \\ drule inferred_do_fpoptimise \\ gs[])
976- \\ Cases_on ‘f’ \\ gs[do_partial_app_def, CaseEq" exp"
977- QED
978-
979- Theorem evaluate_v_ok_FpOptimise:
980- ^(get_goal " FpOptimise"
981- Proof
982- rw[evaluate_def] \\ gvs [AllCaseEqs()]
983- \\ ‘st with fp_state := st.fp_state = st’ by gs [state_component_equality]
984- \\ gvs []
985- >- (
986- last_x_assum drule \\ gs[safe_exp_def, state_ok_def]
987- \\ strip_tac \\ gs[]
988- \\ first_assum $ irule_at Any \\ gs[] \\ conj_tac
989- >- metis_tac[]
990- \\ irule EVERY_v_ok_do_fpoptimise \\ gs[])
991- >- (last_x_assum drule \\ gs[safe_exp_def, state_ok_def])
992- >- (
993- ‘state_ok ctxt (st with fp_state := st.fp_state with canOpt := FPScope annot)’
994- by (gs[state_ok_def] \\ metis_tac[])
995- \\ last_x_assum drule \\ gs[safe_exp_def]
996- \\ strip_tac \\ gs[]
997- \\ ‘state_ok ctxt'' (st' with fp_state := st'.fp_state with canOpt := st.fp_state.canOpt)’
998- by (gs[state_ok_def] \\ metis_tac[])
999- \\ first_assum $ irule_at Any \\ gs[]
1000- \\ irule EVERY_v_ok_do_fpoptimise \\ gs[])
1001- >- (
1002- ‘state_ok ctxt (st with fp_state := st.fp_state with canOpt := FPScope annot)’
1003- by (gs[state_ok_def] \\ metis_tac[])
1004- \\ last_x_assum drule \\ gs[safe_exp_def]
1005- \\ strip_tac \\ gs[]
1006- \\ Cases_on ‘e'’ \\ gs[]
1007- \\ first_assum $ irule_at Any \\ gs[]
1008- \\ gs[state_ok_def] \\ metis_tac[])
1009- QED
1010-
1011847Theorem evaluate_v_ok_pmatch_Nil:
1012848 ^(get_goal " []:(pat # exp) list"
1013849Proof
@@ -1215,7 +1051,6 @@ Proof
12151051 evaluate_v_ok_If, evaluate_v_ok_Mat,
12161052 evaluate_v_ok_Let, evaluate_v_ok_Letrec,
12171053 evaluate_v_ok_Tannot, evaluate_v_ok_Lannot,
1218- evaluate_v_ok_FpOptimise,
12191054 evaluate_v_ok_pmatch_Nil, evaluate_v_ok_pmatch_Cons,
12201055 evaluate_v_ok_decs_Nil, evaluate_v_ok_decs_Cons,
12211056 evaluate_v_ok_decs_Dlet, evaluate_v_ok_decs_Dletrec,
0 commit comments