src/Tools/atomize_elim.ML
changeset 33002 f3f02f36a3e2
parent 31902 862ae16a799d
child 33029 2fefe039edf1
equal deleted inserted replaced
33001:82382652e5e7 33002:f3f02f36a3e2
    40            |> map fst
    40            |> map fst
    41 
    41 
    42 (* rearrange_prems as a conversion *)
    42 (* rearrange_prems as a conversion *)
    43 fun rearrange_prems_conv pi ct =
    43 fun rearrange_prems_conv pi ct =
    44     let
    44     let
    45       val pi' = 0 :: map (curry op + 1) pi
    45       val pi' = 0 :: map (Integer.add 1) pi
    46       val fwd  = Thm.trivial ct
    46       val fwd  = Thm.trivial ct
    47                   |> Drule.rearrange_prems pi'
    47                   |> Drule.rearrange_prems pi'
    48       val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
    48       val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
    49                   |> Drule.rearrange_prems (invert_perm pi')
    49                   |> Drule.rearrange_prems (invert_perm pi')
    50     in Thm.equal_intr fwd back end
    50     in Thm.equal_intr fwd back end