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