68 THEN' simp_tac (put_simpset HOL_basic_ss ctxt |
68 THEN' simp_tac (put_simpset HOL_basic_ss ctxt |
69 addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms}) |
69 addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms}) |
70 THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) |
70 THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) |
71 THEN' SUBGOAL (fn (g, i) => |
71 THEN' SUBGOAL (fn (g, i) => |
72 let |
72 let |
73 val thy = Proof_Context.theory_of ctxt |
|
74 (* Transform the term*) |
73 (* Transform the term*) |
75 val (t,np,nh) = prepare_for_mir q g |
74 val (t,np,nh) = prepare_for_mir q g |
76 (* Some simpsets for dealing with mod div abs and nat*) |
75 (* Some simpsets for dealing with mod div abs and nat*) |
77 val mod_div_simpset = put_simpset HOL_basic_ss ctxt |
76 val mod_div_simpset = put_simpset HOL_basic_ss ctxt |
78 addsimps [refl, mod_add_eq, |
77 addsimps [refl, mod_add_eq, |
99 val simpset2 = put_simpset HOL_basic_ss ctxt |
98 val simpset2 = put_simpset HOL_basic_ss ctxt |
100 addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral}, |
99 addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral}, |
101 @{thm "int_0"}, @{thm "int_1"}] |
100 @{thm "int_0"}, @{thm "int_1"}] |
102 |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] |
101 |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] |
103 (* simp rules for elimination of abs *) |
102 (* simp rules for elimination of abs *) |
104 val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t) |
103 val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) |
105 (* Theorem for the nat --> int transformation *) |
104 (* Theorem for the nat --> int transformation *) |
106 val pre_thm = Seq.hd (EVERY |
105 val pre_thm = Seq.hd (EVERY |
107 [simp_tac mod_div_simpset 1, simp_tac simpset0 1, |
106 [simp_tac mod_div_simpset 1, simp_tac simpset0 1, |
108 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |
107 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |
109 TRY (simp_tac (put_simpset mir_ss ctxt) 1)] |
108 TRY (simp_tac (put_simpset mir_ss ctxt) 1)] |
114 case Thm.prop_of pre_thm of |
113 case Thm.prop_of pre_thm of |
115 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
114 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
116 let val pth = |
115 let val pth = |
117 (* If quick_and_dirty then run without proof generation as oracle*) |
116 (* If quick_and_dirty then run without proof generation as oracle*) |
118 if Config.get ctxt quick_and_dirty |
117 if Config.get ctxt quick_and_dirty |
119 then mirfr_oracle (false, Thm.global_cterm_of thy (Envir.eta_long [] t1)) |
118 then mirfr_oracle (false, Thm.cterm_of ctxt (Envir.eta_long [] t1)) |
120 else mirfr_oracle (true, Thm.global_cterm_of thy (Envir.eta_long [] t1)) |
119 else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1)) |
121 in |
120 in |
122 ((pth RS iffD2) RS pre_thm, |
121 ((pth RS iffD2) RS pre_thm, |
123 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
122 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
124 end |
123 end |
125 | _ => (pre_thm, assm_tac i) |
124 | _ => (pre_thm, assm_tac i) |