Homework 2

Definitions File

theory Defs
  imports "HOL-IMP.AExp"
begin

declare [[names_short]]

datatype bexp' = V vname | And "bexp'" "bexp'" | Not "bexp'" | TT | FF
type_synonym assignment = "vname \<Rightarrow> bool"

fun has_const where
  "has_const TT = True"
| "has_const FF = True"
| "has_const (Not a) = has_const a"
| "has_const (And a b) \<longleftrightarrow> has_const a \<or> has_const b"
| "has_const _ = False"

definition "simplified \<phi> \<longleftrightarrow> \<phi> = TT \<or> \<phi> = FF \<or> \<not> has_const \<phi>"


consts sat :: "bexp' \<Rightarrow> assignment \<Rightarrow> bool"

consts models :: "bexp' \<Rightarrow> assignment set"

consts simplify :: "bexp' \<Rightarrow> bexp'"


end

Template File

theory Submission
  imports Defs
begin

fun sat :: "bexp' \<Rightarrow> assignment \<Rightarrow> bool"  where
  "sat _ = undefined"

fun models :: "bexp' \<Rightarrow> assignment set" where
  "models (V x) = {\<sigma>. \<sigma> x}"
| "models TT = UNIV"
  | "models _ = undefined"

theorem sat_iff_model: "sat \<phi> \<sigma> \<longleftrightarrow> \<sigma> \<in> models \<phi>"
  sorry

fun simplify :: "bexp' \<Rightarrow> bexp'"  where
  "simplify _ = undefined"

value "simplify (And (Not FF) (V ''x'')) = V ''x''"

theorem simplify_simplified: "simplified (simplify \<phi>)"
  sorry

theorem simplify_models: "models (simplify \<phi>) = models \<phi>"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem sat_iff_model: "sat \<phi> \<sigma> \<longleftrightarrow> \<sigma> \<in> models \<phi>"
  by (rule Submission.sat_iff_model)

theorem simplify_simplified: "simplified (simplify \<phi>)"
  by (rule Submission.simplify_simplified)

theorem simplify_models: "models (simplify \<phi>) = models \<phi>"
  by (rule Submission.simplify_models)

end