(*<*)
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
  with polymorphic datatypes and linear arithmetic. We could have modelled by using one of the
  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
  substitution is not injective so we can't write this in terms of @{text "wfRCV"}.
  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) #_\<Gamma> 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 :: "Θ → B → Γ → 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