; $Id: listrev.scm 2299 2008-09-25 14:21:01Z schwicht $
(if (not (assoc "nat" ALGEBRAS))
    (myerror "First execute (libload \"nat.scm\")"))

(display "loading listrev.scm ...") (newline)

(add-param-alg "list" 'prefix-typeop
	       '("Nil" "list")
	       '("Cons" "list=>alpha1=>list"))

; Notice that listrev.scm and list.scm cannot be loaded together.
; Reason: In :0::1::2::3 the ":" is a prefix-op (for listrev.scm), but
; in 3::2::1::0: the ":" is a postfix-op (for list.scm).

; Infix notation allowed (and type parameters omitted) for binary 
; constructors, as follows.  This would also work for prefix notation.
; Example: :: for Cons.  :z::y::x
; Here : is prefix for z

(add-token
 "::" 'add-op ;hence left associative
 (lambda (xs x)
   (let ((type (term-to-type x))
	 (listtype (term-to-type xs)))
     (if (and (alg-form? listtype)
	      (string=? "list" (alg-form-to-name listtype))
	      (equal? type (car (alg-form-to-types listtype))))
	 (mk-term-in-app-form
	  (make-term-in-const-form
	   (let* ((constr (constr-name-to-constr "Cons"))
		  (tvars (const-to-tvars constr))
		  (subst (make-substitution tvars (list type))))
	     (const-substitute constr subst #f)))
	  xs x)
	 (myerror "parse error" "types do not fit for" listtype "::" type)))))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "Cons"
			    (const-to-name (term-in-const-form-to-const op)))
		  (= 2 (length args)))
	     (list 'add-op "::"
		   (term-to-token-tree (car args))
		   (term-to-token-tree (cadr args)))
	     #f))
       #f)))

(add-token
 ":" 'prefix-op
 (lambda (x)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((constr (constr-name-to-constr "Cons"))
	    (tvars (const-to-tvars constr))
	    (subst (make-substitution tvars (list (term-to-type x)))))
       (const-substitute constr subst #f)))
    (make-term-in-const-form
     (let* ((constr (constr-name-to-constr "Nil"))
	    (tvars (const-to-tvars constr))
	    (subst (make-substitution tvars (list (term-to-type x)))))
       (const-substitute constr subst #f)))
    x)))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let* ((op (term-in-app-form-to-final-op x))
	      (args (term-in-app-form-to-args x))
	      (revargs (reverse args)))
	 (if (and (term-in-const-form? op)
		  (string=? "Cons" (const-to-name
				    (term-in-const-form-to-const op)))
		  (= 2 (length args))
		  (term-in-const-form? (cadr revargs))
		  (string=? "Nil" (const-to-name
				   (term-in-const-form-to-const
				    (cadr revargs)))))
	     (list 'prefix-op ":" (term-to-token-tree (car revargs)))
	     #f))
       #f)))

(add-program-constant
 "ListAppend" (py "list alpha=>list alpha=>list alpha"))

(add-token
 ":+:" 'mul-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((const (pconst-name-to-pconst "ListAppend"))
	    (tvars (const-to-tvars const))
	    (listtype (term-to-type x))
	    (type (car (alg-form-to-types listtype)))
	    (subst (make-substitution tvars (list type))))
       (const-substitute const subst #f)))
    x y)))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "ListAppend"
			    (const-to-name (term-in-const-form-to-const op)))
		  (= 2 (length args)))
	     (list 'mul-op ":+:"
		   (term-to-token-tree (car args))
		   (term-to-token-tree (cadr args)))
	     #f))
       #f)))

(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))

(add-computation-rule
 (pt "xs1:+:(Nil alpha)")
 (pt "xs1"))

(add-computation-rule
 (pt "xs1:+:(xs2::x3)")
 (pt "xs1:+:xs2::x3"))

; "ListAppendTotal"
(set-goal (pf "Total(ListAppend alpha)"))
(use "Total")
(use-with "All-AllPartial" (py "list alpha")
	  (make-cterm (pv "xs^") (pf "Total((ListAppend alpha)xs^)"))
	  "?")
(assume "xs1")
(use "Total" 'right)
(use-with "All-AllPartial"  (py "list alpha")
	  (make-cterm (pv "xs^") (pf "Total(xs1:+:xs^)"))
	  "?")
(ind)

; Base
(ng)
(use-with
 "AllPartial-All" (py "list alpha") (make-cterm (pv "xs^") (pf "Total xs^"))
 "?" (pt "xs1"))
(assume "xs^" "H1")
(use "H1")

; Step
(assume "xs" "x" "IH")
(ng)
(use-with (make-proof-in-aconst-form
	   (constr-name-to-constr-total-aconst "Cons"))
	  (py "alpha") (pt "xs1:+:xs") (pt "x") "IH" "?")
(use-with
 "AllPartial-All" (py "alpha") (make-cterm (pv "x^") (pf "Total x^"))
 "?" (pt "x"))
(assume "x^" "H1")
(use "H1")
; Proof finished.
(save "ListAppendTotal")


; "ListAppendNil"
(set-goal (pf "all xs Equal((Nil alpha):+:xs)xs"))
(ind)
(use "Eq-Refl")
(assume "xs" "x" "IH")
(ng)
(simp "IH")
(use "Eq-Refl")
; Proof finished.
(save "ListAppendNil")

(add-rewrite-rule (pt "(Nil alpha):+:xs") (pt "xs"))


; ; "ListAppendNilPartial"
; (set-goal (pf "all xs^(STotal xs^ -> Equal((Nil alpha):+:xs^)xs^)"))
; (ind)
; (use "Eq-Refl")
; (assume "xs^" "x^" "SE xs^" "IH")
; (ng)
; (simp "IH")
; (use "Eq-Refl")
; ; Proof finished.
; (save "ListAppendNilPartial")


(add-program-constant "ListLength" (py "list alpha=>nat") t-deg-zero)

(add-token
 "Lh" 'prefix-op 
 (lambda (x) (make-term-in-app-form
	      (make-term-in-const-form
	       (let* ((const (pconst-name-to-pconst "ListLength"))
		      (tvars (const-to-tvars const))
		      (listtype (term-to-type x))
		      (type (car (alg-form-to-types listtype)))
		      (subst (make-substitution tvars (list type))))
		 (const-substitute const subst #f)))
	      x)))

(add-display
 (py "nat")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-op x)))
	 (if (and (term-in-const-form? op)
		  (string=? "ListLength"
			    (const-to-name (term-in-const-form-to-const op))))
	     (list 'prefix-op "Lh"
		   (term-to-token-tree (term-in-app-form-to-arg x)))
	     #f))
       #f)))

(add-computation-rule (pt "Lh(Nil alpha)") (pt "Zero"))
(add-computation-rule (pt "Lh(xs::x)") (pt "Succ Lh xs"))


; "ListLengthTotal"
(set-goal (pf "Total(ListLength alpha)"))
(use "Total")
(use-with "All-AllPartial" (py "list alpha")
	  (make-cterm (pv "xs^") (pf "Total((ListLength alpha)xs^)"))
	  "?")
(ind)
; Base
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "nat"))))
(use "Truth-Axiom")
; Step
(assume "xs" "x" "IH")
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "nat"))))
(ng)
(use (make-proof-in-aconst-form (finalg-to-total-to-e-aconst (py "nat"))))
(use "IH")
; Proof finished.
(save "ListLengthTotal")


