hol88/cmos/unwind.ml

28        A1 u ... u An  |- ?l1 ... lm. t1  /\ ... /\ tn =
29                          ?l1 ... lm. t1' /\ ... /\ tn'
46         A |- t = (?l1 ... lm. t1 /\ ... /\ tn)
48         A |- t = (?l1 ... lm. t1' /\ ... /\ tn')
82   let l1,l2 = partition (\t. check_frees lefts (rhs t) ? true) eqns
84   if null l1
101                 (map subs_fn l1))
102                (list_mk_conj l1)
122   let l1,l2 = partition (\t. check_frees lefts (rhs t) ? true) eqns
124   if null l1
129    let l1' = map ((mk_eq o (I # subs_fun) o dest_eq) orelsef subs_fun) l1
131    mk_thm([], mk_eq(t, list_mk_conj(l1'@l2))))
155    |- (?l1 ... lm. x1 = t1 /\ ... /\ xn = tn) =
156       (?l1 ... lm. x1 = t1' /\ ... /\ xn = tn')
204    let x1,l1 = dest_andl first
207    if x1=x2 then (x1, l1@l2) else fail)
237    |- (?l1 ... lm. (!x. x1 = t1)  /\ ... /\ (!x. xn = tn)) =
238       (?l1 ... lm. (!x. x1 = t1') /\ ... /\ (!x. xn = tn'))
499    |- (?l1 ... lm. t1 /\ ... /\ tn) = (u1 /\ ... /\ up)
502  for which xi is not one of l1, ... ,lm. The rule below assumes that
510  (let l1,l2 = partition(free_in x)(conjuncts eqs)
512   let th1 = LIST_MK_EXISTS [x] (CONJ_SET_CONV (conjuncts eqs) (l1@l2))
526    |- (?l1 ... lm. t1 /\ ... /\ tn) = (u1 /\ ... /\ up)
529  for which xi is not one of l1, ... ,lm. The rule below assumes that
537  (let l1,l2 = partition(free_in x)(conjuncts eqs)
539   let th1 = LIST_MK_EXISTS [x] (CONJ_SET_CONV (conjuncts eqs) (l1@l2))
704               "IMP(f,g,h) = ?l3 l2 l1.
705               (!x:num. f x = (l1 (x+1)) + (l2 (x+2)) + (l3 (x+3))) /\
709 	      (!x. l1 x = (l2 x) + 1) /\
713 let tm =     "(!x:num. f x = (l1 (x+1)) + (l2 (x+2)) + (l3 (x+3))) /\
714 	      (!x. l1 x = (l2 x) + 1) /\
721 UNWIND_ONCE_CONV (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) tm;;
723 UNWIND_CONV (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) tm;;
725 UNWIND_ONCE_RULE (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) imp;;
727 UNWIND_RULE (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) imp;;