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 "xssset prop_rules. consequent xs  []"
    unfolding prop_rules_def
    using consequent.elims by blast
next
  show "xssset 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