Hi,guys
I am working with HOL4.
This is the subgoal
> val it =
TAKE h' (CX (INSERT h t) p q) ++
DROP h' (CX (INSERT h t) q p) =
TAKE h (CX l p q) ++ DROP h (CX l q p)
------------------------------------
0. !p' q'.
(LENGTH p' = LENGTH q') ==>
(CX (h'::t) p' q' = CX l p' q')
1. LENGTH p = LENGTH q
2. h' < h
I had proved that:
[]
|- !p q l n.
(LENGTH p = LENGTH q) ==>
(CX (INSERT n l) p q = CX (n::l) p q) : thm named "CX_IN".
Where,
val INSERT = Define `(INSERT n [] = n :: [] )
/\ (INSERT n (x::xs) = if (n < x) then n::(x::xs)
else if (n = x) then xs
else x::(INSERT n xs))`;
This function could get an increased list.
val CX_def = Define`
(CX [] p q = p) /\
(CX (x::xs) p q = TAKE x (CX xs p q) ++ DROP x (CX xs q p))`;
Next,I think I should rewrite "(CX (INSERT h t) p q)" with CX_IN,But I
can't find an appropriate rewrite tactic.
Which tactic is available?
Thanks!------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785471&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
