# 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
```