Hi,
While proving a lemma, I get to this step:
Count winner v = max
------------------------------------
0. ((winner' = winner) ∧ (max' = max)) ∧ winner ≠ 0 ⇒
(Count winner v = max)
1. Max_vote n v = (winner',max')
2. Count (SUC n) v > max'
3. SUC n = winner
4. Count (SUC n) v = max
5. winner ≠ 0
I think by using Assumptions 3 and 4 we could easily prove the goal.
But I do not know what Tactic to use?
I have tried DECIDE_TAC, RES_TAC, SUBST1_ALL_TAC, but no success!
this is all I got:
(**********my theory to be proved************)
val Max_vote_eq_lem = store_thm ("Max_vote_eq_lem",
``! n v winner max.(( Max_vote n v= (winner , max )) /\ ~(winner=0))
==>( Count winner v = max)``
REPEAT GEN_TAC THEN
Induct_on `n` THENL [
FULL_SIMP_TAC (srw_ss())[Max_vote] THEN
REPEAT STRIP_TAC THEN
POP_ASSUM (ASSUME_TAC o GSYM) THEN
RES_TAC ,
FULL_SIMP_TAC (srw_ss())[Max_vote, Count] THEN
LET_ELIM_TAC ] THEN
POP_ASSUM MP_TAC THEN
POP_ASSUM MP_TAC THEN
REPEAT IF_CASES_TAC THEN
FULL_SIMP_TAC (srw_ss())[Max_vote, Count] THEN
REPEAT STRIP_TAC
...)
(*************** my functions: ************************)
val Count= Define `(Count c ([])= 0)
/\ ( Count c (h::l) = if h=c then Count c (l) +1
else Count c (l))`
val Max_vote = Define `
(Max_vote 0 v= (0,0)) /\
( Max_vote c v =
let (winner, max)= Max_vote (c-1) v in
( if Count c v > max then ( c , Count c v)
else if Count c v =max then (0,Count c v)
else Max_vote (c-1) v )) `
Thank you,
Masoumeh
------------------------------------------------------------------------------
"Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
Instantly run your Selenium tests across 300+ browser/OS combos. Get
unparalleled scalability from the best Selenium testing platform available.
Simple to use. Nothing to install. Get started now for free."
http://p.sf.net/sfu/SauceLabs
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
