Theory Incredible_Propositional

theory Incredible_Propositional imports
  Abstract_Rules_To_Incredible
  Propositional_Formulas
begin

text ‹Our concrete interpretation with propositional logic will cover conjunction and implication
  as well as constant symbols. The type for variables will be @{typ string}.›

datatype prop_funs = "and" | imp | Const "string"

text ‹The rules are introduction and elimination of conjunction and implication.›
datatype prop_rule = andI | andE | impI | impE

definition prop_rules :: "prop_rule stream"
  where "prop_rules = cycle [andI, andE, impI, impE]"

lemma iR_prop_rules [simp]: "sset prop_rules = {andI, andE, impI, impE}"
  unfolding prop_rules_def by simp

text ‹Just some short notation.›
abbreviation X :: "(string,'a) pform"
  where "X ≡ Var ''X''"
abbreviation Y :: "(string,'a) pform"
  where "Y ≡ Var ''Y''"

text ‹Finally the right- and left-hand sides of the rules.›

fun consequent :: "prop_rule ⇒ (string, prop_funs) pform list"
  where "consequent andI = [Fun and [X, Y]]"
  | "consequent andE = [X, Y]"
  | "consequent impI = [Fun imp [X, Y]]"
  | "consequent impE = [Y]"

fun antecedent :: "prop_rule ⇒ ((string,prop_funs) pform,string) antecedent list"
  where "antecedent andI = [plain_ant X, plain_ant Y]"
  | "antecedent andE = [plain_ant (Fun and [X, Y])]"
  | "antecedent impI = [Antecedent {|X|} Y {}]"
  | "antecedent impE = [plain_ant (Fun imp [X, Y]), plain_ant X]"


interpretation propositional: Abstract_Rules
  "curry (SOME f. bij f):: nat ⇒ string ⇒ string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform ⇒ bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
proof
  show "∀xs∈sset prop_rules. consequent xs ≠ []"
    unfolding prop_rules_def
    using consequent.elims by blast
next
  show "∀xs∈sset prop_rules. ⋃((λ_. {}) ` set (consequent xs)) = {}"
    by clarsimp
next
  fix i' r i ia
  assume "r ∈ sset prop_rules"
    and "ia < length (antecedent r)"
    and "i' < length (antecedent r)"
  then show "a_fresh (antecedent r ! ia) ∩ a_fresh (antecedent r ! i') = {} ∨ ia = i'"
    by (cases i'; auto)
next
  fix p
  show "{} ∪ ⋃((λ_. {}) ` fset (a_hyps p)) ⊆ a_fresh p"  by clarsimp
qed

end