src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41046 f2e94005d283
parent 41045 2a41709f34c1
child 41047 9f1d3fcef1ca
equal deleted inserted replaced
41045:2a41709f34c1 41046:f2e94005d283
   422    (@{const_name snd}, 1),
   422    (@{const_name snd}, 1),
   423    (@{const_name Id}, 0),
   423    (@{const_name Id}, 0),
   424    (@{const_name converse}, 1),
   424    (@{const_name converse}, 1),
   425    (@{const_name trancl}, 1),
   425    (@{const_name trancl}, 1),
   426    (@{const_name rel_comp}, 2),
   426    (@{const_name rel_comp}, 2),
       
   427    (@{const_name prod}, 2),
   427    (@{const_name image}, 2),
   428    (@{const_name image}, 2),
   428    (@{const_name finite}, 1),
   429    (@{const_name finite}, 1),
   429    (@{const_name unknown}, 0),
   430    (@{const_name unknown}, 0),
   430    (@{const_name is_unknown}, 1),
   431    (@{const_name is_unknown}, 1),
   431    (@{const_name safe_The}, 1),
   432    (@{const_name safe_The}, 1),
  1643             raise SAME ())
  1644             raise SAME ())
  1644          handle SAME () =>
  1645          handle SAME () =>
  1645                 s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
  1646                 s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
  1646       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
  1647       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
  1647         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
  1648         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
  1648       | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
  1649       | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
  1649         s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
  1650         $ t1 $ (t2 as Abs (_, _, t2')) =>
  1650                         map (do_term depth Ts) [t1, t2])
  1651         if loose_bvar1 (t2', 0) then
       
  1652           s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2])
       
  1653         else
       
  1654           do_term depth Ts
       
  1655                   (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
       
  1656                    $ t1 $ incr_boundvars ~1 t2')
  1651       | Const (x as (@{const_name distinct},
  1657       | Const (x as (@{const_name distinct},
  1652                Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
  1658                Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
  1653         $ (t1 as _ $ _) =>
  1659         $ (t1 as _ $ _) =>
  1654         (t1 |> HOLogic.dest_list |> distinctness_formula T'
  1660         (t1 |> HOLogic.dest_list |> distinctness_formula T'
  1655          handle TERM _ => do_const depth Ts t x [t1])
  1661          handle TERM _ => do_const depth Ts t x [t1])