namespace http://cds.omdoc.org/examples ❚

import lfx http://gl.mathhub.info/MMT/LFX/TypedHierarchy ❚
import finite http://gl.mathhub.info/MMT/LFX/Finite ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
import ur http://cds.omdoc.org/urtheories ❚


theory NatManually : ur:?DHOL =
  n: type❙
  z : n❙
  s : n ⟶ n❙
  induct_n : {N:type,Z:N,S:N⟶N} n ⟶ N ❙
  induct_z : {N:type,Z:N,S:N⟶N} DED (induct_n N Z S) z EQ Z ❙
  induct_s : {N:type,Z:N,S:N⟶N,X:n} DED (induct_n N Z S) (s X) EQ S ((induct_n N Z S) X) ❘ # induct_s 4 ❙
  
  p_n: type ❘ = n ⟶ n ❙
  p_z: p_n ❘ = [x] x ❙
  p_s: p_n ⟶ p_n ❘ = [f][x] s (f x) ❙
  
  p_induct_n: n ⟶ p_n ❘ = induct_n p_n p_z p_s ❙
  p_induct_z: DED (induct_n p_n p_z p_s z) EQ p_z ❘ = induct_z ❙
  p_induct_s: {X:n} DED (induct_n p_n p_z p_s (s X)) EQ p_s (induct_n p_n p_z p_s X) ❘
            = [X] induct_s X ❙
  
  N_n : n ⟶ type❘ = [x] DED p_induct_n x z EQ x ❙
  N_z : N_n z❘ = p_induct_z CONG [f:p_n] f z ❙
  N_s : {X:n,hX: N_n X} N_n (s X) ❘
      = [X:n][hX:N_n X] ((induct_s X) CONG [f] f z) TRANS (hX CONG s) ❙
❚

