[isabelle] A basic proof



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):
 1. T <='' suc'(0'') ==> T <='' suc'(suc'(0''))

but it can't be solved by auto. Does anyone know what I'm missing?

Thanks for any help
Steve




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.