Theory Incredible_Predicate

theory Incredible_Predicate imports
  Abstract_Rules_To_Incredible
  Predicate_Formulas
begin

text Our example interpretation with predicate logic will cover implication and the
  universal quantifier.

text The rules are introduction and elimination of implication and universal quantifiers.
datatype prop_rule = allI | allE | impI | impE

definition prop_rules :: "prop_rule stream"
  where "prop_rules = cycle [allI, allE, impI, impE]"

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

text Just some short notation.
abbreviation X :: "form"
  where "X  Var 10 []"
abbreviation Y :: "form"
  where "Y  Var 11 []"
abbreviation x :: "form"
  where "x  Var 9 []"
abbreviation t :: "form"
  where "t  Var 13 []"
abbreviation P :: "form  form"
  where "P f  Var 12 [f]"
abbreviation Q :: "form  form"
  where "Q f  Op ''Q'' [f]"
abbreviation imp :: "form  form  form"
  where "imp f1 f2  Op ''imp'' [f1, f2]"
abbreviation ForallX :: "form  form"
  where "ForallX f  Quant ''all'' 9 f"

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

fun consequent :: "prop_rule  form list"
  where "consequent allI = [ForallX (P x)]"
  | "consequent allE = [P t]"
  | "consequent impI = [imp X Y]"
  | "consequent impE = [Y]"

abbreviation allI_input where "allI_input  Antecedent {||} (P (LC 0)) {0}"
abbreviation impI_input where "impI_input  Antecedent {|X|} Y {}"

fun antecedent :: "prop_rule  (form, lconst) antecedent list"
  where "antecedent allI = [allI_input]"
  | "antecedent allE = [plain_ant (ForallX (P x))]"
  | "antecedent impI = [impI_input]"
  | "antecedent impE = [plain_ant (imp X Y), plain_ant X]"

interpretation predicate: Abstract_Rules
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  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. (lc ` set (consequent xs)) = {}"
    by auto
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 r p
  assume "r  sset prop_rules"
  and "p  set (antecedent r)"
  thus "lc (a_conc p)  (lc ` fset (a_hyps p))  a_fresh p" by auto
qed

end