Abstract Interpretation

Definitions File

theory Defs
  imports Main
begin

no_notation less_eq  ("(_/ \<le> _)"  [51, 51] 50)
datatype bin = Zero | One | Single | More | Any

fun \<gamma> :: "bin \<Rightarrow> nat set" where
  "\<gamma> Zero = {0}" |
  "\<gamma> One = {2^0}" |
  "\<gamma> Single = {2^n| n. True }" |
  "\<gamma> More = {n. (\<nexists>k. n = 2^k) \<and> n\<noteq>0 }" |
  "\<gamma> Any = UNIV"

consts less_bin :: "bin \<Rightarrow> bin \<Rightarrow> bool"

consts plus' :: "bin \<Rightarrow> bin \<Rightarrow> bin"

end

Template File

theory Submission
  imports Defs
begin

definition less_bin :: "bin \<Rightarrow> bin \<Rightarrow> bool" ("(_/ \<le> _)"  [51, 51] 50) where
  "x \<le> y = undefined"

theorem less_bin_sub: "(x::bin) \<le> y \<Longrightarrow> \<gamma> x \<subseteq> \<gamma> y"
  sorry

fun plus' :: "bin \<Rightarrow> bin \<Rightarrow> bin" where
  "plus' _ = undefined"

theorem plus'_\<gamma>: "\<lbrakk>n1 \<in> \<gamma> x; n2 \<in> \<gamma> y\<rbrakk> \<Longrightarrow> n1+n2 \<in> \<gamma> (plus' x y)"
  sorry

type_synonym entry = "(bin*bin) option"
type_synonym row = "(nat*entry) list"

definition table :: "row list" where
  "table = undefined"

end

Check File

theory Check
  imports Submission
begin

lemma "(x::bin) \<le> y \<Longrightarrow> \<gamma> x \<subseteq> \<gamma> y"
  by (rule Submission.less_bin_sub)

lemma "\<lbrakk>n1 \<in> \<gamma> x; n2 \<in> \<gamma> y\<rbrakk> \<Longrightarrow> n1+n2 \<in> \<gamma> (plus' x y)"
  by (rule Submission.plus'_\<gamma>)

end