# Theory CaseStudy2

section "Case study 2"
theory CaseStudy2
imports Main "HOL-Library.Multiset"
begin
text ‹
\null
In the second case study, the problem will be examined of defining a function
‹t_ins› performing item insertion into binary search trees (admitting value
repetitions) of elements of a linear order, and then proving the correctness of
this definition, i.e. that the trees output by the function still be sorted if
the input ones are and contain one more occurrence of the inserted value, the
number of occurrences of any other value being left unaltered.
Here below is a naive tail-recursive definition of such function:
\null
›