; "LhAppend"
(set-goal (pf "all xs1,xs2 Lh(xs1:+:xs2)=Lh xs1+Lh xs2"))
(assume "xs1")
(ind)
; Base
(ng)
(use "Truth-Axiom")
; Step
(assume "xs2" "x" "IH")
(ng)
(simp "IH")
(use "Truth-Axiom")
; Proof finished.
(save "LhAppend")

(add-rewrite-rule (pt "Lh(xs1:+:xs2)") (pt "Lh xs1+Lh xs2"))


; Now for projection ListProj.  We use the rule (Nil alpha)__n ->
; (Inhab alpha)

(add-program-constant
 "ListProj" (py "list alpha=>nat=>alpha") t-deg-zero 'const 1)

(add-token
 "__" 'mul-op ;hence left associative
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((const (pconst-name-to-pconst "ListProj"))
	    (tvars (const-to-tvars const))
	    (listtype (term-to-type x))
	    (type (car (alg-form-to-types listtype)))
	    (subst (make-substitution tvars (list type))))
       (const-substitute const subst #f)))
    x y)))

(add-display
 (py "alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "ListProj"
			    (const-to-name (term-in-const-form-to-const op)))
		  (= 2 (length args)))
	     (list 'mul-op "__"
		   (term-to-token-tree (car args))
		   (term-to-token-tree (cadr args)))
	     #f))
       #f)))

