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