(* ========================================================================= *)
(* Part 2: Transcription of Tobias's paper.                                  *)
(* ========================================================================= *)

parse_as_infix("<<",(12,"right"));;

(* ------------------------------------------------------------------------- *)
(* Wellfounded part of a relation.                                           *)
(* ------------------------------------------------------------------------- *)

let WFP_RULES,WFP_INDUCT,WFP_CASES = new_inductive_definition
  `!x. (!y. y << x ==> WFP(<<) y) ==> WFP(<<) x`;;

(* ------------------------------------------------------------------------- *)
(* Wellfounded part induction.                                               *)
(* ------------------------------------------------------------------------- *)

let WFP_PART_INDUCT = prove
 (`!P. (!x. x IN WFP(<<) /\ (!y. y << x ==> P(y)) ==> P(x))
       ==> !x:A. x IN WFP(<<) ==> P(x)`,
  GEN_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN 
  ONCE_REWRITE_TAC[TAUT `a ==> b = a ==> a /\ b`] THEN
  MATCH_MP_TAC WFP_INDUCT THEN ASM_MESON_TAC[WFP_RULES]);;

(* ------------------------------------------------------------------------- *)
(* A relation is wellfounded iff WFP is the whole universe.                  *)
(* ------------------------------------------------------------------------- *)

let WFP_WF = prove
 (`WF(<<) = (WFP(<<) = UNIV:A->bool)`,
  EQ_TAC THENL
   [REWRITE_TAC[WF_IND; EXTENSION; IN; UNIV] THEN MESON_TAC[WFP_RULES];
    DISCH_TAC THEN MP_TAC WFP_PART_INDUCT THEN 
    ASM_REWRITE_TAC[IN; UNIV; WF_IND]]);;

(* ------------------------------------------------------------------------- *)
(* The multiset order.                                                       *)
(* ------------------------------------------------------------------------- *)

let morder = new_definition
  `morder(<<) N M = ?M0 a K. (M = M0 munion (msing a)) /\
                             (N = M0 munion K) /\
                             (!b. b min K ==> b << a)`;;

(* ------------------------------------------------------------------------- *)
(* We separate off this part from the proof of LEMMA_2_1.                    *)
(* ------------------------------------------------------------------------- *)

let LEMMA_2_0 = prove
 (`morder(<<) N (M0 munion (msing a))
   ==> (?M. morder(<<) M M0 /\ (N = M munion (msing a))) \/
       (?K. (N = M0 munion K) /\ (!b:A. b min K ==> b << a))`,
  GEN_REWRITE_TAC LAND_CONV [morder] THEN
  DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN 
   [`M1:(A)multiset`; `b:A`; `K:(A)multiset`]) STRIP_ASSUME_TAC) THEN
  ASM_CASES_TAC `b:A = a` THENL 
   [DISJ2_TAC THEN UNDISCH_THEN `b:A = a` SUBST_ALL_TAC THEN
    EXISTS_TAC `K:(A)multiset` THEN ASM_MESON_TAC[MUNION_11]; DISJ1_TAC] THEN
  SUBGOAL_THEN `?M2. M1 = M2 munion (msing(a:A))` STRIP_ASSUME_TAC THENL
   [EXISTS_TAC `M1 mdiff (msing(a:A))` THEN
    MAP_EVERY MATCH_MP_TAC [MIN_MDIFF; MUNION_INUNION] THEN
    UNDISCH_TAC `M0 munion (msing a) = M1 munion (msing(b:A))` THEN
    ASM_REWRITE_TAC[MEXTENSION; MUNION; MSING; min] THEN
    DISCH_THEN(MP_TAC o SPEC `a:A`) THEN ASM_REWRITE_TAC[] THEN 
    ARITH_TAC; ALL_TAC] THEN
  EXISTS_TAC `M2 munion K:(A)multiset` THEN ASM_REWRITE_TAC[MUNION_AC] THEN
  REWRITE_TAC[morder] THEN 
  MAP_EVERY EXISTS_TAC [`M2:(A)multiset`; `b:A`; `K:(A)multiset`] THEN
  UNDISCH_TAC `M0 munion msing (a:A) = M1 munion msing b` THEN
  ASM_REWRITE_TAC[MUNION_AC] THEN MESON_TAC[MUNION_AC; MUNION_11]);;
  
(* ------------------------------------------------------------------------- *)
(* The sequence of lemmas from Tobias's paper.                               *)
(* ------------------------------------------------------------------------- *)

let LEMMA_2_1 = prove
 (`(!M b:A. b << a /\ M IN WFP(morder(<<)) 
            ==> (M munion (msing b)) IN WFP(morder(<<))) /\
   M0 IN WFP(morder(<<)) /\
   (!M. morder(<<) M M0 ==> (M munion (msing a)) IN WFP(morder(<<)))
   ==> (M0 munion (msing a)) IN WFP(morder(<<))`,
  STRIP_TAC THEN REWRITE_TAC[IN] THEN MATCH_MP_TAC WFP_RULES THEN
  X_GEN_TAC `N:(A)multiset` THEN
  DISCH_THEN(DISJ_CASES_THEN MP_TAC o MATCH_MP LEMMA_2_0) THENL
   [ASM_MESON_TAC[IN]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
  SPEC_TAC(`N:(A)multiset`,`N:(A)multiset`) THEN
  ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  MATCH_MP_TAC MULTISET_INDUCT THEN REPEAT STRIP_TAC THEN
  RULE_ASSUM_TAC(REWRITE_RULE[MUNION_ASSOC; MIN_MUNION; MIN_MSING]) THEN
  ASM_MESON_TAC[IN; MUNION_EMPTY]);;

let LEMMA_2_2 = prove
 (`(!M b. b << a /\ M IN WFP(morder(<<)) 
          ==> (M munion (msing b)) IN WFP(morder(<<)))
   ==> !M. M IN WFP(morder(<<)) ==> (M munion (msing a)) IN WFP(morder(<<))`,
  STRIP_TAC THEN MATCH_MP_TAC WFP_PART_INDUCT THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC LEMMA_2_1 THEN ASM_REWRITE_TAC[]);;

let LEMMA_2_3 = prove
 (`WF(<<)
   ==> !a M. M IN WFP(morder(<<)) ==> (M munion (msing a)) IN WFP(morder(<<))`,
  REWRITE_TAC[WF_IND] THEN DISCH_THEN MATCH_MP_TAC THEN MESON_TAC[LEMMA_2_2]);;

let LEMMA_2_4 = prove
 (`WF(<<) ==> !M. M IN WFP(morder(<<))`,
  DISCH_TAC THEN MATCH_MP_TAC MULTISET_INDUCT THEN CONJ_TAC THENL
   [REWRITE_TAC[IN] THEN MATCH_MP_TAC WFP_RULES THEN 
    REWRITE_TAC[morder; MUNION_MEMPTY];
    ASM_SIMP_TAC[LEMMA_2_3]]);;

(* ------------------------------------------------------------------------- *)
(* Hence the final result.                                                   *)
(* ------------------------------------------------------------------------- *)

let MORDER_WF = prove
 (`WF(<<) ==> WF(morder(<<))`,
  SIMP_TAC[WFP_WF; EXTENSION; IN_UNIV; LEMMA_2_4]);;