Theory RCLogic

(*<*)
theory RCLogic
  imports Wellformed
begin
  (*>*)

hide_const Syntax.dom

chapter ‹Refinement Constraint Logic›

text ‹ Semantics for the logic we use in the refinement constraints. It is a multi-sorted, quantifier free
logic with polymorphic datatypes and linear arithmetic. We could have modelled by using one of the 
encodings to FOL however we wanted to explore using a more direct model. ›

section ‹Evaluation and Satisfiability›

subsection ‹Valuation›

text ‹ Refinement constraint logic values. SUt is a value for the uninterpreted 
       sort that corresponds to basic type variables. For now we only need one of these universes.
       We wrap an smt\_val inside it during a process we call 'boxing' 
       which is introduced in the RCLogicL theory ›
nominal_datatype rcl_val = SBitvec "bit list" | SNum int | SBool bool | SPair rcl_val rcl_val | 
  SCons tyid string rcl_val | SConsp tyid string b rcl_val |
  SUnit | SUt rcl_val 

text ‹ RCL sorts. Represent our domains. The universe is the union of all of the these.
        S\_Ut is the single uninterpreted sort. These map almost directly to basic type 
        but we have them to distinguish syntax (basic types) and semantics (RCL sorts) ›
nominal_datatype rcl_sort = S_bool | S_int | S_unit | S_pair rcl_sort rcl_sort | S_id tyid | S_app tyid rcl_sort | S_bitvec | S_ut 

type_synonym valuation = "(x,rcl_val) map"

type_synonym type_valuation = "(bv,rcl_sort) map"

text ‹Well-sortedness for RCL values›
inductive wfRCV:: "Θ ⇒ rcl_val ⇒ b ⇒ bool" ( ‹ _  ⊢ _ : _› [50,50] 50) where
  wfRCV_BBitvecI:  "P ⊢ (SBitvec bv)  : B_bitvec"
| wfRCV_BIntI:  "P ⊢ (SNum n)  : B_int"
| wfRCV_BBoolI: "P ⊢ (SBool b) : B_bool"
| wfRCV_BPairI: "⟦ P ⊢ s1 : b1 ; P ⊢ s2 : b2 ⟧ ⟹ P ⊢ (SPair s1 s2) : (B_pair b1 b2)"
| wfRCV_BConsI: "⟦  AF_typedef s dclist ∈ set Θ;
      (dc, ⦃ x : b  | c ⦄) ∈ set dclist ;
     Θ ⊢ s1 : b ⟧ ⟹ Θ ⊢(SCons s dc s1) : (B_id s)"
