Theory IA_Instance

theory IA_Instance
imports
  Ord.IA_Checker
  LTS_Termination_Prover
  LTS_Safety_Prover
begin

no_notation Simplex.curr_val_satisfies_state ("⊨")

context IA_locale begin

fun constant_exp where
  "constant_exp (Bool True) = Fun LessF [const 0, const 1]"
| "constant_exp (Bool False) = Fun LessF [const 1, const 0]"
| "constant_exp (Int n) = const n"

sublocale algebra_constant I constant_exp
proof
  show "vars_term (constant_exp d) = {}" for d by (cases d rule: constant_exp.cases, auto)
  show "⟦constant_exp d⟧ α = d" for d α by (cases d rule: constant_exp.cases, auto)
qed

fun is_constant where
  "is_constant (Fun _ []) = True"
| "is_constant _ = False"

lemma is_constant:
  assumes "is_constant e" shows "⟦e⟧α = ⟦e⟧β"
proof(cases e)
  case (Fun f es) with assms show ?thesis by (cases es, auto)
qed (insert assms, auto)

sublocale art_checker
  where type_fixer = "TYPE(_)"
    and I = I
    and type_of_fun = type_of_fun
    and Values_of_type = Values_of_type
    and Bool_types = "{BoolT}"
    and to_bool = to_bool
    and tc = check_clause
    and tc2 = check_clause
    and sa = showsl_IA_exp
    and sa2 = showsl_IA_exp
    and ne = negate
    and ne2 = negate ..

abbreviation "less_eq_formula s t ≡ Atom (Fun LeF [s,t])"
abbreviation "less_formula s t ≡ Atom (Fun LessF [s,t])"

lemma less_eq_meaning:
  assumes α: "assignment α"
      and s: "s :⇩f IntT"
      and t: "t :⇩f IntT"
  shows "α ⊨ less_eq_formula s t ⟷ ⟦s⟧ α ≤ ⟦t⟧ α"
  using eval_types[OF α s] eval_types[OF α t] s t
  by (cases "⟦s⟧α"; cases "⟦t⟧α", auto simp: is_bool_def)

lemma less_meaning:
  assumes α: "assignment α"
      and s: "s :⇩f IntT"
      and t: "t :⇩f IntT"
  shows "α ⊨ less_formula s t ⟷ ⟦s⟧ α < ⟦t⟧ α"
  using eval_types[OF α s] eval_types[OF α t] s t
  by (cases "⟦s⟧α"; cases "⟦t⟧α", auto simp: is_bool_def)

(* lemma transition_removal is an instance of transition_removal_bounded *)
interpretation transition_removal: transition_removal_bounded
  where type_fixer = "TYPE(_)"
    and I = I
    and type_of_fun = type_of_fun
    and Values_of_type = Values_of_type
    and Bool_types = "{BoolT}"
    and to_bool = to_bool
    and showsl_atom = showsl_IA_exp
    and logic_checker = check_clause
    and negate_atom = negate
    and dom_type = IntT
    and less_eq = "(≤) :: val ⇒ _ ⇒ _"
    and less = "(<)"
    and less_eq_formula = less_eq_formula
    and less_formula = less_formula
    and is_constant = is_constant
  by (unfold_locales; (fact less_eq_meaning less_meaning is_constant | simp add: All_less_Suc))


sublocale termination_checker: termination_checker
  where type_fixer = "TYPE(_)"
    and I = I
    and type_of_fun = type_of_fun
    and Values_of_type = Values_of_type
    and Bool_types = "{BoolT}"
    and to_bool = to_bool
    and sa = showsl_IA_exp
    and tc = check_clause
    and ne = negate
    and sa2 = showsl_IA_exp
    and tc2 = check_clause
    and ne2 = negate
    and dom_type = IntT
    and less_eq = "(≤) :: val ⇒ _ ⇒ _"
    and less = "(<)"
    and less_eq_formula = less_eq_formula
    and less_formula = less_formula
    and definability_checker = def_checker
    and is_constant = is_constant
    by unfold_locales

definition check_termination where "check_termination ≡ termination_checker.check"

lemma check_termination: "isOK (check_termination P prf) ⟹ lts_termination (lts_of P)"
  by (unfold check_termination_def, fact termination_checker.sound)

end


thm IA.check_termination IA.check_safety

declare IA.constant_exp.simps[code]
  IA.check_termination_def[code]
  IA.check_safety_def[code]

end