src/holfoot/holfootLib.sml

393    val (tag_t,e1,data,e2) = dest_holfoot_ap_data_list_seg tt;
398       val thm0 = ISPECL [e1, e2, sfb, tag_t, data]
406       val thm0 = ISPECL [sfb, e1, tag_t, data]
430    val (tagL,e1,data) = dest_holfoot_ap_data_tree tt;
431    val thm0 = ISPECL [e1, tagL, data, sfb]
442    val (is_interval, (e1,e2,data)) = dest_holfoot_ap_data_array_interval tt;
445    val base_thm = ISPECL [c1, c2, data, sfb]
884             val (tagL_t, _, data') = dest_holfoot_ap_data_tree ls_t;
885             val (dtagL, data) = pairSyntax.dest_pair data';
887             ISPECL [tagL_t, e, dtagL, data, sfb1, sfb2', wpb,rpb]
906          val (_, _, data') = dest_holfoot_ap_data_tree ls_t;
907          val (_, data) = pairSyntax.dest_pair data';
909          QUANT_CONV (QUANT_CONV (my_asl_exists_list_CONV data)) THENC
945    val (tagL_t, _, data') = dest_holfoot_ap_data_tree ls_t;
946    val (dtagL, data) = pairSyntax.dest_pair data';
947    val (v_t, tL_t) = dest_node data;
1076       val (is_interval, (e1, e2, data)) = dest_holfoot_ap_data_array_interval sf;
1077       val (dataL, data_ty) = listSyntax.dest_list data;
1082       val (thm0,data) = if need_intro then
1102                           (mk_var ("data", holfoot_a_expression_ty));
1105            val (data, _) = dest_forall (rhs (concl xthm4))
1107            (xthm4,data)
1114         val data' = listSyntax.mk_list (dataL2_h::dataL2, data_ty)
1115         val data_perm_thm = EQT_ELIM (permLib.PERM_NORMALISE_CONV (list_mk_icomb (permLib.PERM_tm, [data, data'])))
1124      (thm0, need_intro,SOME data)
1561    (*intro needed data*)
2075          val (_, _, data') = dest_holfoot_ap_data_tree ttt;
2076          val (_, data) = pairSyntax.dest_pair data';
2078          QUANT_CONV (QUANT_CONV (my_asl_exists_list_CONV data)) THENC
2098           val (tagL,e1,data) = dest_holfoot_ap_data_tree ttt
2099           val (dtagL, _) = pairSyntax.dest_pair data;
2103              val (tagL',e1',data) = dest_holfoot_ap_data_tree tttt
2104              val (dtagL', _) = pairSyntax.dest_pair data;
2414    val data = listSyntax.mk_list (rev upL', pairSyntax.mk_prod (
2417    val thm0 = SPECL [e, data] (GSYM holfoot_ap_data_array_1);