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  (aA. bB. 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 _ "{bB. aA. R a b}"]) blast
  apply blast
  done

end