Theory Universals

theory Universals imports FOL

begin

typedecl Un

arities Un :: "term"

consts

IsA :: "Un => Un => o"
IsAPr :: "Un => Un => o"
IsARoot :: "Un => o" 
IsAI :: "Un => Un => o"
IsAO :: "Un => Un => o"

axioms

IsA_refl: "(ALL c. (IsA(c,c)))"
IsA_antisym: "(ALL c d. (IsA(c,d) & IsA(d,c) --> c = d))"
IsA_trans: "(ALL c d e. (IsA(c,d) & IsA(d,e) --> IsA(c,e)))" 
IsA_wsp_IsAI: "(ALL c d. (IsAPr(c,d) --> (EX e. (IsAPr(e,d) & ~IsAI(e,c)))))" 
IsA_npo: "ALL c d. (IsAO(c,d) --> IsAI(c,d))"
IsA_root: "(EX c. IsARoot(c))" 

defs

IsAPr_def: "IsAPr(c,d) == IsA(c,d) & ~IsA(d,c)"
IsARoot_def: "IsARoot(d) == (ALL c. IsA(c,d))" 
IsAI_def: "IsAI(c,d) == IsA(c,d) | IsA(d,c)"
IsAO_def: "IsAO(c,d) == (EX e. (IsA(e,c) & IsA(e,d)))"


(* axioms as rules *)

lemma IsA_antisym_rule : "[|IsA(c,d);IsA(d,c)|] ==> c = d"
apply(insert IsA_antisym)
apply(erule_tac x="c" in allE,erule_tac x="d" in allE)
apply(drule mp)
apply(auto)
done

lemma IsA_trans_rule: "[|IsA(c,d);IsA(d,e)|] ==> IsA(c,e)"
apply(insert IsA_trans)
apply(erule_tac x="c" in allE,erule_tac x="d" in allE, erule_tac x="e" in allE)
apply(drule mp)
apply(auto)
done
 

lemma IsA_wsp_IsAI_rule: "IsAPr(c,d) ==> (EX e. (IsAPr(e,d) & ~IsAI(e,c)))" 
apply(insert IsA_wsp_IsAI)
apply(erule_tac x="c" in allE,erule_tac x="d" in allE)
apply(drule mp)
apply(auto)
done

lemma IsA_npo_rule: "[|IsA(e,c);IsA(e,d)|] ==> IsAI(c,d)"
apply(insert IsA_npo)
apply(unfold IsAO_def)
apply(auto)
done

lemma IsA_npo_rule1: "IsAO(c,d) ==> IsAI(c,d)"
apply(insert IsA_npo)
apply(auto)
done



(* theorems about Universals *)

theorem IsA_impl_Id_or_IsAPr: "IsA(c,d) ==> (c=d | IsAPr(c,d))"
apply(safe)
apply(unfold IsAPr_def)
apply(safe)
apply(drule IsA_antisym_rule)
apply(auto)
done


theorem IsARoot_unique: "[|IsARoot(c);IsARoot(d)|] ==> c=d"
apply(unfold IsARoot_def)
apply(insert IsA_antisym_rule)
apply(auto)
done



theorem IsAI_refl: "(ALL c. IsAI(c,c))"
apply(unfold IsAI_def)
apply(rule allI)
apply(insert IsA_refl) 
apply(erule_tac x="c" in allE)
apply(auto)
done

theorem IsA_imp_IsAI: "IsA(c,d) ==> IsAI(c,d)"
apply(unfold IsAI_def)
apply(auto)
done

theorem IsAPr_imp_IsA: "IsAPr(c,d) ==> IsA(c,d)"
apply(unfold IsAPr_def)
apply(erule conjE)
apply(assumption)
done

theorem IsAI_imp_IsAI_imp_IsA_rule: "(ALL e. (IsAI(e,c)-->IsAI(e,d))) ==> IsA(c,d)"
apply(frule_tac x="c" in spec)
apply(insert IsAI_refl)
apply(rotate_tac 2)
apply(erule_tac x="c" in allE)
apply(drule mp)
apply(assumption)
apply(unfold IsAI_def)
apply(rotate_tac 2)
apply(erule disjE)
apply(assumption)
apply(drule_tac c="d" and d="c" in IsA_impl_Id_or_IsAPr)
apply(fold IsAI_def)
apply(safe)
apply(insert IsA_refl)
apply(auto)
apply(drule_tac c="d" and d="c" in IsA_wsp_IsAI_rule)
apply(erule exE)
apply(erule conjE)
apply(erule_tac x="e" in allE)
apply(auto)
apply(drule_tac c="e" and d="c" in IsAPr_imp_IsA)
apply(drule_tac c="e" and d="c" in IsA_imp_IsAI)
apply(auto)
done

lemma  IsAI_imp_IsAI_imp_IsA: "(ALL c d. (ALL e. (IsAI(e,c)-->IsAI(e,d))) --> IsA(c,d))"
apply(insert  IsAI_imp_IsAI_imp_IsA_rule)
apply(auto)
done


lemma ltb3: "(ALL e. (A(e,c) & B(e,d))) ==> (ALL e. A(e,c)) & (ALL e. B(e,d))"
apply(auto)
done

theorem IsAI_iff_IsAI_iff_eq: "(ALL c d. (ALL e. (IsAI(e,c) <-> IsAI(e,d))) <-> c=d)"
apply(clarify)
apply(rule iffI)
prefer 2
apply(auto)
apply(unfold iff_def)
apply(drule ltb3)
apply(rule IsA_antisym_rule)
apply(insert IsAI_imp_IsAI_imp_IsA)
apply(auto)
done

theorem IsA_wsp: "IsAPr(c,d) ==> (EX e. (IsAPr(e,d) & ~(EX f. IsA(f,e) & IsA(f,c))))" 
apply(drule IsA_wsp_IsAI_rule)
apply(clarify)
apply(rule_tac x="e" in exI)
apply(safe)
apply(drule_tac e="f" and c="e" and d="c" in IsA_npo_rule)
apply(auto)
done


theorem IsA_and_IsAI_impl_IsAI: "[|IsA(c,d);IsAI(c,e)|] ==> IsAI(d,e)"
apply(unfold IsAI_def)
apply(safe)
apply(drule_tac e="c" and c="d" and d="e" in IsA_npo_rule)
apply(assumption)
apply(unfold IsAI_def)
apply(auto)
apply(drule_tac c="e" and d="c" and e="d" in IsA_trans_rule)
apply(auto)
done

theorem IsA_and_not_IsAI_impl_not_IsAI: "[|IsA(c,d);~IsAI(d,e)|] ==> ~IsAI(c,e)"
apply(unfold IsAI_def)
apply(safe)
apply(drule_tac e="c" and c="d" and d="e" in IsA_npo_rule)
apply(assumption)
apply(unfold IsAI_def)
apply(auto)
apply(drule_tac c="e" and d="c" and e="d" in IsA_trans_rule)
apply(auto)
done

theorem IsAI_impl_IsA_and_IsA: "IsAI(c,d) ==> IsAO(c,d)"
apply(unfold IsAI_def,unfold IsAO_def)
apply(safe)
apply(insert IsA_refl)
apply(rule_tac x="c" in exI)
apply(force)
apply(rule_tac x="d" in exI)
apply(auto)
done

theorem IsAI_iff_IsAO: "ALL c d. (IsAI(c,d) <-> IsAO(c,d))"
apply(auto)
apply(rule IsAI_impl_IsA_and_IsA)
apply(assumption)
apply(drule IsA_npo_rule1)
apply(assumption)
done

end