machine-code/hoare-triple/helperLib.sml

137 val car = fst o dest_comb;
207    (if fst (dest_const (car tm)) = "one" then cdr tm else fail())
634   fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x))
834   val th = CONV_RULE (PRE_CONV (MOVE_OUT_CONV (car tm) THENC REWRITE_CONV [STAR_ASSOC])) th
835   val _ = find_term (fn x => x ~~ car tm) (car (concl th))
1152     val lhs = (cdr o car o car) n
1154     val ys = map (fn x => ((list_dest dest_star o car) x, x)) xs
1197   val ys = list_dest dest_star (car gs)
1200   val tm2 = list_mk_star (qs2 @ rev zs) (type_of (car gs))
1201   val lemma = auto_prove "SEP_WRITE_TAC" (mk_eq(car gs,tm2),SIMP_TAC (bool_ss++star_ss) [])
1204   val rhs = mk_comb((car o cdr) gs, df)
1206   val ys = (list_dest dest_star o hd o map car) xs
1228     val xs = list_dest dest_star (car h)
1234   in (z1,z2,list_mk_star (filter (not o is_match) xs) (type_of (car h)),cdr h) end
1241   if is_comb tm andalso combinSyntax.is_update (car tm)
1243        in (combinSyntax.dest_update (car tm) :: x, y) end else ([],tm)
1250     in (list_dest dest_star (car tm),f,df) end
1263   val tm = hd (filter (fn tm => is_eq tm andalso is_var((cdr o car) tm) andalso
1290   fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x))
1359   fun finder tm = ((fst o dest_const o car) tm = func_name) handle HOL_ERR _ => false
1401                               filter is_one_pair o list_dest dest_star o car) x) xs)
1414     fun finder tm = ((fst o dest_const o repeat car) tm = name) handle HOL_ERR _ => false
1458   in if can (match_term format) tm then (cdr (car tm), cdr tm) else fail() end;
1464   val ys = list_dest dest_star (car goal)
1474   val rw_goal = mk_eq(car (cdr (concl th3)),car goal)