Hi all,
I observed a strange behavior of the same tactic in HOL-k10 vs HOL-k12
Consider a proof goal
``?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)``
e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV));
(* In HOL-k10, the tactic results a desired behavior*)
?!m. ((m = n) \/ m < n) /\ (~(m < n) \/ (f m = x)) /\ (m < n \/ (a = x))
(* In HOL-k12, the tactic results *)
?!m. ((m = n) \/ m < n) /\ (if m < n then $= (f m) else $= a) x
Am I missing something?
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
