Theory Instantiation

theory Instantiation

imports  TNEMO Universals

begin

consts

Inst :: "Ob => Un => Ti => o"

axioms

Inst_IsA: "(ALL c d t x. (IsA(c,d) --> (Inst(x,c,t) --> Inst(x,d,t))))"
Inst_IsAI: "(ALL x c d t. ((Inst(x,c,t) & Inst(x,d,t) --> IsAI(c,d))))"
Inst_E: "(ALL x c t. (Inst(x,c,t) --> E(x,t)))"
Inst_Un: "(ALL c. (EX x t. (Inst(x,c,t))))"
Inst_Ob: "(ALL x t. (E(x,t) --> (EX c. (Inst(x,c,t)))))"

(* axioms as rules *)

lemma Inst_IsA_rule: "IsA(c,d) ==> (ALL x t. (Inst(x,c,t) --> Inst(x,d,t)))"
apply(insert Inst_IsA)
apply(auto)
done

lemma Inst_IsAI_rule: "[|Inst(x,c,t);Inst(x,d,t)|] ==> IsAI(c,d)"
apply(insert Inst_IsAI)
apply(auto)
done

lemma Inst_Ob_rule: "(E(x,t) ==> (EX c. (Inst(x,c,t))))"
apply(insert Inst_Ob)
apply(auto)
done

end