(* 
クイックソート関数の正当性（完全帰納法の使用例）
*)

(********************)
(* qsort            *)
(********************)

val qsort_defn = Hol_defn "qsort"
    `(qsort [] = []) /\
    (qsort (x::l) =
     APPEND (qsort (FILTER (\y. y < x) l))
     (x :: qsort (FILTER (\y. ~(y < x)) l)))`;;
val LENGTH_FILTER = prove
    (``!P l. LENGTH (FILTER P l) < SUC (LENGTH l)``, 
     GEN_TAC THEN
     Induct_on `l` THEN
     RW_TAC list_ss [listTheory.FILTER]);;
val qsort = 
    #1(Defn.tprove 
       (qsort_defn,
	WF_REL_TAC `measure LENGTH` THEN
	RW_TAC list_ss [LENGTH_FILTER]));;



(********************)
(* correctness      *)
(********************)

val SPLIT1 = Define
    `(SPLIT1 x l1 [] = (l1,[])) /\
    (SPLIT1 x l1 (y::l2) = if x = y then (l1,l2)
			   else SPLIT1 x (APPEND l1 [y]) l2)`;;
val SPLIT = Define 
    `SPLIT x l = SPLIT1 x [] l`;;


val ordered_pre = Define 
    `ordered_pre l = 
    !x. MEM x l ==> EVERY (\y. y <= x) (FST (SPLIT x l))`;;
val ordered_post = Define 
    `ordered_post l = 
    !x. MEM x l ==> EVERY (\y. x <= y) (SND (SPLIT x l))`;;
val ordered = Define 
    `ordered l = ordered_pre l /\ ordered_post l`;;



(********************)
(* proof            *)
(********************)


val FILTER = listTheory.FILTER;;
val APPEND_APPEND = prove
      (``!l1 l2 l3. APPEND (APPEND l1 l2) l3 = APPEND l1 (APPEND l2 l3)``,
       RW_TAC list_ss []);;


val EVERY_IMP_EVERY_FILTER = prove
    (``!P Q l. EVERY P l ==> EVERY P (FILTER Q l)``,
     Induct_on `l` THEN
     RW_TAC list_ss [FILTER]);;
val EVERY_FILTER = prove
    (``!P Q l. (!x. Q x ==> P x) ==> EVERY P (FILTER Q l)``, 
     GEN_TAC THEN GEN_TAC THEN
     Induct_on `l` THEN
     RW_TAC list_ss [FILTER]);;
val EVERY_FILTER_lemma1 = prove
    (``!P l. 
     EVERY P (FILTER (\y. y < h) l) /\
     EVERY P (FILTER (\y. ~(y < h)) l) ==> EVERY P l``,
     GEN_TAC THEN
     Induct_on `l` THEN
     RW_TAC list_ss [FILTER]);;
val EVERY_FILTER_lemma2 = prove
    (``!x h l. ~(x < h) ==> 
	 EVERY (\y. y <= x) (FILTER (\y. y < h) l)``,
     Induct_on `l` THEN
     RW_TAC list_ss [FILTER]);;
val EVERY_FILTER_lemma3 = prove
    (``!h l. EVERY (\y. y <= h) (FILTER (\y. y < h) l)``,
     Induct_on `l` THEN
     RW_TAC list_ss [FILTER]);;
val EVERY_FILTER_lemma4 = prove
      (``!x h l. x < h ==>
	   EVERY (\y. x <= y) (FILTER (\y. ~(y < h)) l)``,
       Induct_on `l` THEN
       RW_TAC list_ss [FILTER]);;
val EVERY_FILTER_lemma5 = prove
      (``!h l. EVERY (\y. h <= y) (FILTER (\y. ~(y < h)) l)``,
       Induct_on `l` THEN
       RW_TAC list_ss [FILTER]);;


val MEM_FILTER = prove
    (``!x P l. MEM x (FILTER P l) = MEM x l /\ P x``,
     Induct_on `l` THENL
     [RW_TAC list_ss [FILTER],
      RW_TAC list_ss [FILTER] THEN
      PROVE_TAC []]);;
val MEM_FILTER_lemma1 = prove
    (``!h l. ~(MEM h (FILTER (\y. y < h) l))``,
     RW_TAC list_ss [MEM_FILTER]);;
