Theory AutoCorres_Base

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

chapter "Basic Stuff" 
theory AutoCorres_Base
  imports
  "TypHeapLib"
  "LemmaBucket_C"
  "CTranslation"
  "Synthesize"
  "Cong_Tactic"

  "Reaches"
  "Mutual_CCPO_Recursion"
  "Simp_Trace"
begin

definition THIN :: "prop ⇒ prop" where "PROP THIN (PROP P) ≡ PROP P"

lemma THIN_I: "PROP P ⟹ PROP THIN (PROP P)"
  by (simp add: THIN_def)

ML_file ‹utils.ML›

named_theorems corres_admissible and corres_top
named_theorems funp_intros and fun_of_rel_intros


definition fun_of_rel:: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool" where
  "fun_of_rel r f = (∀x y. r x y ⟶ y = f x)"

definition funp:: "('a ⇒ 'b ⇒ bool) ⇒ bool" where
 "funp r = (∃f. fun_of_rel r f)" 

lemma funp_witness: "fun_of_rel r f ⟹ funp r"
  by (auto simp add: funp_def)

lemma funp_to_single_valuedp: "funp r ⟹ single_valuedp r"
  by (auto simp add: single_valuedp_def funp_def fun_of_rel_def)

lemma fun_of_rel_xval[fun_of_rel_intros]:
  "fun_of_rel L f_l ⟹ fun_of_rel R f_r ⟹ fun_of_rel (rel_xval L R) (map_xval f_l f_r)"
  by (auto simp add: fun_of_rel_def rel_xval.simps)

lemma funp_rel_xval[funp_intros, corres_admissible]:
  assumes L: "funp L" 
  assumes R: "funp R" 
  shows "funp (rel_xval L R)"
proof -
  from L obtain f_l where f_l: "⋀x y. L x y ⟶ y = f_l x" by (auto simp add: funp_def fun_of_rel_def)
  from R obtain f_r where f_r: "⋀x y. R x y ⟶ y = f_r x" by (auto simp add: funp_def fun_of_rel_def)
  define f where "f = map_xval f_l f_r"
  {
    fix x y
    have "rel_xval L R x y ⟶ y = f x"
      using f_l f_r
      by (auto simp add: rel_xval.simps f_def)
  }
  then show ?thesis
    by (auto simp add: funp_def fun_of_rel_def)
qed

lemma fun_of_rel_eq[fun_of_rel_intros]: "fun_of_rel (=) (λx. x)"
  by (auto simp add: fun_of_rel_def)

lemma fun_of_rel_bot[fun_of_rel_intros]: "fun_of_rel (λ_ _. False) f"
  by (auto simp add: fun_of_rel_def)

lemma funp_eq[funp_intros, corres_admissible]: "funp (=)"
  by (auto simp add: funp_def fun_of_rel_def)

lemma admissible_mem: "ccpo.admissible Inf (≥) (λA. x ∈ A)"
  by (auto simp: ccpo.admissible_def)

lemma funp_rel_prod[funp_intros, corres_admissible]: 
  assumes L: "funp L" 
  assumes R: "funp R" 
  shows "funp (rel_prod L R)"
proof -
  from L obtain f_l where f_l: "⋀x y. L x y ⟶ y = f_l x" by (auto simp add: funp_def fun_of_rel_def)
  from R obtain f_r where f_r: "⋀x y. R x y ⟶ y = f_r x" by (auto simp add: funp_def fun_of_rel_def)
  define f where "f = map_prod f_l f_r"
  {
    fix x y
    have "rel_prod L R x y ⟶ y = f x"
      using f_l f_r
      by (auto simp add: rel_prod.simps f_def map_prod_def split: prod.splits)
  }
  then show ?thesis
    by (auto simp add: funp_def fun_of_rel_def)
qed

lemma funp_rel_sum[funp_intros, corres_admissible]:
  assumes L: "funp L" 
  assumes R: "funp R" 
  shows "funp (rel_sum L R)"
proof -
  from L obtain f_l where f_l: "⋀x y. L x y ⟶ y = f_l x" by (auto simp add: funp_def fun_of_rel_def)
  from R obtain f_r where f_r: "⋀x y. R x y ⟶ y = f_r x" by (auto simp add: funp_def fun_of_rel_def)
  define f where "f = sum_map f_l f_r"
  {
    fix x y
    have "rel_sum L R x y ⟶ y = f x"
      using f_l f_r
      by (auto simp add: rel_sum.simps f_def)
  }
  then show ?thesis
    by (auto simp add: funp_def fun_of_rel_def)
