(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/exp".
+set "baseuri" "cic:/matita/library_autobatch/nat/exp".
include "auto/nat/div_and_mod.ma".
[ O \Rightarrow (S O)
| (S p) \Rightarrow (times n (exp n p)) ].
-interpretation "natural exponent" 'exp a b = (cic:/matita/library_auto/nat/exp/exp.con a b).
+interpretation "natural exponent" 'exp a b = (cic:/matita/library_autobatch/nat/exp/exp.con a b).
theorem exp_plus_times : \forall n,p,q:nat.
n \sup (p + q) = (n \sup p) * (n \sup q).
intros.
-elim p;simplify;auto.
+elim p;simplify;autobatch.
(*[ rewrite < plus_n_O.
reflexivity
| rewrite > H.
theorem exp_n_O : \forall n:nat. S O = n \sup O.
intro.
-auto.
+autobatch.
(*simplify.
reflexivity.*)
qed.
theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
intro.
-auto.
+autobatch.
(*simplify.
rewrite < times_n_SO.
reflexivity.*)
(n \sup p) \sup q = n \sup (p * q).
intros.
elim q;simplify
-[ auto.
+[ autobatch.
(*rewrite < times_n_O.
simplify.
reflexivity*)
| rewrite > H.
rewrite < exp_plus_times.
- auto
+ autobatch
(*rewrite < times_n_Sm.
reflexivity*)
]
theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m.
intros.
-elim m;simplify;auto.
+elim m;simplify;autobatch.
(*unfold lt
[ apply le_n
| rewrite > times_n_SO.
[ simplify.
rewrite < plus_n_Sm.
apply le_S_S.
- auto
+ autobatch
(*apply le_S_S.
rewrite < sym_plus.
apply le_plus_n*)
- | auto
+ | autobatch
(*apply le_times;assumption*)
]
]
apply antisym_le
[ apply le_S_S_to_le.
rewrite < H1.
- auto
+ autobatch
(*change with (m < n \sup m).
apply lt_m_exp_nm.
assumption*)
intros 4.
apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y))
[ intros.
- auto
+ autobatch
(*apply sym_eq.
apply (exp_to_eq_O n)
[ assumption
(* esprimere inj_times senza S *)
cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b)
[ apply Hcut
- [ auto
+ [ autobatch
(*simplify.
unfold lt.
apply le_S_S_to_le.
apply le_S.
assumption*)
- | (*NB qui auto non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
+ | (*NB qui autobatch non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
assumption
]
| intros 2.
- apply (nat_case n);intros;auto
+ apply (nat_case n);intros;autobatch
(*[ apply False_ind.
apply (not_le_Sn_O O H3)
| apply (inj_times_r m1).