val MEM_FILTER_lemma2 = prove
    (``!x h l. ~(x < h) ==> ~(MEM x (FILTER (\y. y < h) l))``,
     RW_TAC list_ss [MEM_FILTER]);;
val MEM_FILTER_lemma3 = prove
    (``!x h l. MEM x l /\ ~(x < h) ==> 
	 MEM x (FILTER (\y. ~(y < h)) l)``,
     RW_TAC list_ss [MEM_FILTER]);;
val MEM_FILTER_lemma4 = prove
      (``!x h l. MEM x l /\ (x < h) ==> 
	   MEM x (FILTER (\y. y < h) l)``,
       RW_TAC bool_ss [MEM_FILTER]);;


val SPLIT1_lemma = prove
    (``!(x:'a) l1 l2. SPLIT1 x l1 l2 = 
     let (l3,l4) = SPLIT1 x [] l2 in 
	 (APPEND l1 l3,l4)``,
     PAIR_TAC ``SPLIT1 (x:'a) [] l2`` THEN
     LETR_TAC THEN
     Induct_on `l2` THENL
     [RW_TAC list_ss [SPLIT1],
      ONCE_REWRITE_TAC [SPLIT1] THEN
      REPEAT STRIP_TAC THEN
      Cases_on `x = h` THENL
      [ONCE_ASM_REWRITE_TAC [] THEN
       SIMP_TAC list_ss [],
       ONCE_ASM_REWRITE_TAC [] THEN
       SIMP_TAC list_ss [] THEN
       R_TAC [APPEND_APPEND] THEN
       SIMP_TAC list_ss []]]);;
val SPLIT_APPEND = prove
    (``!x l1 l2.
     ~(MEM x l1) ==>
	 (SPLIT x (APPEND l1 (x::l2)) = (l1,l2))``,
     Induct_on `l1` THENL
     [RW_TAC list_ss [] THEN
      R_TAC [SPLIT,SPLIT1],
      RW_TAC list_ss [] THEN
      R_TAC [SPLIT] THEN
      R_TAC [SPLIT1] THEN
      RW_TAC list_ss [] THEN
      RES_TAC THEN
      ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
      R_TAC [SPLIT] THEN
      DISCH_TAC THEN
      ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
      PAIR_TAC ``SPLIT1 x [] (APPEND l1 (x::l2))`` THEN
      LETR_TAC THEN
      RW_TAC list_ss []]);;


val MEM_qsort = prove
    (``!x l. MEM x (qsort l) = MEM x l``,
     REPEAT GEN_TAC THEN
     completeInduct_on `LENGTH l` THEN
     Induct_on `l` THENL
     [RW_TAC list_ss [qsort],
      RW_TAC list_ss [qsort] THEN
      ASSUM_LIST (fn thl => ASSUME_TAC
		  (REWRITE_RULE [LENGTH_FILTER]
		   (SPEC ``LENGTH (FILTER (\y. y < h) l)`` (el 2 thl)))) THEN
      ASSUM_LIST (fn thl => ASSUME_TAC 
		  (REWRITE_RULE []
		   (SPEC ``FILTER (\y. y < h) l`` (el 1 thl)))) THEN
      ASSUM_LIST (fn thl => ASSUME_TAC
		  (REWRITE_RULE [LENGTH_FILTER]
		   (SPEC ``LENGTH (FILTER (\y. ~(y < h)) l)`` (el 4 thl)))) THEN
      ASSUM_LIST (fn thl => ASSUME_TAC 
		  (REWRITE_RULE []
		   (SPEC ``FILTER (\y. ~(y < h)) l`` (el 1 thl)))) THEN
      RW_TAC list_ss [] THEN
      RW_TAC list_ss [MEM_FILTER] THEN
      EQ_TAC THENL
      [RW_TAC bool_ss [] THEN RW_TAC bool_ss [],
       RW_TAC bool_ss [] THEN RW_TAC arith_ss []]]);;


val EVERY_qsort = prove
    (``!P l. EVERY P (qsort l) = EVERY P l``,
     REPEAT GEN_TAC THEN
     completeInduct_on `LENGTH l` THEN
     Induct_on `l` THENL
     [RW_TAC list_ss [qsort],
      RW_TAC list_ss [qsort] THEN
      ASSUM_LIST (fn thl => ASSUME_TAC 
		  (REWRITE_RULE []
		   (SPEC ``FILTER (\y. y < h) l``
		    (REWRITE_RULE [LENGTH_FILTER]
		     (SPEC ``LENGTH (FILTER (\y. y < h) l)`` (el 2 thl)))))) THEN
      ASSUM_LIST (fn thl => ASSUME_TAC 
		  (REWRITE_RULE []
		   (SPEC ``FILTER (\y. ~(y < h)) l``
		    (REWRITE_RULE [LENGTH_FILTER]
		     (SPEC ``LENGTH (FILTER (\y. ~(y < h)) l)`` (el 3 thl)))))) THEN
      RW_TAC bool_ss [] THEN
      EQ_TAC THENL
      [RW_TAC bool_ss [] THEN
       IMP_RES_TAC EVERY_FILTER_lemma1,
       RW_TAC bool_ss [] THEN
       RW_TAC bool_ss [EVERY_IMP_EVERY_FILTER]]]);;



val NOT_MEM_FST_SPLIT = prove
    (``!x l. ~MEM x l ==> (FST (SPLIT x l) = l)``,
     Induct_on `l` THENL
     [RW_TAC list_ss [SPLIT,SPLIT1],
      RW_TAC list_ss [SPLIT,SPLIT1] THEN
      RES_TAC THEN
      ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
      PAIR_TAC ``SPLIT1 (x:'a) [] l`` THEN
      LETR_TAC THEN
      UNDISCH_TAC ``FST (SPLIT x l) = l`` THEN
      R_TAC [SPLIT] THEN
      RW_TAC list_ss []]);;
val MEM_FST_SPLIT_APPEND = prove
    (``!x l1 l2. MEM x l1 ==>
	 (FST (SPLIT x (APPEND l1 l2)) = FST (SPLIT x l1))``,
     GEN_TAC THEN
     Induct_on `l1` THENL
     [RW_TAC list_ss [],
      RW_TAC list_ss [SPLIT,SPLIT1] THEN
      RES_TAC THEN
      ASSUM_LIST (fn thl => ASSUME_TAC (REWRITE_RULE [SPLIT] (el 1 thl))) THEN
      ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
      PAIR_TAC ``SPLIT1 (x:'a) [] (APPEND l1 l2)`` THEN
      LETR_TAC THEN
      PAIR_TAC ``SPLIT1 (x:'a) [] l1`` THEN
      LETR_TAC THEN
      RW_TAC list_ss []]);;
val NOT_MEM_FST_SPLIT_APPEND = prove
    (``!x l1 l2. ~MEM x l1 ==>
	 (FST (SPLIT x (APPEND l1 l2)) = APPEND l1 (FST (SPLIT x l2)))``,
     GEN_TAC THEN
     Induct_on `l1` THENL
     [RW_TAC list_ss [],
      RW_TAC list_ss [SPLIT,SPLIT1] THEN
      RES_TAC THEN
      ASSUM_LIST (fn thl => ASSUME_TAC (REWRITE_RULE [SPLIT] (el 1 thl))) THEN
      ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
      PAIR_TAC ``SPLIT1 (x:'a) [] (APPEND l1 l2)`` THEN
      LETR_TAC THEN
      PAIR_TAC ``SPLIT1 (x:'a) [] l2`` THEN
      LETR_TAC THEN
      RW_TAC list_ss []]);;
val MEM_SND_SPLIT_APPEND = prove
      (``!(x:'a) l1 l2. MEM x l1 ==>
	   (SND (SPLIT x (APPEND l1 l2)) = APPEND (SND (SPLIT x l1)) l2)``,
       Induct_on `l1` THENL
       [RW_TAC list_ss [],
	RW_TAC list_ss [] THENL
	[RW_TAC list_ss [SPLIT,SPLIT1],
	 RW_TAC list_ss [SPLIT,SPLIT1] THEN
	 ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
	 PAIR_TAC ``SPLIT1 (x:'a) [] (APPEND l1 l2)`` THEN
	 LETR_TAC THEN
	 PAIR_TAC ``SPLIT1 (x:'a) [] l1`` THEN
	 LETR_TAC THEN RES_TAC THEN
	 ASSUM_LIST (fn thl => REWRITE_TAC [REWRITE_RULE [SPLIT] (el 1 thl)])]]);;
val NOT_MEM_SND_SPLIT_APPEND = prove
      (``!(x:'a) l1 l2. ~(MEM x l1) ==> 
	   (SND (SPLIT x (APPEND l1 l2)) = SND (SPLIT x l2))``,
       Induct_on `l1` THENL
       [RW_TAC list_ss [],
	RW_TAC list_ss [SPLIT,SPLIT1] THEN
	ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
	PAIR_TAC ``SPLIT1 (x:'a) [] (APPEND l1 l2)`` THEN
	LETR_TAC THEN
	PAIR_TAC ``SPLIT1 (x:'a) [] l2`` THEN
	LETR_TAC THEN RES_TAC THEN
	ASSUM_LIST (fn thl => REWRITE_TAC [REWRITE_RULE [SPLIT] (el 1 thl)])]);;



val ordered_pre_qsort = prove
    (``!l. ordered_pre (qsort l)``,
     R_TAC [ordered_pre] THEN
     REPEAT GEN_TAC THEN
     completeInduct_on `LENGTH l` THEN
     Induct_on `l` THENL
     [R_TAC [qsort,ordered_pre] THEN
      R_TAC [SPLIT,SPLIT1] THEN
      RW_TAC list_ss [],
      R_TAC [qsort] THEN
      RW_TAC list_ss [] THENL
      [IMP_RES_TAC MEM_FST_SPLIT_APPEND THEN
       RW_TAC list_ss [] THEN
       ASSUM_LIST (fn thl => ASSUME_TAC
		   (REWRITE_RULE [LENGTH_FILTER]
		    (SPEC ``LENGTH (FILTER (\y. y < h) l)`` (el 4 thl)))) THEN
       ASSUM_LIST (fn thl => ASSUME_TAC
		   (REWRITE_RULE []
		    (SPEC ``FILTER (\y. y < h) l`` (el 1 thl)))) THEN
       RW_TAC bool_ss [],
       ASSUME_TAC (ONCE_REWRITE_RULE [EQ_SYM_RULE MEM_qsort] MEM_FILTER_lemma1) THEN
       RW_TAC list_ss [SPLIT_APPEND] THEN
       R_TAC [EVERY_qsort] THEN
       R_TAC [EVERY_FILTER_lemma3],
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       R_TAC [MEM_qsort] THEN
       SIMP_TAC bool_ss [MEM_FILTER] THEN
       STRIP_TAC THEN
       IMP_RES_TAC MEM_FILTER_lemma2 THEN
       ASSUM_LIST (fn thl => ASSUME_TAC 
		   (ONCE_REWRITE_RULE [EQ_SYM_RULE MEM_qsort]
		    (SPEC ``l:num list`` (el 1 thl)))) THEN
       RW_TAC bool_ss [NOT_MEM_FST_SPLIT_APPEND] THEN
       RW_TAC list_ss [] THENL
       [R_TAC [EVERY_qsort] THEN
	RW_TAC list_ss [EVERY_FILTER_lemma2],
	RW_TAC list_ss [SPLIT,SPLIT1] THEN
	ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
	PAIR_TAC ``SPLIT1 x [] (qsort (FILTER (\y. ~(y < h)) l))`` THEN
	LETR_TAC THEN
	RW_TAC list_ss [] THEN
	R_TAC [EQ_SYM_RULE SPLIT] THEN
	ASSUM_LIST (fn thl => ASSUME_TAC
		    (REWRITE_RULE [LENGTH_FILTER]
		     (SPEC ``LENGTH (FILTER (\y. ~(y < h)) l)`` (el 7 thl)))) THEN
	ASSUM_LIST (fn thl => ASSUME_TAC
		    (REWRITE_RULE []
		     (SPEC ``FILTER (\y. ~(y < h)) l`` (el 1 thl)))) THEN
	IMP_RES_TAC MEM_FILTER_lemma3 THEN
	ASSUM_LIST (fn thl => ASSUME_TAC
		    (ONCE_REWRITE_RULE [EQ_SYM_RULE MEM_qsort] (el 2 thl))) THEN
	RW_TAC bool_ss []]]]);;


val ordered_post_qsort = prove
    (``!l. ordered_post (qsort l)``,
     R_TAC [ordered_post] THEN
     REPEAT GEN_TAC THEN
     completeInduct_on `LENGTH l` THEN
     Induct_on `l` THENL
     [R_TAC [qsort,ordered_post] THEN
      RW_TAC list_ss [SPLIT,SPLIT1],
      R_TAC [qsort] THEN
      RW_TAC list_ss [] THENL
      [ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       R_TAC [MEM_qsort] THEN
       SIMP_TAC bool_ss [MEM_FILTER] THEN
       STRIP_TAC THEN
       IMP_RES_TAC MEM_FILTER_lemma4 THEN
       ASSUM_LIST (fn thl => ASSUME_TAC (ONCE_REWRITE_RULE [EQ_SYM_RULE MEM_qsort] (el 2 thl))) THEN
       RW_TAC bool_ss [MEM_SND_SPLIT_APPEND] THEN
       RW_TAC list_ss [] THENL
       [RW_TAC list_ss [SPLIT,SPLIT1] THEN
	ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
	PAIR_TAC ``SPLIT1 x [] (qsort (FILTER (\y. y < h) l))`` THEN
	LETR_TAC THEN
	R_TAC [EQ_SYM_RULE SPLIT] THEN
	ASSUM_LIST (fn thl => ASSUME_TAC
		    (REWRITE_RULE [LENGTH_FILTER]
		     (SPEC ``LENGTH (FILTER (\y. y < h) l)`` (el 7 thl)))) THEN
        ASSUM_LIST (fn thl => ASSUME_TAC
		    (REWRITE_RULE []
		     (SPEC ``FILTER (\y. y < h) l`` (el 1 thl)))) THEN
	RW_TAC bool_ss [],
	R_TAC [EVERY_qsort] THEN
	RW_TAC bool_ss [EVERY_FILTER_lemma4]],
       ASSUME_TAC (ONCE_REWRITE_RULE [EQ_SYM_RULE MEM_qsort] MEM_FILTER_lemma1) THEN
       RW_TAC list_ss [SPLIT_APPEND] THEN
       R_TAC [EVERY_qsort] THEN
       R_TAC [EVERY_FILTER_lemma5],
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       R_TAC [MEM_qsort] THEN
       SIMP_TAC bool_ss [MEM_FILTER] THEN
       STRIP_TAC THEN
       IMP_RES_TAC
       (ONCE_REWRITE_RULE [EQ_SYM_RULE MEM_qsort] MEM_FILTER_lemma2) THEN
       RW_TAC bool_ss [NOT_MEM_SND_SPLIT_APPEND] THEN
       RW_TAC list_ss [SPLIT,SPLIT1] THENL
       [R_TAC [EVERY_qsort] THEN
	R_TAC [EVERY_FILTER_lemma5],
	ONCE_REWRITE_TAC [SPLIT1_lemma] THEN
	PAIR_TAC ``SPLIT1 x [] (qsort (FILTER (\y. ~(y < h)) l))`` THEN
	LETR_TAC THEN
	ONCE_REWRITE_TAC [EQ_SYM_RULE SPLIT] THEN
	ASSUM_LIST (fn thl => ASSUME_TAC
		    (REWRITE_RULE [LENGTH_FILTER]
		     (SPEC ``LENGTH (FILTER (\y. ~(y < h)) l)`` (el 6 thl)))) THEN
	ASSUM_LIST (fn thl => ASSUME_TAC
		    (REWRITE_RULE []
		     (SPEC ``FILTER (\y. ~(y < h)) l`` (el 1 thl)))) THEN
	IMP_RES_TAC MEM_FILTER_lemma3 THEN
	ASSUM_LIST (fn thl => ASSUME_TAC (REWRITE_RULE [MEM_qsort] (el 3 thl))) THEN
	RW_TAC bool_ss []]]]);;


val qsort_correctness = prove
    (``!l. ordered (qsort l)``,
     R_TAC [ordered,ordered_pre_qsort,ordered_post_qsort]);;