qed

lemma fun_of_rel_bottom: "fun_of_rel ((λ_ _. False)) f"
  by (auto simp add: fun_of_rel_def)

lemma funp_bottom [funp_intros, corres_admissible]: "funp (λ_ _. False)"
  using fun_of_rel_bottom
  by (metis funp_def)

lemma fun_of_rel_prod[fun_of_rel_intros]:
  "fun_of_rel L f_l ⟹ fun_of_rel R f_r ⟹ fun_of_rel (rel_prod L R) (map_prod f_l f_r)"
  by (auto simp add: fun_of_rel_def)

lemma fun_of_rel_sum[fun_of_rel_intros]:
  "fun_of_rel L f_l ⟹ fun_of_rel R f_r ⟹ fun_of_rel (rel_sum L R) (sum_map f_l f_r)"
  by (auto simp add: fun_of_rel_def rel_sum.simps)

lemma fun_of_relcompp[fun_of_rel_intros]: "fun_of_rel F f ⟹ fun_of_rel G g ⟹ fun_of_rel (F OO G) (g o f)"
  by (auto simp add: fun_of_rel_def)

lemma funp_relcompp[funp_intros, corres_admissible]: "funp F ⟹ funp G ⟹ funp (F OO G)"
  using fun_of_relcompp
  by (force simp add: funp_def)


lemma fun_of_rel_rel_map[fun_of_rel_intros]: "fun_of_rel (rel_map f) f"
  by (auto simp add: fun_of_rel_def rel_map_def)

lemma funp_rel_map[funp_intros, corres_admissible]: "funp (rel_map f)"
  using fun_of_rel_rel_map
  by (auto simp add:funp_def)

lemma ccpo_prod_gfp_gfp:
  "class.ccpo
    (prod_lub Inf Inf :: (('a::complete_lattice * 'b :: complete_lattice) set ⇒ _))
    (rel_prod (≥) (≥)) (mk_less (rel_prod (≥) (≥)))"
  by (rule ccpo_rel_prodI ccpo_Inf)+

lemma runs_to_partial_top[corres_top]: "⊤ ∙ s ?⦃ Q ⦄"
  by (simp add: runs_to_partial_def_old)

lemma refines_top[corres_top]: "refines C ⊤ s t R"
  by (auto simp add: refines_def_old)

lemma pred_andE[elim!]: "⟦ (A and B) x; ⟦ A x; B x ⟧ ⟹ R ⟧ ⟹ R"
  by(simp add:pred_conj_def)

lemma pred_andI[intro!]: "⟦ A x; B x ⟧ ⟹ (A and B) x"
  by(simp add:pred_conj_def)

(* A version of "measure" that takes any wellorder, instead of
 * being fixed to "nat". *)
definition measure' :: "('a ⇒ 'b::wellorder) => ('a × 'a) set"
where "measure' = (λf. {(a, b). f a < f b})"

lemma in_measure'[simp, code_unfold]:
    "((x,y) : measure' f) = (f x < f y)"
  by (simp add:measure'_def)

lemma wf_measure' [iff]: "wf (measure' f)"
  apply (clarsimp simp: measure'_def)
  apply (insert wf_inv_image [OF wellorder_class.wf, where f=f])
  apply (clarsimp simp: inv_image_def)
  done

lemma wf_wellorder_measure: "wf {(a, b). (M a :: 'a :: wellorder) < M b}"
  apply (subgoal_tac "wf (inv_image ({(a, b). a < b}) M)")
   apply (clarsimp simp: inv_image_def)
  apply (rule wf_inv_image)
  apply (rule wellorder_class.wf)
  done

lemma wf_custom_measure:
  "⟦ ⋀a b. (a, b) ∈ R ⟹ f a < (f :: 'a ⇒ nat) b ⟧ ⟹  wf R"
  by (metis in_measure wf_def wf_measure)

lemma rel_fun_conversep': "rel_fun R Q f g ⟷ rel_fun R¯¯ Q¯¯ g f"
  unfolding rel_fun_def by auto

end