theory NatExample : ?LFXI =
	theory nat_decls_long = 
		n: type ❙
    z: n ❙
    s: n ⟶ n ❙
  ❚

	reflect nat_long() : NatExample/nat_decls_long() ❙
  inductive_definition plusn_long() : nat_long() ❘ =
		n = nat_long/n ⟶ nat_long/n ❙
		z: n ❘ = ([x] x) ❙
		s: n ⟶ n ❘ = ([u,x] nat_long/s (u x)) ❙
  ❚


	theory unital_type =
		n: type ❙
    z: n ❙
  ❚

	theory nat_decls = 
		include ?NatExample/unital_type ❙
    s: n ⟶ n ❙
  ❚
	reflect nat() : NatExample/nat_decls() ❙


  inductive_definition plusn() : nat() ❘ =
		n = nat/n ⟶ nat/n ❙
		z: n ❘ = ([x] x) ❙
		s: n ⟶ n ❘ = ([u,x] nat/s (u x)) ❙
  ❚
	plus: nat/n ⟶ nat/n ⟶ nat/n ❘ = plusn/n ❘ # 1 + 2 prec 100 ❙

	ind_proof z_left_neutral() : nat() ❘=
		n = [m] DED (nat/z + m) EQ m ❙
		z = plusn/z/Applied nat/z ❙
		s : {x:nat/n} n x ⟶ n (nat/s x) ❘ = [x, px] plusn/z/Applied (nat/s x) ❙
  ❚

	ind_proof z_right_neutral() : nat() ❘=
		n = [m] DED m EQ (m + nat/z) ❙
		z = SYM (plusn/z/Applied nat/z) ❙
		s : {x:nat/n} n x ⟶ n (nat/s x) ❘ = [x, px] (px CONG nat/s) TRANS (SYM (plusn/s/Applied x nat/z)) ❙
  ❚

	ind_proof suc_comm() : nat() ❘=
	 	n = [a:nat/n, b:nat/n] DED (nat/s a) + b EQ a + (nat/s b) ❙
	 	z : {b:nat/n} n nat/z b ❘ = [b] ((plusn/s/Applied nat/z b) TRANS ((plusn/z/Applied b) CONG nat/s)) TRANS (SYM (plusn/z/Applied (nat/s b))) ❙
	 	s : {a:nat/n, b: nat/n} n a b ⟶ n (nat/s a) b ❘ = [a: nat/n, b: nat/n, pa: n a b] ((plusn/s/Applied (nat/s a) b) TRANS (pa CONG nat/s)) TRANS (SYM (plusn/s/Applied a (nat/s b))) ❙
  ❚

	ind_proof plus_comm() : nat() ❘ =
		n = [a:nat/n, b:nat/n] DED a + b EQ b + a ❙
		z : {b: nat/n} n nat/z b ❘ = [b] (z_left_neutral/n b) TRANS (z_right_neutral/n b) ❙
		s : {a:nat/n, b: nat/n, pa: n a b} n (nat/s a) b ❘ = [a, b, pa] ((plusn/s/Applied a b) TRANS (pa CONG nat/s))
			 TRANS ((SYM (plusn/s/Applied b a)) TRANS (suc_comm/n b a)) ❙ 
	❚

	ind_proof plus_assoc() : nat() ❘ =
		n : {b:nat/n, a:nat/n, c:nat/n} type ❘ = [b, a, c] DED a + (b + c) EQ (a + b) + c ❙
		z : {a, c} n nat/z a c ❘ = [a, c]  (z_left_neutral/n c CONG ([x] a + x)) TRANS (z_right_neutral/n a CONG ([x] x + c)) ❙
		s : {b, a, c, pb: n b a c} n (nat/s b) a c ❘ = [b, a, c, pb] ((((plusn/s/Applied b c) CONG ([x] a + x)) TRANS (SYM (suc_comm/n a (b+c)))) TRANS (plusn/s/Applied a (b+c)))
			TRANS ((pb CONG nat/s) TRANS (SYM ((((SYM (suc_comm/n a b)) TRANS (plusn/s/Applied a b)) CONG ([x] x + c)) TRANS (plusn/s/Applied (a+b) c)))) ❙
	❚

	inductive_definition times() : nat() ❘=
		n: type ❘ = (nat/n ⟶ nat/n) ❙
    z: n ❘ = ([x] nat/z) ❙
    s: n ⟶ n ❘ = ([u,x] (x + (u x))) ❙
  ❚

	timesn: nat/n ⟶ nat/n ⟶ nat/n ❘ = [a, b] times/n a b ❘ # 1 * 2 prec 101 ❙ 
	
	ind_proof times_z() : nat() ❘ =
		n : {a:nat/n} type ❘ = [a] DED a * nat/z EQ nat/z ❙
		z : n nat/z ❘ = times/z/Applied nat/z ❙
		s : {a:nat/n, pa: n a} n (nat/s a) ❘ = [a, pa] (times/s/Applied a nat/z) TRANS (plusn/z/Applied (a * nat/z)) TRANS pa  ❙
	❚
	
	ind_proof times_right() : nat() ❘ =
		n : {b:nat/n, a:nat/n} type ❘ = [b, a] DED b + b * a EQ b * (nat/s a) ❙
		z : {a: nat/n} n nat/z a ❘ = [a] ((plusn/z/Applied (nat/z * a)) TRANS (times/z/Applied a)) TRANS SYM (times/z/Applied (nat/s a)) ❙
		s : {b:nat/n, a:nat/n, pb: n b a} n (nat/s b) a ❘ = [b, a, pb] 
						(((plusn/s/Applied b ((nat/s b)*a)) TRANS ((times/s/Applied b a) CONG ([x] nat/s (b + x))))
			TRANS (((plus_assoc/n a b (b*a)) CONG nat/s) TRANS ((plus_comm/n b a) CONG ([x] nat/s (x + (b*a))))))
			TRANS (((SYM (plusn/s/Applied (a+b) (b*a))) TRANS ((SYM (plusn/s/Applied a b)) CONG ([x] x + (b*a))))
			TRANS ((SYM (plus_assoc/n b (nat/s a) (b*a))) TRANS ((pb  CONG ([x] (nat/s a) + x)) TRANS (SYM (times/s/Applied b (nat/s a))))))  ❙
	❚

	ind_proof distrib_left() : nat() ❘ =
		n : {a:nat/n, b:nat/n, c:nat/n} type ❘ = [a, b, c] DED (a + b) * c EQ a*c + b*c ❙
		z : {b:nat/n, c:nat/n} n nat/z b c ❘ = [b, c] ((plusn/z/Applied b) CONG ([x] x * c)) TRANS (SYM ((times/z/Applied c) CONG ([x] x+ (b*c)) TRANS (plusn/z/Applied (b*c)))) ❙
		s = [a, b, c, pa] ((((plusn/s/Applied a b) CONG ([x] x * c)) TRANS (times/s/Applied (a+b) c)) TRANS (pa CONG ([x] c + x))) TRANS ((plus_assoc/n (a*c) c (b*c)) TRANS (SYM ((times/s/Applied a c) CONG ([x] x + b*c)))) ❙
	❚

	ind_proof times_comm() : nat() ❘ =
		n = [a, b] DED a * b EQ b * a ❙
		z = [x] times_z/n x ❙
	  s = [a, b, pa:n a b] ((times/s/Applied a b) TRANS (pa CONG ([x] b + x))) TRANS (times_right/n b a) ❙
	❚

	left_distrib: {a:nat/n, b:nat/n, c:nat/n} DED (a + b) * c EQ a*c + b*c ❘ = [a, b, c] distrib_left/n a b c ❙
	right_distrib: {a:nat/n, b:nat/n, c:nat/n} DED a * (b + c) EQ a*b + a*c ❘ = [a, b, c] ((times_comm/n a (b+c)) TRANS (distrib_left/n b c a)) TRANS (((times_comm/n b a) CONG ([x] x + (c*a))) TRANS (times_comm/n c a CONG ([x] (a*b) + x))) ❙

	ind_proof times_assoc() : nat() ❘ =
		n = [a, b, c] DED a * (b * c) EQ (a * b) * c ❙
		z = [b, c] (times/z/Applied (b*c)) TRANS (SYM (((times/z/Applied b) CONG ([x] x * c)) TRANS (times/z/Applied c))) ❙
		s = [a, b, c, pa] ((times/s/Applied a (b*c)) TRANS (pa CONG ([x] (b*c) + x))) TRANS (SYM (((times/s/Applied a b) CONG ([x] x * c)) TRANS (distrib_left/n b (a*b) c)))  ❙
	❚

	inductive_definition predec() : nat() ❘ =
		n: type ❘ = nat/n ❙
		z: n ❘ = nat/z ❙
		s: n ⟶ n ❘ = ([u] u) ❙
  ❚
	
  inductive_definition monus() : nat() ❘ =
		n: type ❘ = (nat/n ⟶ nat/n) ❙
		z: n ❘ = ([x] x) ❙
		s: n ⟶ n ❘ = ([u,x] predec/n (u x)) ❙
  ❚

❚