UNWIND_CONV : ((term -> bool) -> conv)
STRUCTURE
unwindLib
SYNOPSIS
Unwinds device behaviour using selected line equations until no change.
LIBRARY
unwind
DESCRIPTION
UNWIND_CONV p "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn" returns a theorem of the form: 
   |- t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn =
      t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn'
where ti' (for 1 <= i <= n) is ti rewritten with the equations eqni (1 <= i <= m). These equations are the conjuncts for which the predicate p is true. The ti terms are the conjuncts for which p is false. The rewriting is repeated until no changes take place.
FAILURE
Never fails but may loop indefinitely.
EXAMPLE
#UNWIND_CONV (\tm. mem (line_name tm) [`l1`;`l2`])
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)
SEEALSO
UNWIND_ONCE_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE
HOL  Kananaskis-14