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❚

theory InductivelyDefinedTypes : ?LFXI =
	include ?NatExample ❙
		
	theory list_decls > a : type ❘ =
		list: type ❙
    nil: list ❙
    cons: a ⟶ list ⟶ list ❙
  ❚

	reflect list1(a: type) : ☞?InductivelyDefinedTypes/list_decls(a:type) ❙

  inductive list1_unreflected(a: type) ❘ =
    list: type ❙
    nil: list ❙
    cons: a ⟶ list ⟶ list ❙
  ❚
	
	inductive_definition concat(a:type) : list1(a: type) ❘ =
		list : type ❘ = list1/list a⟶ list1/list a ❙
		nil : list ❘ = [l] l ❙
		cons : {x: a, f: list, l: list1/list a} list1/list a ❘ = [x, f, l] (list1/cons a x (f l)) ❙
	❚

	single: {a : type} a ⟶ list1/list a ❘ = [a, x] list1/cons a x (list1/nil a) ❙
	inductive_definition reverse(a: type) : list1(a:type) ❘ =
		list : type ❘ = list1/list a❙
		nil : list ❘ = list1/nil a❙
		cons : {x: a, xs: list} list ❘ = [x, xs] concat/list a xs (single a x) ❙
	❚

	inductive_definition length(a: type) : list1(a:type) ❘ =
		list: type ❘ = nats/n ❙
		nil: list ❘ = nats/z ❙
		cons: {x: a, l:list} list ❘ = [x, l] nats/s l ❙
	❚

// length: {a : type} list1/list a ⟶ nat/n ❘ = [a, l] (list1/induct/list a ([tp:type] nat/n) ([tp:type] nat/z) ([tp:type, x:tp, xs:nat/n] nat/s xs)) l ❙

	record pair(A: type, B: type) ❘ = 
		a: A ❙
		b: B ❙
	❚
	product_type: type ⟶ type ⟶ type ❘ # 1 * 2 prec 10 ❘ = [a, b] pair/Type a b ❙
	record_term pairs(A: type, B: type, x: A, y: B) : pair(A, B) ❘ = 
		a: A ❘ = x ❙
		b: B ❘ = y ❙
	❚
	pair_term: {a: type, b: type} a ⟶ b ⟶ a * b ❘ = [a, b, x, y] pairs/Make a b x y ❙

	inductive vector(a: type) ❘ =
		vec: {n: nat/n} type ❙
		empty: vec nat/z ❙
		add: {n: nat/n} vec n ⟶ a ⟶ vec (nat/s n) ❙
	❚

	// ind_vec: {a: type, vecP: {a:type}{n: nat/n} type, emptyP: {a: type} (vecP a) nat/z, addP: {a: type}{n: nat/n}(vecP a) n ⟶ (a ⟶ (vecP a) (nat/s n)), n: nat/n} (vector/vec a) n ⟶ (vecP a) n ❘ = [a, vecP, emptyP, addP, n, l] ([ys] (vector/induct/vec a vecP emptyP addP n l) ys) ❙
	inductive_definition zip(a: type, b: type) : vector(a) ❘ =
		vec: {n: nat/n} type ❘ = [n] vector/vec b n  ⟶ vector/vec (a*b) n ❙
		empty: vec nat/z ❘ = [l] vector/empty (a*b) ❙
		add: {n: nat/n} vec n ⟶ a ⟶ vec (nat/s n) ❘ = [n, xs, x] vector/induct/vec b ([t, p] vector/vec (a*t) p) ([t] vector/empty (a*t)) ([t, p, ys, y] vector/add (a*t) p ys (pair_term a t x y)) (nat/s n) ❙
	❚

	inductive list2() ❘ =
		list: type ⟶ type ❙
		nil: {a: type} list a ❙
		cons: {a: type} a ⟶ list a ⟶ list a ❙
		length2: {a:type} list a ⟶ nat/n ❙
		length2_nil: {a: type} DED (length2 a (nil a) EQ nat/z) ❙
		length2_cons: {a:type, hd: a, tl: list a} DED length2 a (cons a hd tl) EQ nat/s (length2 a tl) ❙
	❚
	
	inductive list3(a : type) ❘ =
		list: type ❙
		nil: list ❙
		cons: {hd: a, tl:list} list  ❘ # 1 ∷ 2 ❙
		head: {l:list, P:DED (l NEQ nil)} a ❙
		head_cons: {hd: a, tl: list, P: DED (cons hd tl NEQ nil)} DED ((head (cons hd tl) P) EQ hd) ❙
	❚

	cons_nonempty: {a:type, hd:a, tl:list3/list a} DED (hd ∷ tl) NEQ list3/nil a ❘ = [a, hd, tl] list3/no_conf_cons_nil a hd tl ❙
	// seems to be an universe issue
	head_cons: {a : type, hd: a, tl:list3/list a} DED (list3/head a (list3/cons a hd tl) (list3/no_conf_cons_nil a hd tl)) EQ hd ❘ = [a, hd, tl] list3/head_cons a hd tl (list3/no_conf_cons_nil a hd tl) ❙

	inductive FM(a: type) ❘ =
		fm: type ❙
		gen: a ⟶ fm ❙
		unit: fm ❙
		comp: fm ⟶ fm ⟶ fm ❘ # 1 . 2 ❙
		assoc: {x: fm, y: fm, z: fm} DED comp (comp x y) z EQ comp x (comp y z) ❙
		unit_r: {x: fm} DED comp x unit EQ x ❙
		unit_l: {x: fm} DED comp unit x EQ x ❙
	❚
❚