(add-token
 "Proj" 'prefix-op
 (lambda (x) (make-term-in-app-form
	      (make-term-in-const-form
	       (let* ((const (pconst-name-to-pconst "ListProj"))
		      (tvars (const-to-tvars const))
		      (listtype (term-to-type x))
		      (type (car (alg-form-to-types listtype)))
		      (subst (make-substitution tvars (list type))))
		 (const-substitute const subst #f)))
	      x)))

(add-display
 (py "nat=>alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "ListProj"
			    (const-to-name (term-in-const-form-to-const op)))
		  (= 1 (length args)))
	     (list 'prefix-op "Proj"
		   (term-to-token-tree (car args)))
	     #f))
       #f)))

(add-computation-rule (pt "Proj(Nil alpha)") (pt "[nat](Inhab alpha)"))

(add-computation-rule
 (pt "Proj(xs::x)")
 (pt "[n][if (n<Lh xs) (xs__n)
             [if (n=Lh xs) x (Inhab alpha)]]"))

; (pp (nt (pt "(:0::1::2::3)__1")))
; 1
; (pp (nt (pt "(:True::True::False::True)__1")))
; True
; (pp (nt (pt "(Nil boole)__27")))
; (Inhab boole)

; "ListProjTotal"
(set-goal (pf "Total(ListProj alpha)"))
(use "Total")
(use-with "All-AllPartial" (py "list alpha")
	  (make-cterm (pv "xs^") (pf "Total(Proj xs^)"))
	  "?")
(ind)
; Base
(ng)
(use "Total")
(use "All-AllPartial")
(ng)
(assume "n")
; ?_10: Total(Inhab alpha)
(use "InhabTotal")

; Step
(assume "xs" "x" "IH")
(ng)
(use "Total")
(use "All-AllPartial")
(assume "n")
(ng)
(cases (pt "n<Lh xs"))
(assume "n<Lh xs")
(ng)
(use "Total")
(use "IH")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "nat"))))
(ng)
(use "Truth-Axiom")
(assume "n<Lh xs -> F")
(ng)
(cases (pt "n=Lh xs"))
(assume "n=Lh xs")
(ng)
(use-with
 "AllPartial-All" (py "alpha") (make-cterm (pv "x^") (pf "Total x^"))
 "?" (pt "x"))
(assume "x^" "H1")
(use "H1")
(assume "n=Lh xs -> F")
(ng)
(use "InhabTotal")
; Proof finished.
(save "ListProjTotal")

(add-program-constant
 "ListFBar" (py "(nat=>alpha)=>nat=>list alpha") t-deg-zero)

(add-token
 "fbar" 'pair-op ;hence right associative
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((const (pconst-name-to-pconst "ListFBar"))
	    (tvars (const-to-tvars const))
	    (fcttype (term-to-type x))
	    (type (car (alg-form-to-types fcttype)))
	    (subst (make-substitution tvars (list type))))
       (const-substitute const subst #f)))
    x y)))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "ListFBar"
			    (const-to-name (term-in-const-form-to-const op)))
		  (= 2 (length args)))
	     (list 'pair-op "fbar"
		   (term-to-token-tree (car args))
		   (term-to-token-tree (cadr args)))
	     #f))
       #f)))

(add-computation-rule (pt "nat=>alpha fbar 0") (pt "(Nil alpha)"))

(add-computation-rule (pt "nat=>alpha fbar Succ n")
		      (pt "(nat=>alpha fbar n)::(nat=>alpha n)"))

; (pp (nt (pt "Succ fbar 4")))
; (pp (nt (pt "([n]n+3)fbar 4")))


