Theory Test_Side_Conditions

subsection ‹Contrived side conditions›

theory Test_Side_Conditions
imports Dict_Construction
begin

ML ‹
fun assert_alt_total ctxt term = @{assert} (Side_Conditions.is_total ctxt term)
›

fun head where
"head (x # _) = x"

local_setup ‹snd o Side_Conditions.mk_side @{thms head.simps} NONE›

lemma head_side_eq: "head_side xs ⟷ xs ≠ []"
by (cases xs) (auto intro: head_side.intros elim: head_side.cases)

declaration ‹K (Side_Conditions.set_alt @{term head} @{thm head_side_eq})›

fun map where
"map f [] = []" |
"map f (x # xs) = f x # map f xs"

local_setup ‹snd o Side_Conditions.mk_side @{thms map.simps} (SOME @{thms map.induct})›
thm map_side.intros

ML ‹assert_alt_total @{context} @{term map}›

experiment begin

  text ‹Functions that use partial functions always in their domain are processed correctly.›

  fun tail where
  "tail (_ # xs) = xs"

  local_setup ‹snd o Side_Conditions.mk_side @{thms tail.simps} NONE›

  lemma tail_side_eq: "tail_side xs ⟷ xs ≠ []"
  by (cases xs) (auto intro: tail_side.intros elim: tail_side.cases)

  declaration ‹K (Side_Conditions.set_alt @{term tail} @{thm tail_side_eq})›

  function map' where
  "map' f xs = (if xs = [] then [] else f (head xs) # map' f (tail xs))"
  by auto

  termination
    apply (relation "measure (size ∘ snd)")
    apply rule
    subgoal for f xs by (cases xs) auto
    done

  local_setup ‹snd o Side_Conditions.mk_side @{thms map'.simps} (SOME @{thms map'.induct})›
  thm map'_side.intros

  ML ‹assert_alt_total @{context} @{term map'}›

end

lemma map_cong:
  assumes "xs = ys" "⋀x. x ∈ set ys ⟹ f x = g x"
  shows "map f xs = map g ys"
unfolding assms(1)
using assms(2)
by (induction ys) auto

definition map_head where
"map_head xs = map head xs"

experiment begin

  declare map_cong[fundef_cong]

  local_setup ‹snd o Side_Conditions.mk_side @{thms map_head_def} NONE›
  thm map_head_side.intros

  lemma "map_head_side xs ⟷ (∀x ∈ set xs. x ≠ [])"
  by (auto intro: map_head_side.intros elim: map_head_side.cases)

  definition map_head' where
  "map_head' xss = map (map head) xss"

  local_setup ‹snd o Side_Conditions.mk_side @{thms map_head'_def} NONE›
  thm map_head'_side.intros

  lemma "map_head'_side xss ⟷ (∀xs ∈ set xss. ∀x ∈ set xs. x ≠ [])"
  by (auto intro: map_head'_side.intros elim: map_head'_side.cases)

end

experiment begin

  local_setup ‹snd o Side_Conditions.mk_side @{thms map_head_def} NONE›
  term map_head_side
  thm map_head_side.intros

  lemma "¬ map_head_side xs"
  by (auto elim: map_head_side.cases)

end


definition head_known where
"head_known xs = head (3 # xs)"

local_setup ‹snd o Side_Conditions.mk_side @{thms head_known_def} NONE›
thm head_known_side.intros

ML‹assert_alt_total @{context} @{term head_known}›

fun odd :: "nat ⇒ bool" and even where
"odd 0 ⟷ False" |
"even 0 ⟷ True" |
"odd (Suc n) ⟷ even n" |
"even (Suc n) ⟷ odd n"

local_setup ‹snd o Side_Conditions.mk_side @{thms odd.simps even.simps} (SOME @{thms odd_even.induct})›
thm odd_side_even_side.intros

ML‹assert_alt_total @{context} @{term odd}›
ML‹assert_alt_total @{context} @{term even}›

definition odd_known where
"odd_known = odd (Suc 0)"

local_setup ‹snd o Side_Conditions.mk_side @{thms odd_known_def} NONE›
thm odd_known_side.intros

ML‹assert_alt_total @{context} @{term odd_known}›

end