equal
deleted
inserted
replaced
110 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) |
110 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) |
111 (* The result of the quantifier elimination *) |
111 (* The result of the quantifier elimination *) |
112 val (th, tac) = |
112 val (th, tac) = |
113 case Thm.prop_of pre_thm of |
113 case Thm.prop_of pre_thm of |
114 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
114 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
115 let val pth = |
115 let |
116 (* If quick_and_dirty then run without proof generation as oracle*) |
116 val pth = mirfr_oracle (ctxt, Envir.eta_long [] t1) |
117 if Config.get ctxt quick_and_dirty |
|
118 then mirfr_oracle (false, Thm.cterm_of ctxt (Envir.eta_long [] t1)) |
|
119 else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1)) |
|
120 in |
117 in |
121 ((pth RS iffD2) RS pre_thm, |
118 ((pth RS iffD2) RS pre_thm, |
122 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
119 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
123 end |
120 end |
124 | _ => (pre_thm, assm_tac i) |
121 | _ => (pre_thm, assm_tac i) |