41 fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = |
41 fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = |
42 aux def t1 andalso aux false t2 |
42 aux def t1 andalso aux false t2 |
43 | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 |
43 | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 |
44 | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) = |
44 | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) = |
45 aux def t1 andalso aux false t2 |
45 aux def t1 andalso aux false t2 |
46 | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2 |
46 | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2 |
47 | aux def (t1 $ t2) = aux def t1 andalso aux def t2 |
47 | aux def (t1 $ t2) = aux def t1 andalso aux def t2 |
48 | aux def (t as Const (s, _)) = |
48 | aux def (t as Const (s, _)) = |
49 (not def orelse t <> @{const Suc}) andalso |
49 (not def orelse t <> @{const Suc}) andalso |
50 not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
50 not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
51 @{const_name nat_gcd}, @{const_name nat_lcm}, |
51 @{const_name nat_gcd}, @{const_name nat_lcm}, |
215 @{const "op &"} $ do_term new_Ts old_Ts polar t1 |
215 @{const "op &"} $ do_term new_Ts old_Ts polar t1 |
216 $ do_term new_Ts old_Ts polar t2 |
216 $ do_term new_Ts old_Ts polar t2 |
217 | @{const "op |"} $ t1 $ t2 => |
217 | @{const "op |"} $ t1 $ t2 => |
218 @{const "op |"} $ do_term new_Ts old_Ts polar t1 |
218 @{const "op |"} $ do_term new_Ts old_Ts polar t1 |
219 $ do_term new_Ts old_Ts polar t2 |
219 $ do_term new_Ts old_Ts polar t2 |
220 | @{const "op -->"} $ t1 $ t2 => |
220 | @{const HOL.implies} $ t1 $ t2 => |
221 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
221 @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
222 $ do_term new_Ts old_Ts polar t2 |
222 $ do_term new_Ts old_Ts polar t2 |
223 | Const (x as (s, T)) => |
223 | Const (x as (s, T)) => |
224 if is_descr s then |
224 if is_descr s then |
225 do_descr s T |
225 do_descr s T |
226 else |
226 else |
332 do_eq_or_imp Ts true def t0 t1 t2 seen |
332 do_eq_or_imp Ts true def t0 t1 t2 seen |
333 | (t0 as @{const "==>"}) $ t1 $ t2 => |
333 | (t0 as @{const "==>"}) $ t1 $ t2 => |
334 if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen |
334 if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen |
335 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 => |
335 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 => |
336 do_eq_or_imp Ts true def t0 t1 t2 seen |
336 do_eq_or_imp Ts true def t0 t1 t2 seen |
337 | (t0 as @{const "op -->"}) $ t1 $ t2 => |
337 | (t0 as @{const HOL.implies}) $ t1 $ t2 => |
338 do_eq_or_imp Ts false def t0 t1 t2 seen |
338 do_eq_or_imp Ts false def t0 t1 t2 seen |
339 | Abs (s, T, t') => |
339 | Abs (s, T, t') => |
340 let val (t', seen) = do_term (T :: Ts) def t' [] seen in |
340 let val (t', seen) = do_term (T :: Ts) def t' [] seen in |
341 (list_comb (Abs (s, T, t'), args), seen) |
341 (list_comb (Abs (s, T, t'), args), seen) |
342 end |
342 end |
399 aux_eq careful true t0 t1 t2 |
399 aux_eq careful true t0 t1 t2 |
400 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = |
400 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = |
401 t0 $ aux false t1 $ aux careful t2 |
401 t0 $ aux false t1 $ aux careful t2 |
402 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) = |
402 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) = |
403 aux_eq careful true t0 t1 t2 |
403 aux_eq careful true t0 t1 t2 |
404 | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) = |
404 | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) = |
405 t0 $ aux false t1 $ aux careful t2 |
405 t0 $ aux false t1 $ aux careful t2 |
406 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') |
406 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') |
407 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 |
407 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 |
408 | aux _ t = t |
408 | aux _ t = t |
409 and aux_eq careful pass1 t0 t1 t2 = |
409 and aux_eq careful pass1 t0 t1 t2 = |
606 do_quantifier s0 T0 s1 T1 t1 |
606 do_quantifier s0 T0 s1 T1 t1 |
607 | @{const "op &"} $ t1 $ t2 => |
607 | @{const "op &"} $ t1 $ t2 => |
608 s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) |
608 s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) |
609 | @{const "op |"} $ t1 $ t2 => |
609 | @{const "op |"} $ t1 $ t2 => |
610 s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) |
610 s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) |
611 | @{const "op -->"} $ t1 $ t2 => |
611 | @{const HOL.implies} $ t1 $ t2 => |
612 @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1 |
612 @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1 |
613 $ aux ss Ts js skolemizable polar t2 |
613 $ aux ss Ts js skolemizable polar t2 |
614 | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 => |
614 | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 => |
615 t0 $ t1 $ aux ss Ts js skolemizable polar t2 |
615 t0 $ t1 $ aux ss Ts js skolemizable polar t2 |
616 | Const (x as (s, T)) => |
616 | Const (x as (s, T)) => |
617 if is_real_inductive_pred hol_ctxt x andalso |
617 if is_real_inductive_pred hol_ctxt x andalso |
1119 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => |
1119 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => |
1120 (case distribute_quantifiers t1 of |
1120 (case distribute_quantifiers t1 of |
1121 (t10 as @{const "op |"}) $ t11 $ t12 => |
1121 (t10 as @{const "op |"}) $ t11 $ t12 => |
1122 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
1122 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
1123 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
1123 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
1124 | (t10 as @{const "op -->"}) $ t11 $ t12 => |
1124 | (t10 as @{const HOL.implies}) $ t11 $ t12 => |
1125 t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
1125 t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
1126 $ Abs (s, T1, t11)) |
1126 $ Abs (s, T1, t11)) |
1127 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
1127 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
1128 | (t10 as @{const Not}) $ t11 => |
1128 | (t10 as @{const Not}) $ t11 => |
1129 t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
1129 t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |