(*


The main thing that works well is the expanded SIMP_TAC, with custom local constants.
To do:
  rehash local simp tac when new theorems are added, rather than have it rebuild with each call.


sectioning is

*)

(* experiments in revising proof style *)

open Basics;;

let section_stack  = ref [];;

let context = ref [];;

let assumption_list = ref [];;

let begin_section (s:string) = 
  section_stack := s:: !section_stack;;

let get_section() = hd (!section_stack);;

let end_section (s:string) = 
  let s1 = hd(!section_stack) in
  let _ = (s1 = s) or failwith "section" in
  let _ = section_stack := tl !section_stack in
  let _ = context := filter (fun (s1,_) -> not(s1 = s)) !context in
    ();;

let declare t = 
  let _ = context := setify ((get_section(),t) :: !context) in 
   !context;;


(* from Hales_tactic *)

let retype gls tm = 
  let varl = filter has_stv (setify(frees tm)) in
  let svarl = map (fun t-> (fst(dest_var t),t)) varl in
  let fn = fun buff (s,t) -> try (let (_,_,m)= term_match [] t (assoc s gls) in m @ buff)
  with _ -> failwith ("not found: "^s) in
  let tyassoc = List.fold_left fn [] svarl in
     (instantiate ([],[],tyassoc)) tm ;;

let get_env () = 
    map (fun (_,t) -> (fst (dest_var t),t)) !context;;

let declare_as (v,t) = 
  let v1 = mk_var(v,mk_vartype("?1")) in
  let t1 = map (fun t -> (fst (dest_var t),t)) (frees t) in
    declare (retype (t1 @ (get_env())) v1);;

let mk_assumption (s,t) = assumption_list := (get_section(),s,retype (get_env()) t) :: !assumption_list;;

begin_section "stuff";;

declare_as ("V",`packing V`);;

declare `u0:real^3`;;
declare `u1:real^3`;;
declare `v1:real^3`;;
declare `v2:real^3`;;

mk_assumption ("pV",`packing V`);;
mk_assumption ("sV",`saturated V`);;

(* Augment simplification theorems. *)


let simp_thm_list = ref [];;
let add_simp_thm q = simp_thm_list := q::!simp_thm_list;;
let get_simp_thms () = (!simp_thm_list);;


let local_net_of_thm locals rep th =
  let tm = concl th in
  let lconsts = setify (union locals (freesl (hyp th))) in
  let matchable = can o term_match lconsts in
  match tm with
    Comb(Comb(Const("=",_),(Abs(x,Comb(Var(s,ty) as v,x')) as l)),v')
         when x' = x & v' = v & not(x = v) ->
        let conv tm =
          match tm with
            Abs(y,Comb(t,y')) when y = y' & not(free_in y t) ->
              INSTANTIATE(term_match [] v t) th
          | _ -> failwith "REWR_CONV (ETA_AX special case)" in
        enter lconsts (l,(1,conv))
  | Comb(Comb(Const("=",_),l),r) ->
      if rep & free_in l r then
        let th' = EQT_INTRO th in
        enter lconsts (l,(1,REWR_CONV th'))
      else if rep & matchable l r & matchable r l then
        enter lconsts (l,(1,ORDERED_REWR_CONV term_order th))
      else enter lconsts (l,(1,REWR_CONV th))
  | Comb(Comb(_,t),Comb(Comb(Const("=",_),l),r)) ->
        if rep & free_in l r then
          let th' = DISCH t (EQT_INTRO(UNDISCH th)) in
          enter lconsts (l,(3,IMP_REWR_CONV th'))
        else if rep & matchable l r & matchable r l then
          enter lconsts (l,(3,ORDERED_IMP_REWR_CONV term_order th))
        else enter lconsts(l,(3,IMP_REWR_CONV th));;

help_grep "strip";;

(* ex local var *)

let post_rewrite =
  let ex_local v thm = 
    EXISTS (mk_exists(v, (concl thm)),v) thm in
  let ex_shared v thm = 
    let a4 = ASSUME (mk_exists (v,hd(hyp thm))) in
    let a5 = EXISTS (concl a4,v) thm in
      CHOOSE (v,a4) a5 in
  let ex_comb local v thm = if (mem v local) then ex_local v thm else ex_shared v thm in
    fun locals th ->
      if (not (is_imp (concl th))) then th else 
	let (p,q) = dest_imp (concl th) in
	let (evs,p') = strip_exists p in
	let a1 = ASSUME p' in 
	let a2 = List.fold_right (ex_comb locals) evs a1 in
	let a3 = DISCH_ALL a2 in
	  IMP_TRANS a3 th;;

(*
let ex_local v thm = 
  EXISTS (mk_exists(v, (concl thm)),v) thm;;
let ex_shared v thm = 
  let a4 = ASSUME (mk_exists (v,hd(hyp thm))) in
  let a5 = EXISTS (concl a4,v) thm in
    CHOOSE (v,a4) a5;;
let ex_comb local v thm = if (mem v local) then ex_local v thm else ex_shared v thm;;

let a0 = hd(mk_rewrites true LEAF_SQRT2 []);;
post_rewrite [x] a0;;

a2;;
ex_shared x a2;;
ex_local v (ex_shared x a2);;

let a0 = snd(post_rewrite [`V:real^3->bool`] (hd(mk_rewrites true LEAF_SQRT2 [])));;
let v = `V:real^3->bool`;;
let a1 = fst (EQ_IMP_RULE (REFL a0));;
let a2 = UNDISCH a1;;
let a3 = EXISTS (mk_exists(v, (concl a2)),v) a2;;
(* shared var *)
let x = `ul:(real^3)list`;;
let a4 = ASSUME (mk_exists(x, a0));;
let a5 = EXISTS (concl a4,x) a2;;
let a6 = CHOOSE(x,a4) a5;;

add_simp_thm LEAF_SQRT2;;
mk_rewrites true LEAF_SQRT2 [];;
add_simp_thm (hd(mk_rewrites true (UNDISCH (SPEC_ALL LEAF_SQRT2)) []));;

get_simp_thms();;

  (hd (hyp a2)) a2      
    let evs'= subtract evs locals in
    let p'' = list_mk_exists (evs',p') in
   let p''p = (p''-> p) in
      IMP_TRANS p''p th;; *)


let mk_local_rewrites locals thm sofar =
  let rw = mk_rewrites true thm [] in
    (map (post_rewrite locals) rw @ sofar);;

let local_basic_ss =
  fun thl ->
    let local = map snd !context in
    let rewmaker = mk_local_rewrites local in
    let cthms = itlist rewmaker thl [] in
    let net' = itlist (local_net_of_thm local true) cthms (basic_net()) in
    let net'' = itlist net_of_cong (basic_congs()) net' in
  Simpset(net'',basic_prover,[],rewmaker);;

simp_thm_list;;

let LOCAL_SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 8;;
let LOCAL_SIMP_CONV thl = LOCAL_SIMPLIFY_CONV (local_basic_ss []) ((get_simp_thms()) @ thl);;
let LOCAL_SIMP_RULE thl = CONV_RULE(LOCAL_SIMP_CONV thl);;
let LOCAL_SIMP_TAC thl = CONV_TAC(LOCAL_SIMP_CONV thl);;
let LOCAL_ASM_SIMP_TAC = ASM LOCAL_SIMP_TAC;;
let LOCAL_STEP_TAC () = RULE_ASSUM_TAC (LOCAL_SIMP_RULE (get_simp_thms())) THEN LOCAL_ASM_SIMP_TAC (get_simp_thms());;


(* GENERAL TACTIC KEYED TO TERMS *)


let act_list = ref [];;
let add_actionl p q = act_list := (p,q):: !act_list;;
let add_action  = unlist add_actionl;;
  

let matchable s t = can(term_match[] s) t;;
let some_matchable s tl = exists (matchable s) tl;;
let all_matchable sl tl = forall (fun s -> some_matchable s tl) sl;;

let actl pl = 
  let pl = map (retype (get_env())) pl in
  let r = filter (fun (tl,_) -> all_matchable pl tl) !act_list in
  let _ = (List.length r > 0) or failwith "act -- no match" in
    snd(hd r);;

let act = unlist actl;;

let whatl patl = 
  let patl = map (retype (get_env())) patl in
  let matcher u pat = can (find_term (can (term_match[] pat))) (concl u) in
  let matches = filter (fun (_,u) -> forall (matcher u) patl) (!thm_list) in
    matches;;

let getl patl = 
  let w = whatl patl in
  let _ = List.length w > 0 or failwith "no patterns" in
    hd (map snd w);;

let get = unlist getl;;

add_action `&0 < sqrt x` (GMATCH_SIMP_TAC SQRT_POS_LT);;
add_action `&0 <= sqrt x` (GMATCH_SIMP_TAC SQRT_POS_LE);;
add_action `sqrt x <= sqrt y` (GMATCH_SIMP_TAC SQRT_MONO_LE_EQ);;
add_action `sqrt x < sqrt y` (GMATCH_SIMP_TAC SQRT_MONO_LT_EQ);;
add_action `&0 < x * y` (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);;
add_action `x * x <= y * y` (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE);;
add_action `&0 <= x/y` (GMATCH_SIMP_TAC REAL_LE_DIV);;
add_action `&0 <= x * y` (GMATCH_SIMP_TAC REAL_LE_MUL);;
add_action `&0 <= x * x` (REWRITE_TAC[ REAL_LE_SQUARE]);;
add_action `&0 <= x pow 2` (REWRITE_TAC[ REAL_LE_POW_2]);;
add_action `sqrt x pow 2` (GMATCH_SIMP_TAC SQRT_POW_2);;
add_action `x /z <= y` (GMATCH_SIMP_TAC REAL_LE_LDIV_EQ);;
add_action `&0 <= x pow 2` (REWRITE_TAC[ REAL_LE_POW_2]);;
add_action `x < sqrt y` (GMATCH_SIMP_TAC REAL_LT_RSQRT);;
add_action `x /z <= y/ z` (GMATCH_SIMP_TAC REAL_LE_DIV2_EQ);;
add_action `sqrt(y*y)` (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);;
add_action `x * y <= x * z` (GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP);;
add_action `x < y/ z` (GMATCH_SIMP_TAC REAL_LT_RDIV_EQ);;
add_action `&0 < x/y` (GMATCH_SIMP_TAC REAL_LT_DIV);;
add_action `sqrt x * sqrt y` (GMATCH_SIMP_TAC (GSYM SQRT_MUL));;
add_action `x * x < y * y` (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE);;
add_action `x * y < x * z` (GMATCH_SIMP_TAC REAL_LT_LMUL_EQ);;
add_action `x <= y/z` (GMATCH_SIMP_TAC REAL_LE_RDIV_EQ);;
add_action `inv y <= inv x` (GMATCH_SIMP_TAC REAL_LE_INV2);;
add_action `&0 < inv x` (GMATCH_SIMP_TAC REAL_LT_INV);;

add_thm `(x:A) IN {}` NOT_IN_EMPTY;;
add_thm `&x < &y`( REAL_OF_NUM_LT);;
add_thm `&x <= &y`( REAL_OF_NUM_LE);;
add_thm `&0 <= inv x`(REAL_LE_INV_EQ);;
add_thm `&0 < inv x`(REAL_LT_INV_EQ);;
add_thm `abs(a*b)`(REAL_ABS_MUL);;
add_thm `inv (&0) = &0` REAL_INV_0;;
add_thm `hl [u0:real^A; u1]` Marchal_cells_3.HL_2;;

add_thm `~(n = 0)` (ARITH_RULE `1 < n ==> ~(n = 0)`);;

get `a \/ b`;;
getl [`a:bool`;`inv (&0)`];;
get `hl [u0;u1]`;;
get `~(t = 0)`;;
!thm_list;;
get `int_of_num`;;



(* auto matches pattern anywhere and does a sub1 repeatedly at the end of each proof step *)


let LIST_PROPS = map (fun t -> prove_by_refinement(t,[ BY(REWRITE_TAC[Bump.EL_EXPLICIT;set_of_list;LENGTH])])) 
  [
 `!(x:A) y. EL 0 (CONS (x:A) y) = x`;
  `!(x:A) y. EL 1 (CONS (x:A) y) = EL 0 y`;
  `!(x:A) y. EL 2 (CONS (x:A) y) = EL 1 y`;
  `!(x:A) y. EL 3 (CONS (x:A) y) = EL 2 y`;
  `!(x:A) y. set_of_list (CONS x y) = x INSERT (set_of_list y)`;
  `set_of_list ([]:(A)list) = {}`;
  `LENGTH ([]:(A)list) = 0`;
  `!x y. LENGTH (CONS (x:A) y) = SUC (LENGTH y)`
  ];;

map add_simp_thm LIST_PROPS;;

map add_simp_thm 
  [
    INITIAL_SUBLIST_CONS;
    INITIAL_SUBLIST_NIL;
    TRUNCATE_SIMPLEX0;
    LENGTH_TRUNCATE_SIMPLEX;
    TRUNCATE_SIMPLEX_CONS;
    CONS_11;
    TRUNCATE_SIMPLEX_EXPLICIT;
  ];;

let XIN_BARV = prove_by_refinement(
  `!V u k. u IN barV V k <=> barV V k u`,
  (* {{{ proof *)
  [
BY(REWRITE_TAC[IN])
  ]);;
  (* }}} *)

add_simp_thm XIN_BARV;;

let LEAF_BARV = prove_by_refinement(
  `!V ul. leaf V ul ==> barV V 2 ul`,
  (* {{{ proof *)
  [
    BY(MESON_TAC[Leaf_cell.leaf;IN])
  ]);;
  (* }}} *)

add_simp_thm LEAF_BARV;;

add_simp_thm Sphere.sqrt2;;


(* has variable in antecedent problem *)

let LEAF_SQRT2 = prove_by_refinement(
  `!V ul. leaf V ul ==> hl ul < sqrt(&2)`,
  (* {{{ proof *)
  [
    BY(MESON_TAC[Leaf_cell.leaf;IN;Sphere.sqrt2])
  ]);;
  (* }}} *)

(*

auto (`EL 0 (CONS (x:A) y)`,EL0_CONS);;
auto (`EL 1 (CONS (x:A) y)`,EL1_CONS);;
auto (`EL 2 (CONS (x:A) y)`,EL2_CONS);;
auto (`EL 3 (CONS (x:A) y)`,EL3_CONS);;
auto (`set_of_list (CONS (x:A) y)`,SET_OF_LIST_CONS);;
auto (`set_of_list []`,SET_OF_LIST_EMPTY);;
auto (`truncate_simplex 0 (CONS x y)`,
auto (`truncate_simplex 1 (CONS x y)`,
auto (`truncate_simplex 2 (CONS x y)`,
auto (`truncate_simplex 3 (CONS x y)`,
auto (`truncate_simplex 0 ul = [EL 0 ul]`,
auto (`HD ul`)
auto (`x IN barV V k`)
assumption `saturated V`;;

*)

add_simp_thm (arith `1 < 2`);;
add_simp_thm (LE_REFL);;

add_simp_thm Fan.th3a;;

let REUHADY = prove_by_refinement(
  `!V u0 u1 v1 v2.
    saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\ 
    ~(v1 =v2)  ==>
   sum {X | mcell_set V X /\ {u0,u1} IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2}
             (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2`,
  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC Reuhady.REUHADY1;
  GEXISTL_TAC [`[u0;u1;v1]`;`[u0;u1;v2]`];
  LOCAL_STEP_TAC();
  TYPIFY `hl [u0;u1] < sqrt(&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
    INTRO_TAC Rogers.XNHPWAB4 [`V`;`[u0;u1;v1]`;`2`];
    LOCAL_STEP_TAC();
    DISCH_THEN (C INTRO_TAC [`1`;`2`]);
    LOCAL_STEP_TAC();
    TYPIFY `hl [u0;u1;v1] < sqrt (&2)` ENOUGH_TO_SHOW_TAC;
      BY(REAL_ARITH_TAC);
    BY(LOCAL_STEP_TAC());
  TYPIFY `~collinear (set_of_list [u0; u1; v1]) /\  ~collinear (set_of_list [u0; u1; v2])` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Leaf_cell.GBEWYFX]);
  LOCAL_STEP_TAC();
  ASM_SIMP_TAC[Leaf_cell.WEDGE_GE_ALMOST_DISJOINT];
  TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
  TYPIFY `u0 IN V /\ u1 IN V` (C SUBGOAL_THEN (unlist ASM_REWRITE_TAC));
    INTRO_TAC Packing3.BARV_SUBSET [`V`;`2`;`[u0;u1;v1]`];
    LOCAL_STEP_TAC();
    BY(SET_TAC[]);
  SUBCONJ_TAC;
    ASM_SIMP_TAC[Local_lemmas.AZIM_EQ_0_GE_ALT2];
    DISCH_TAC;
    INTRO_TAC Leaf_cell.FCHKUGT [`V`;`u0`;`u1`;`v1`;`v2`];
    LOCAL_STEP_TAC();
    REWRITE_TAC[Leaf_cell.cc_A0];
    LOCAL_STEP_TAC();
    MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MP_TAC;
    GMATCH_SIMP_TAC Collect_geom.IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF;
    LOCAL_STEP_TAC();
    REWRITE_TAC[Collect_geom.aff];
    DISCH_THEN DISJ_CASES_TAC;
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM (MP_TAC o (MATCH_MP AFFINE_HULL_3_IMP_COLLINEAR));
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC Leaf_cell.EWYBJUA;
  TYPIFY `V` EXISTS_TAC;
  BY(LOCAL_STEP_TAC())
  ]);;
  (* }}} *)

let LEAF_RANKING_LEMMA = prove_by_refinement(
  `!V ul w0 n.  0 < n /\ packing V /\ saturated V /\ 
    s_leaf V ul HAS_SIZE n /\
  ~collinear {EL 0 ul,EL 1 ul,w0} ==>
    (?f.  IMAGE f (:num) = s_leaf V ul /\
       (!i. f (i + n) = f i) /\
       (!i j. i < n /\ j < n /\ i < j ==> azim (EL 0 ul) (EL 1 ul) w0 (f i) < azim (EL 0 ul) (EL 1 ul) w0 (f j)))`,
  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `(s:real^3->bool) = s_leaf V ul` TYPED_ABBREV_TAC;
  TYPIFY `!x. x IN s ==> ~(collinear {EL 0 ul,EL 1 ul,x})` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[s_leaf_collinear]);
  INTRO_TAC STRICT_SORT_FINITE [`\v w.  (azim (EL 0 ul) (EL 1 ul) w0 v <= azim (EL 0 ul) (EL 1 ul) w0 w)`;`s`;`n` ];
  BETA_TAC;
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      BY(REAL_ARITH_TAC);
    REPEAT WEAK_STRIP_TAC;
    TYPIFY `azim (EL 0 ul) (EL 1 ul) w0 x = azim (EL 0 ul) (EL 1 ul) w0 y ==> (x = y)` ENOUGH_TO_SHOW_TAC;
      REPEAT WEAK_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    DISCH_TAC;
    MATCH_MP_TAC Leaf_cell.FCHKUGT;
    GEXISTL_TAC [`V`;`EL 0 ul`;`EL 1 ul`];
    REWRITE_TAC[Leaf_cell.cc_A0];
    REWRITE_TAC[Bump.EL_EXPLICIT];
    FIRST_ASSUM (C INTRO_TAC [`x`]);
    FIRST_X_ASSUM (C INTRO_TAC [`y`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM_ST `azim` MP_TAC;
    ASM_SIMP_TAC[AZIM_EQ_ALT];
    BY(ASM_MESON_TAC[Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;s_leaf_leaf]);
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `\i. f (SUC (i MOD n))` EXISTS_TAC;
  BETA_TAC;
  CONJ2_TAC;
    CONJ_TAC;
      REPEAT WEAK_STRIP_TAC;
      INTRO_TAC MOD_MULT_ADD [`1`;`n`;`i`];
      REWRITE_TAC[arith `1 * n + i = i + n`];
      DISCH_THEN SUBST1_TAC;
      BY(REWRITE_TAC[]);
    REPEAT WEAK_STRIP_TAC;
    ASM_SIMP_TAC[MOD_LT];
    FIRST_X_ASSUM (C INTRO_TAC [`SUC i`;`SUC j`]);
    REWRITE_TAC[arith `~(a <= b) <=> (b <a)`];
    DISCH_THEN MATCH_MP_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[EXTENSION;IMAGE;IN_ELIM_THM;IN_UNIV];
  GEN_TAC;
  MATCH_MP_TAC (TAUT `((a==> b) /\ (b ==> a)) ==> (a = b)`);
  CONJ_TAC;
    REPEAT WEAK_STRIP_TAC;
    TYPIFY `SUC (x' MOD n)` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_NUMSEG];
    REWRITE_TAC[arith `1 <= SUC x`];
    REWRITE_TAC[arith `SUC x <= n <=> x < n`];
    BY(ASM_MESON_TAC[DIVISION;arith `~(n=0) <=> (0 < n)`]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `PRE x'` EXISTS_TAC;
  AP_TERM_TAC;
  TYPIFY `PRE x' MOD n = PRE x'` (C SUBGOAL_THEN SUBST1_TAC);
    MATCH_MP_TAC MOD_LT;
    FIRST_X_ASSUM_ST `IN` MP_TAC;
    REWRITE_TAC[IN_NUMSEG];
    BY(ARITH_TAC);
  FIRST_X_ASSUM_ST `IN` MP_TAC;
  REWRITE_TAC[IN_NUMSEG];
  BY(ARITH_TAC)
  ]);;
  (* }}} *)