(* //===========================================================================
-- //
-- // AUTHOR(S): Wishnu Prasetya, Ade Azurat
-- // PACKAGE  : (c)xMECH, class LITE, version alpha 1.3.1
-- //
-- //======================================================================== *)
(* // *)
(* 

This HOL Script will prove the sde example program.

*)

val litemechDir = "../../hollib" ;

loadPath := !loadPath @ [litemechDir] ;
use  (litemechDir ^ "/litemech.smx") ;

load "sdeTheory" ;
open sdeTheory ;
load "combinTheory" ;
load "listTheory" ;

(* Some general list theorems we will need *)

val listfuns_defs = 
	[COUNT_def
	 ,SUM__def	
	 ,listTheory.FILTER 
	,listTheory.MAP ] ;

val UNDISCH_ALL_TAC = REPEAT (FIRST_ASSUM (UNDISCH_TAC o concl)) ;

fun LEMMA lemma tac 
	= 
	SUBGOAL_THEN (Term lemma) ASSUME_TAC
	THENL [tac,ALL_TAC] ;		

val COUNT_NON_NEGATIVE_thm
	=
	prove(
	--`!s. COUNT s >= 0`--,
	Induct
	THEN RW_TAC list_ss [COUNT_def]
	THEN COOPER_TAC) ;

val COUNT_MAP_thm 
	= 
	prove(
	--`!s f. COUNT (MAP f s) = COUNT s`--,
	Induct
	THEN RW_TAC list_ss [COUNT_def]) ;

val COUNT_FILTER_ZERO_thm_1
	= 
	prove(
	--`!s p x. COUNT (FILTER p (x::s)) <= 0 ==> COUNT (FILTER p s) <= 0`--,
	Induct
	THEN RW_TAC list_ss listfuns_defs
	THEN COOPER_TAC) ;

val COUNT_FILTER_ZERO_thm_2 
	= 
	prove(
	--`!s p. COUNT (FILTER p s) <= 0 ==> (!x. MEM x s ==> ~p x)`--,
	Induct
	THEN RW_TAC list_ss listfuns_defs
	THEN RW_TAC std_ss []
	THEN TRY (PROVE_TAC [])
	THEN LEMMA `~(COUNT (FILTER p s) >= 0)` COOPER_TAC
	THEN PROVE_TAC [COUNT_NON_NEGATIVE_thm] ) ;

val FILTER_2_1_EQ_thm
	=
	prove(
	--`!s. (!x. MEM x s ==> (p x /\ q x = p x))
		 ==>
		(FILTER p (FILTER q s) = FILTER p s)`--,
	Induct
	THEN RW_TAC list_ss listfuns_defs
	THEN RW_TAC std_ss []
	THEN TRY (PROVE_TAC [])) ;
	
val FUN_EQ_lemma =
	prove(
	--`(x = y) ==> (f x = f y)`--,
	RW_TAC std_ss []) ;



(* === [1] proof of the abstracted total correctness *)


val std_tac =
	RW_TAC std_ss [sumOfPositiveSaldo_def
			,deleteById_def
			,combinTheory.o_DEF]
	THEN MATCH_MP_TAC FUN_EQ_lemma
	THEN MATCH_MP_TAC FUN_EQ_lemma
	THEN MATCH_MP_TAC FILTER_2_1_EQ_thm
	THEN RW_TAC std_ss []
	THEN ASM_CASES_TAC (--`customer = (customerId:string)`--)
	THENL [ASM_REWRITE_TAC[], PROVE_TAC []]
	THEN RULE_ASSUM_TAC (REWRITE_RULE [COUNT_MAP_thm])
	THEN RULE_ASSUM_TAC (REWRITE_RULE 
		[prove(--`~(x>0) = x<=0`-- , COOPER_TAC)])
	THEN IMP_RES_TAC COUNT_FILTER_ZERO_thm_2
	THEN RULE_ASSUM_TAC BETA_RULE
	THEN PROVE_TAC [] ;

read_mechout "sde.lqs.hout.std" ;
val std_vc = snd from_mech ; 
print "\n\n==>[1] Verification of abstracted standard correctness.... \n\n" ;

val justification_of_stdcor_sde_spec = (Count.apply prove) (std_vc, std_tac) ;

(* -------------------------------------------------------------
Run data:
runtime: 0.881s,    gctime: 0.170s,     systime: 0.881s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 4239.
Total: 4239.
------------------------------------------------------------- *)

(* ==[2,3] proof of array overflow and division by zero is skipped; 
	they are trivial (program does not contain any array or
	division operation) *)

print "\n\n==>[2] Verification of array overflow check is skipped (trivial). \n\n" ;
print "\n\n==>[3] Verification of division by zero check is skipped (trivial). \n\n" ;
print "\n\n==> DONE. \n\n" ;

(* END *)