Email Gateway (Aug 18 2022 at 14:04): Email Gateway (Aug 18 2022 at 14:04):From: S W <s.wong.731@googlemail.com>
Hi,
I'm testing out a basic proof, so I'm trying to show that given T <= 2, then
T <= 1.
I'm using axioms for Naturals and I have the following:
axioms
X1_def_Nat: "1'' = suc'(0'')"
X2_def_Nat: "2'' = suc'(1'')"
ax1: "T <='' 1''"
leq_def1_Nat : "0'' <='' X_n"
dvd_def_Nat : "(m dvd' X_n) = (EX k. X_n = m *'' k)"
leq_def2_Nat: "~ suc'(X_n) <='' 0''"
leq_def3_Nat:"(suc'(m) <='' suc'(X_n)) = (m <='' X_n)"
geq_def_Nat : "(m >='' X_n) = (X_n <='' m)"
less_def_Nat : "(m <'' X_n) = (m <='' X_n & ~ m = X_n)"
declare leq_def1_Nat [simp]
declare dvd_def_Nat [simp]
declare leq_def2_Nat [simp]
declare leq_def3_Nat [simp]
declare geq_def_Nat [simp]
declare less_def_Nat [simp]
declare greater_def_Nat [simp]
lemma test: "T <='' 2''"
using ax1
apply (simp add: X1_def_Nat X2_def_Nat)
by auto
The subgoal produced after simplification is:
proof (prove): step 2
goal (1 subgoal):
but it can't be solved by auto. Does anyone know what I'm missing?
Thanks for any help
Steve
Last updated: Apr 25 2024 at 16:19 UTC