Theory AutoCorres_Utils

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory AutoCorres_Utils
  imports 
    Print_Annotated 
    ML_Fun_Cache 
  keywords "lazy_named_theorems"::thy_decl

begin

definition CONV_ID:: "'a::{} ⇒ 'a" where
 "CONV_ID x ≡ x"

lemma CONV_ID_intro: "(x::'a::{}) ≡ CONV_ID x"
  by (simp add: CONV_ID_def)

ML_file "utils.ML"

definition "FALSE ≡ (⋀P. PROP P)"
lemma ex_falso_quodlibet: "PROP FALSE ⟹ PROP P"
  by (simp add: FALSE_def)

ML_file ‹context_tactical.ML›
ML_file "lazy_named_theorems.ML"
ML_file "interpretation_data.ML"

definition sim_set :: "('a ⇒ 'b ⇒ bool) ⇒ 'a set ⇒ 'b set ⇒ bool" where
  "sim_set R A B ⟷ (∀a∈A. ∃b∈B. R a b)"

lemma sim_set_empty: "sim_set R {} B"
  by (auto simp: sim_set_def)

lemma sim_set_insert: "R a b ⟹ sim_set R A B ⟹ sim_set R (insert a A) (insert b B)"
  by (auto simp: sim_set_def)

lemma sim_set_Collect_Ex:
  "(⋀a. sim_set R {x. P a x} {x. Q a x}) ⟹ sim_set R {x. ∃a. P a x} {x. ∃a. Q a x}"
  by (fastforce simp: sim_set_def)

lemma sim_set_Collect_conj:
  "(A ⟹ sim_set R {x. P x} {x. Q x}) ⟹ sim_set R {x. A ∧ P x} {x. A ∧ Q x}"
  by (fastforce simp: sim_set_def)

lemma sim_set_Collect_eq:
  "R a b ⟹ sim_set R {x. x = a} {x. x = b}"
  by (fastforce simp: sim_set_def)

lemma sim_set_eq_rel_set: "sim_set R = rel_set R OO (⊆)"
  apply (auto simp: sim_set_def rel_set_def relcomp.simps fun_eq_iff OO_def)[1]
  subgoal for A B
    by (intro exI[of _ "{b∈B. ∃a∈A. R a b}"]) blast
  apply blast
  done

end