; "ListFBarTotal"
(set-goal (pf "Total(ListFBar alpha)"))
(use "Total")
(use-with "All-AllPartial" (py "nat=>alpha")
	  (make-cterm (pv "(nat=>alpha)^")
		      (pf "Total((ListFBar alpha)(nat=>alpha)^)"))
	  "?")
(assume "nat=>alpha")
(use "Total" 'right)
(use-with "All-AllPartial"  (py "nat")
	  (make-cterm (pv "n^") (pf "Total((nat=>alpha)fbar n^)"))
	  "?")
(ind)

; Base
(ng)
(use-with (make-proof-in-aconst-form
	   (constr-name-to-constr-total-aconst "Nil"))
	  (py "alpha"))

; Step
(assume "n" "IH")
(ng)
(use-with (make-proof-in-aconst-form
	   (constr-name-to-constr-total-aconst "Cons"))
	  (py "alpha") (pt "(nat=>alpha)fbar n") (pt "(nat=>alpha)n") "IH" "?")
(use-with
 "AllPartial-All" (py "alpha") (make-cterm (pv "x^") (pf "Total x^"))
 "?" (pt "(nat=>alpha)n"))
(assume "x^" "H1")
(use "H1")
; Proof finished.
(save "ListFBarTotal")


; We use (a bar n) as notation for ((Proj a)fbar n).

(add-token
 "bar" 'add-op ;hence left associative
 (lambda (a n)
   (let* ((listtype (term-to-type a))
	  (type (car (alg-form-to-types listtype)))
	  (projconst (let* ((const (pconst-name-to-pconst "ListProj"))
			    (tvars (const-to-tvars const))
			    (subst (make-substitution tvars (list type))))
		       (const-substitute const subst #f)))
	  (fbarconst (let* ((const (pconst-name-to-pconst "ListFBar"))
			    (tvars (const-to-tvars const))
			    (subst (make-substitution tvars (list type))))
		       (const-substitute const subst #f))))
     (mk-term-in-app-form
      (make-term-in-const-form fbarconst)
      (make-term-in-app-form (make-term-in-const-form projconst)
			     a)
      n))))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if
	  (and (term-in-const-form? op)
	       (string=? "ListFBar" 
			 (const-to-name (term-in-const-form-to-const op)))
	       (= 2 (length args)))
	  (let* ((arg1 (car args))
		 (arg1op (term-in-app-form-to-final-op arg1))
		 (arg1args (term-in-app-form-to-args arg1)))
	    (if
	     (and (term-in-const-form? arg1op)
		  (string=? "ListProj"
			    (const-to-name
			     (term-in-const-form-to-const arg1op)))
		  (= 1 (length arg1args)))
	     (list 'add-op "bar"
		   (term-to-token-tree (car arg1args))
		   (term-to-token-tree (cadr args)))
	     #f))
	  #f))
       #f)))

; (pp (pt "(list boole)bar nat"))
; (pp (pt "Proj(list boole)"))

(set-goal (pf "all (nat=>alpha)^,n Lh((nat=>alpha)^ fbar n)=n"))
(assume "(nat=>alpha)^")
(ind)
(use "Truth-Axiom")
(assume "n" "IH")
(use "IH")

(add-rewrite-rule (pt "Lh((nat=>alpha)^ fbar n)") (pt "n"))


(add-program-constant
 "ListMap" (py "(alpha1=>alpha2)=>list alpha1=>list alpha2") t-deg-zero)

(add-token
 "map" 'pair-op ;hence right associative
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((const (pconst-name-to-pconst "ListMap"))
	    (tvars (const-to-tvars const))
	    (listtype (term-to-type y))
	    (type1 (car (alg-form-to-types listtype)))
	    (type2 (arrow-form-to-val-type (term-to-type x)))
	    (subst (make-substitution tvars (list type1 type2))))
       (const-substitute const subst #f)))
    x y)))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "ListMap"
			    (const-to-name (term-in-const-form-to-const op)))
		  (= 2 (length args)))
	     (list 'pair-op "map"
		   (term-to-token-tree (car args))
		   (term-to-token-tree (cadr args)))
	     #f))
       #f)))

(add-var-name "phi" (py "alpha1=>alpha2"))

(add-computation-rule (pt "phi map(Nil alpha1)") (pt "(Nil alpha2)"))

(add-var-name "y" (py "alpha1"))
(add-var-name "ys" (py "list alpha1"))
(add-var-name "z" (py "alpha2"))
(add-var-name "zs" (py "list alpha2"))

(add-computation-rule (pt "phi map ys::y") (pt "(phi map ys)::phi y"))

; (pp (nt (pt "Pred map :2::3::4")))


; "ListMapTotal"
(set-goal (pf "Total(ListMap alpha1 alpha2)"))
(use "Total")
(use-with "All-AllPartial" (py "alpha1=>alpha2")
	  (make-cterm (pv "phi^") (pf "Total((ListMap alpha1 alpha2)phi^)"))
	  "?")
(assume "phi")
(use "Total" 'right)
(use-with "All-AllPartial" (py "list alpha1")
	  (make-cterm (pv "ys^") (pf "Total(phi map ys^)"))
	  "?")
(ind)

; Base
(ng)
(use-with (make-proof-in-aconst-form
	   (constr-name-to-constr-total-aconst "Nil"))
	  (py "alpha2"))

; Step
(assume "ys" "y" "IH")
(ng)
(use-with (make-proof-in-aconst-form
	   (constr-name-to-constr-total-aconst "Cons"))
	  (py "alpha2") (pt "phi map ys") (pt "phi y") "IH" "?")
(use-with
 "AllPartial-All" (py "alpha2") (make-cterm (pv "z^") (pf "Total z^"))
 "?" (pt "phi y"))
(assume "z^" "H1")
(use "H1")
; Proof finished.
(save "ListMapTotal")


; "LhMap"
(set-goal (pf "all phi,ys Lh(phi map ys)=Lh ys"))
(assume "phi")
(ind)
(use "Truth-Axiom")
(assume "ys" "y" "IH")
(use "IH")
; Proof finished.
(save "LhMap")


; "LhMapPartial"
(set-goal (pf "all phi^,ys^(STotal ys^ -> Lh(phi^ map ys^)=Lh ys^)"))
(assume "phi^")
(ind)
(use "Truth-Axiom")
(assume "ys^" "y^" "SE ys^" "IH")
(use "IH")
; Proof finished.
(save "LhMapPartial")


; "MapAppend"
(set-goal (pf "all phi,ys1,ys2
               Equal(phi map (ys1:+:ys2))((phi map ys1):+:(phi map ys2))"))
(assume "phi" "ys1")
(ind)
(ng)
(use-with "Eq-Refl" (py "list alpha2")(pt "phi map ys1"))
(assume "ys" "y" "IH")
(ng)
(simp "IH")
(use "Eq-Refl")
; Proof finished.
(save "MapAppend")


; "MapAppendPartial"
(set-goal
 (pf "all phi^,ys^1,ys^2(
       STotal ys^2 ->
       Equal(phi^ map (ys^1:+:ys^2))((phi^ map ys^1):+:(phi^ map ys^2)))"))
(assume "phi^" "ys^1")
(ind)
(ng)
(use-with "Eq-Refl" (py "list alpha2")(pt "phi^ map ys^1"))
(assume "ys^" "y^" "SE ys^" "IH")
(ng)
(simp "IH")
(use "Eq-Refl")
; Proof finished.
(save "MapAppendPartial")


; "MapFbar"
(set-goal
 (pf "all (nat=>alpha1)^,phi^,n 
       Equal(phi^ map (nat=>alpha1)^ fbar n)
            (([n]phi^((nat=>alpha1)^ n))fbar n)"))
(assume "(nat=>alpha1)^" "phi^")
(ind)
(use "Eq-Refl")
(assume "n" "IH")
(ng #t)
(simp "IH")
(use "Eq-Refl")
; Proof finished.
(save "MapFbar")

(add-rewrite-rule
 (pt "phi^ map (nat=>alpha1)^ fbar n")
 (pt "([n]phi^((nat=>alpha1)^ n))fbar n"))


; We add a bounded universal quantifier.  AllBList n P means that for
; all lists of length n of booleans the property P holds.

(add-program-constant
 "AllBList" (py "nat=>(list boole=>boole)=>boole") t-deg-zero)

(add-computation-rule (pt "AllBList 0 list boole=>boole")
		      (pt "(list boole=>boole)(Nil boole)"))
(add-computation-rule
 (pt "AllBList(Succ n)list boole=>boole")
 (pt "(AllBList n([list boole]list boole=>boole(list boole::True)))andb
      (AllBList n([list boole]list boole=>boole(list boole::False)))"))


; "AllBListTotal"
(set-goal (pf "Total AllBList"))
(use "Total")
(use "All-AllPartial")
(ind)
; Base
(use "Total" 'right)
(use "All-AllPartial")
(assume "(list boole=>boole)")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "boole"))))
(use "Truth-Axiom")
; Step
(assume "n" "IH")
(use "Total" 'right)
(assume "(list boole=>boole)^" "Tf")
(ng)
(assert (pf "all boole^1(Total boole^1 -> all boole^2(Total boole^2 -> 
                         Total(boole^1 andb boole^2)))"))
  (assume "boole^1" "T1" "boole^2" "T2")
  (use "Total")
  (use "Total")
  (use "AndConstTotal")
  (use "T1")
  (use "T2")
(assume "TA")
(use "TA")
; Case True
(use "Total")
(use "IH")
(use "Total")
(use "All-AllPartial")
(assume "list boole")
(ng)
(use "Total")
(use "Tf")
(use (make-proof-in-aconst-form
      (finalg-to-e-to-total-aconst (py "list boole"))))
(use "Truth-Axiom")
; Case False
(use "Total")
(use "IH")
(use "Total")
(use "All-AllPartial")
(assume "list boole")
(ng)
(use "Total")
(use "Tf")
(use (make-proof-in-aconst-form
      (finalg-to-e-to-total-aconst (py "list boole"))))
(use "Truth-Axiom")
; Proof finished
(save "AllBListTotal")


; "ListLhZero"
(set-goal
 (pf "all xs^(STotal xs^ -> Lh xs^ =0 -> Equal xs^(Nil alpha))"))
(cases)
(assume "H")
(use "Eq-Refl")
(assume "xs^" "x^" "H" "IH")
(use "Efq")
(use "IH")
; Proof finished.
(save "ListLhZero")


; "AllBListIntro"
(set-goal
 (pf "all n,(list boole=>boole)(
       all (list boole)^(
        Lh (list boole)^ =n -> (list boole=>boole) (list boole)^) -> 
       AllBList n (list boole=>boole))"))
(ind)
(assume "(list boole=>boole)")
(ng)
(strip)
(use 1)
(use "Truth-Axiom")
(assume "n" "IH" "(list boole=>boole)" "H")
(ng)
(split)
(use "IH")
(ng)
(assume "(list boole)^" "Lh (list boole)^ =n")
(use "H")
(use "Lh (list boole)^ =n")
(use "IH")
(ng)
(assume "(list boole)^" "Lh (list boole)^ =n")
(use "H")
(use "Lh (list boole)^ =n")
; Proof finished.
(save "AllBListIntro")


; "AllBListElim"
(set-goal
 (pf "all n,(list boole=>boole)(
       AllBList n (list boole=>boole) -> 
       all (list boole)
        (Lh (list boole)=n -> (list boole=>boole)(list boole)))"))
(ind)
(assume "(list boole=>boole)" "H1")
(cases)
(assume "Trivial")
(use "H1")
(assume "list boole" "boole" "Absurd")
(use "Efq")
(use "Absurd")
(assume "n" "IH" "(list boole=>boole)" "H1")
(cases)
(assume "Absurd")
(use "Efq")
(use "Absurd")
(assume "list boole")
(cases)
(use-with "IH"
	  (pt "[(list boole)_1](list boole=>boole)((list boole)_1::True)")
	  "?" (pt "list boole"))
(ng)
(use "H1")
(use-with "IH"
	  (pt "[(list boole)_1](list boole=>boole)((list boole)_1::False)")
	  "?" (pt "list boole"))
(ng)
(use "H1")
; Proof finished.
(save "AllBListElim")

(remove-var-name "x" "xs" "phi" "y" "ys" "z" "zs")