| wfRCV_BConsPI:"⟦ AF_typedef_poly s bv dclist ∈ set Θ;
      (dc, ⦃ x : b  | c ⦄) ∈ set dclist ;
       atom bv ♯ (Θ, SConsp s dc b' s1, B_app s b');
     Θ ⊢ s1 : b[bv::=b']bb ⟧ ⟹ Θ ⊢(SConsp s dc b' s1) : (B_app s b')"
| wfRCV_BUnitI: "P ⊢ SUnit : B_unit"
| wfRCV_BVarI: "P ⊢ (SUt n) : (B_var bv)"
equivariance wfRCV
nominal_inductive wfRCV 
  avoids wfRCV_BConsPI: bv
proof(goal_cases)
  case (1 s bv dclist Θ dc x b c b' s1)
  then show ?case using fresh_star_def by auto
next
  case (2 s bv dclist Θ dc x b c s1 b')
  then show ?case by auto
qed

inductive_cases wfRCV_elims :
  "wfRCV P s  B_bitvec"
  "wfRCV P s (B_pair b1 b2)"
  "wfRCV P s (B_int)"
  "wfRCV P s (B_bool)"
  "wfRCV P s (B_id ss)"
  "wfRCV P s (B_var bv)"
  "wfRCV P s (B_unit)"
  "wfRCV P s (B_app tyid b)"
  "wfRCV P (SBitvec bv) b"
  "wfRCV P (SNum n)  b"
  "wfRCV P (SBool n)  b"
  "wfRCV P (SPair s1 s2) b"
  "wfRCV P (SCons s dc s1) b"
  "wfRCV P (SConsp s dc b' s1) b"
  "wfRCV P SUnit b"
  "wfRCV P (SUt s1) b"

text ‹ Sometimes we want to assert @{text "P ⊢ s ~ b[bv=b']"} and we want to know what b is 
however substitution is not injective so we can't write this in terms of @{text "wfRCV"}. 
So we define a relation that makes the components of the substitution explicit. ›

inductive wfRCV_subst:: "Θ ⇒ rcl_val ⇒ b ⇒ (bv*b) option ⇒ bool" where
  wfRCV_subst_BBitvecI:  "wfRCV_subst P (SBitvec bv) B_bitvec  sub "
| wfRCV_subst_BIntI:  "wfRCV_subst P (SNum n)  B_int sub "
| wfRCV_subst_BBoolI: "wfRCV_subst P (SBool b)  B_bool sub  "
| wfRCV_subst_BPairI: "⟦ wfRCV_subst P s1 b1 sub ; wfRCV_subst P s2 b2 sub ⟧ ⟹ wfRCV_subst P (SPair s1 s2) (B_pair b1 b2) sub"
| wfRCV_subst_BConsI: "⟦  AF_typedef s dclist ∈ set Θ;
      (dc, ⦃ x : b  | c ⦄) ∈ set dclist ;
     wfRCV_subst Θ s1 b None ⟧ ⟹ wfRCV_subst Θ (SCons s dc s1) (B_id s) sub"
| wfRCV_subst_BConspI: "⟦  AF_typedef_poly s bv dclist ∈ set Θ;
      (dc, ⦃ x : b  | c ⦄) ∈ set dclist ;
     wfRCV_subst Θ s1 (b[bv::=b']bb) sub  ⟧ ⟹ wfRCV_subst Θ (SConsp s dc b' s1) (B_app s b') sub"
| wfRCV_subst_BUnitI: "wfRCV_subst P SUnit B_unit sub "
| wfRCV_subst_BVar1I: "bvar ≠ bv ⟹ wfRCV_subst P (SUt n) (B_var bv)  (Some (bvar,bin))"
| wfRCV_subst_BVar2I: "⟦ bvar = bv; wfRCV_subst P s bin None ⟧ ⟹ wfRCV_subst P s (B_var bv)  (Some (bvar,bin))"
| wfRCV_subst_BVar3I: "wfRCV_subst P (SUt n) (B_var bv)  None"
equivariance wfRCV_subst
nominal_inductive wfRCV_subst .

subsection ‹Evaluation base-types›

inductive eval_b :: "type_valuation ⇒ b ⇒ rcl_sort ⇒ bool"  ( ‹_ ⟦ _ ⟧ ~ _ › ) where
  "v ⟦ B_bool ⟧ ~ S_bool"
| "v ⟦ B_int ⟧ ~ S_int"
| "Some s = v bv ⟹ v ⟦ B_var bv ⟧ ~ s"
equivariance eval_b
nominal_inductive eval_b .

subsection ‹Wellformed vvaluations›

definition wfI ::  "Θ ⇒ Γ ⇒ valuation ⇒ bool" ( ‹ _ ; _ ⊢ _› )  where
  "Θ ; Γ ⊢ i = (∀ (x,b,c) ∈ toSet Γ. ∃s. Some s = i x ∧ Θ ⊢ s : b)"

subsection ‹Evaluating Terms›

nominal_function eval_l :: "l ⇒ rcl_val" ( ‹⟦ _ ⟧ › ) where
  "⟦ L_true ⟧ = SBool True"
|  "⟦ L_false ⟧ = SBool False"
|  "⟦ L_num n ⟧ = SNum n"
|  "⟦ L_unit ⟧ = SUnit"
|  "⟦ L_bitvec n ⟧ = SBitvec n"
                   apply(auto simp: eqvt_def eval_l_graph_aux_def)
  by (metis l.exhaust)
nominal_termination (eqvt) by lexicographic_order

inductive eval_v :: "valuation ⇒ v ⇒ rcl_val ⇒ bool"  ( ‹_ ⟦ _ ⟧ ~ _ › ) where
  eval_v_litI:   "i ⟦ V_lit l ⟧ ~ ⟦ l ⟧ "
| eval_v_varI: "Some sv = i x  ⟹ i ⟦ V_var x ⟧ ~ sv"
| eval_v_pairI: "⟦ i ⟦ v1 ⟧ ~ s1 ; i ⟦ v2 ⟧ ~ s2 ⟧ ⟹ i ⟦ V_pair v1 v2 ⟧ ~ SPair s1 s2"
| eval_v_consI: "i ⟦ v ⟧ ~ s ⟹ i ⟦ V_cons tyid dc v ⟧ ~ SCons tyid dc s"
| eval_v_conspI: "i ⟦ v ⟧ ~ s ⟹ i ⟦ V_consp tyid dc b v ⟧ ~ SConsp tyid dc b s"
equivariance eval_v
nominal_inductive eval_v .

inductive_cases eval_v_elims:
  "i ⟦ V_lit l ⟧ ~  s"
  "i ⟦ V_var x ⟧ ~  s"
  "i ⟦ V_pair v1 v2 ⟧ ~ s"
  "i ⟦ V_cons tyid dc v ⟧ ~ s"
  "i ⟦ V_consp tyid dc b v ⟧ ~ s"

inductive eval_e :: "valuation ⇒ ce ⇒ rcl_val ⇒ bool" ( ‹_ ⟦ _ ⟧ ~ _ › )  where
  eval_e_valI: "i ⟦ v ⟧ ~  sv ⟹ i ⟦ CE_val v ⟧ ~ sv"
| eval_e_plusI: "⟦ i ⟦ v1 ⟧ ~ SNum n1; i ⟦ v2 ⟧ ~ SNum n2  ⟧  ⟹ i ⟦ (CE_op Plus v1 v2) ⟧ ~ (SNum (n1+n2))"
| eval_e_leqI: "⟦ i ⟦ v1 ⟧ ~ (SNum n1); i ⟦ v2 ⟧ ~ (SNum n2) ⟧  ⟹ i ⟦ (CE_op LEq v1 v2) ⟧ ~ (SBool (n1 ≤ n2))"
| eval_e_eqI: "⟦ i ⟦ v1 ⟧ ~ s1; i ⟦ v2 ⟧ ~ s2 ⟧  ⟹ i ⟦ (CE_op Eq v1 v2) ⟧ ~ (SBool (s1 = s2))"
| eval_e_fstI: "⟦ i ⟦ v ⟧ ~ SPair v1 v2  ⟧ ⟹ i ⟦ (CE_fst v) ⟧ ~ v1"
| eval_e_sndI: "⟦ i ⟦ v ⟧ ~ SPair v1 v2  ⟧ ⟹ i ⟦ (CE_snd v) ⟧ ~ v2"
| eval_e_concatI:"⟦ i ⟦ v1 ⟧ ~ (SBitvec bv1); i ⟦ v2 ⟧ ~ (SBitvec bv2) ⟧ ⟹ i ⟦ (CE_concat v1 v2) ⟧ ~ (SBitvec (bv1@bv2))"
| eval_e_lenI:"⟦ i ⟦ v ⟧  ~ (SBitvec bv) ⟧ ⟹ i ⟦ (CE_len v) ⟧ ~ (SNum (int (List.length bv)))"
equivariance eval_e
nominal_inductive eval_e .

inductive_cases eval_e_elims:
  "i ⟦ (CE_val v) ⟧ ~ s"
  "i ⟦ (CE_op Plus v1 v2) ⟧ ~ s"
  "i ⟦ (CE_op LEq v1 v2) ⟧ ~ s"
  "i ⟦ (CE_op Eq v1 v2) ⟧ ~ s"
  "i ⟦ (CE_fst v) ⟧ ~ s"
  "i ⟦ (CE_snd v) ⟧ ~ s"
  "i ⟦ (CE_concat v1 v2) ⟧ ~ s"
  "i ⟦ (CE_len v) ⟧ ~ s"

inductive eval_c :: "valuation ⇒ c ⇒ bool ⇒ bool" ( ‹ _ ⟦ _ ⟧ ~ _ ›)  where
  eval_c_trueI:  "i ⟦ C_true ⟧ ~ True"
| eval_c_falseI:"i ⟦ C_false ⟧ ~ False"
| eval_c_conjI: "⟦ i ⟦ c1 ⟧ ~ b1 ; i ⟦ c2 ⟧ ~ b2 ⟧ ⟹  i ⟦ (C_conj c1 c2) ⟧ ~  (b1 ∧ b2)"
| eval_c_disjI: "⟦ i ⟦ c1 ⟧ ~ b1 ; i ⟦ c2 ⟧ ~ b2 ⟧ ⟹  i ⟦ (C_disj c1 c2) ⟧ ~ (b1 ∨ b2)"
| eval_c_impI:"⟦ i ⟦ c1 ⟧ ~ b1 ; i ⟦ c2 ⟧ ~ b2 ⟧ ⟹  i ⟦ (C_imp c1 c2) ⟧ ~ (b1 ⟶ b2)"
| eval_c_notI:"⟦ i ⟦ c ⟧ ~ b ⟧ ⟹ i ⟦ (C_not c) ⟧ ~ (¬ b)"
| eval_c_eqI:"⟦ i ⟦ e1 ⟧ ~ sv1; i ⟦ e2 ⟧ ~ sv2 ⟧ ⟹ i ⟦ (C_eq e1 e2) ⟧ ~ (sv1=sv2)"
equivariance eval_c
nominal_inductive eval_c .

inductive_cases eval_c_elims:
  "i ⟦ C_true ⟧ ~  True"
  "i ⟦ C_false ⟧ ~ False"
  "i ⟦ (C_conj c1 c2)⟧ ~ s"
  "i ⟦ (C_disj c1 c2)⟧ ~ s"
  "i ⟦ (C_imp c1 c2)⟧ ~ s"
  "i ⟦ (C_not c) ⟧ ~ s"
  "i ⟦ (C_eq e1 e2)⟧ ~ s"
  "i ⟦ C_true ⟧ ~ s"
  "i ⟦ C_false ⟧ ~ s"

subsection ‹Satisfiability›

inductive  is_satis :: "valuation ⇒ c ⇒ bool" ( ‹ _ ⊨ _ › ) where
  "i ⟦ c ⟧ ~ True ⟹ i ⊨ c"
equivariance is_satis
nominal_inductive is_satis .

nominal_function is_satis_g :: "valuation ⇒ Γ ⇒ bool" ( ‹ _ ⊨ _ › ) where
  "i ⊨ GNil = True"
| "i ⊨ ((x,b,c) #Γ G) = ( i ⊨ c ∧  i ⊨ G)"
       apply(auto simp: eqvt_def is_satis_g_graph_aux_def)
  by (metis Γ.exhaust old.prod.exhaust)
nominal_termination (eqvt) by lexicographic_order

section ‹Validity›

nominal_function  valid :: "Θ ⇒ ℬ ⇒ Γ ⇒ c ⇒ bool"  (‹_ ; _ ; _  ⊨ _ › [50, 50] 50)  where
  "P ; B ; G ⊨ c = ( (P ; B ; G ⊢wf c) ∧ (∀i. (P ; G ⊢ i) ∧  i ⊨ G ⟶ i ⊨ c))"
  by (auto simp: eqvt_def wfI_def valid_graph_aux_def)
nominal_termination (eqvt) by lexicographic_order

section ‹Lemmas›
text ‹Lemmas needed for Examples›

lemma valid_trueI [intro]:
  fixes G::Γ
  assumes "P ; B ⊢wf G"
  shows "P ; B ; G ⊨ C_true"
proof -
  have "∀i. i ⊨ C_true" using is_satis.simps eval_c_trueI by simp
  moreover have "P ; B ; G ⊢wf C_true" using wfC_trueI assms by simp
  ultimately show ?thesis using valid.simps by simp
qed

end