| DISP | list_length_df | | |== || |
| ABS | list_length | || == (letrec l L = case L of [] => 0 | h::t => 1 + l t esac ) |
| ML | list_length_unroll | let list_length_nil_unrollC =
FwdMacroC
`list_length_nil_unrollC`
(UnfoldC `list_length`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
 || []
;;
let list_length_cons_unrollC =
FwdMacroC
`list_length_cons_unrollC`
(UnfoldC `list_length`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `list_length`
)
|| (h::t)
;;
let list_length_unrollC =
list_length_nil_unrollC ORELSEC
list_length_cons_unrollC
;;
add_AbReduce_conv `list_length` list_length_unrollC;;
|
| THM | list_length_wf_nat |  T: . ||  T List    |
| ML | list_length_ind | let ListLenInd i = InvImageInd1 || CompNatInd i ;;
|
| THM | list_length_wf_int | T:. || T List  |
| THM | apply_wf_list_length | T:. L:T List. || L |
| THM | apply_wf_list_length_nat | T:. L:T List. || L |
| THM | apply_wf_list_length_int | T:. L:T List. || L |
| THM | list_length_non_negative | T:. L:T List. || L  0 |
| THM | length_wf_nat | T:. L:T List. ||L|| |
| THM | discrete__list | T:. Discrete{T}   Discrete{(T List)} |
| ML | length_ind_tac | let LengthWFInd i = InvImageInd1 || CompNatInd i ;;
|
| ML | null_unroll | let null_nil_unrollC =
FwdMacroC
`null_nil_unrollC`
(UnfoldC `null`
ANDTHENC ReduceC
)
null([])
;;
let null_cons_unrollC =
FwdMacroC
`null_cons_unrollC`
(UnfoldC `null`
ANDTHENC ReduceC
)
null(h::t)
;;
let null_unrollC =
null_nil_unrollC ORELSEC null_cons_unrollC
;;
add_AbReduce_conv `null` null_unrollC;;
|
| THM | null_true_lemma | T:. L:T List. null(L) = tt  L = [] |
| THM | null_false_lemma | T:. L:T List. null(L) = ff ( h:T. t:T List. L = (h::t)) |
| DISP | remove_df | remove(<eq:eq:L><x:A:L><L:A list:L>)== remove(<eq><x><L>) |
| ABS | remove | remove(eq;x;L) ==
(letrec remove eq x L = case L of
[] => []
h::t => if eq x h
then t
else h::(remove eq x t)
fi
esac )
eq
x
L |
| ML | remove_unroll | let remove_nil_unrollC =
FwdMacroC
`remove_nil_unrollC`
(UnfoldC `remove`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
remove(eq;x;[])
;;
let remove_cons_unrollC =
FwdMacroC
`remove_cons_unrollC`
(UnfoldC `remove`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `remove`
)
remove(eq;x;(h::t))
;;
let remove_unrollC =
remove_nil_unrollC ORELSEC remove_cons_unrollC
;;
add_AbReduce_conv `remove` remove_unrollC;;
|
| THM | remove_wf | T:. eq:T T  . x:T. L:T List. remove(eq;x;L) T List |
| DISP | filter_df | filter(<f:T :L><L:T list:L>)== filter(<f><L>) |
| ABS | filter | filter(f;L) ==
(letrec filter f L = case L of
[] => []
h::t => if f h
then h::(filter f t)
else filter f t
fi
esac )
f
L |
| ML | filter_unroll | let filter_nil_unrollC =
FwdMacroC
`filter_nil_unrollC`
(UnfoldC `filter`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
filter(f;[])
;;
let filter_cons_unrollC =
FwdMacroC
`filter_cons_unrollC`
(UnfoldC `filter`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `filter`
)
filter(f;(h::t))
;;
let filter_unrollC =
filter_nil_unrollC ORELSEC filter_cons_unrollC
;;
add_AbReduce_conv `filter` filter_unrollC;;
|
| THM | filter_wf | T:. f:T . L:T List. filter(f;L) T List |
| THM | filter_wf_subtype | T:. f:T . L:T List. filter(f;L) {x:T|  (f x)} List |
| DISP | is_member_df | <x:T:L>(<eq:T equality:L>) <L:T list:L>== <x>(<eq>) <L> |
| ABS | is_member | x(eq) L ==
(letrec is_member x eq L = case L of
[] => ff
h::t => if eq x h
then tt
else is_member x eq t
fi
esac )
x
eq
L |
| ML | is_member_unroll | let is_member_nil_unrollC =
FwdMacroC
`is_member_nil_unrollC`
(UnfoldC `is_member`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
x(eq) []
;;
let is_member_cons_unrollC =
FwdMacroC
`is_member_cons_unrollC`
(UnfoldC `is_member`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `is_member`
)
x(eq) (h::t)
;;
let is_member_unrollC =
is_member_nil_unrollC ORELSEC is_member_cons_unrollC
;;
add_AbReduce_conv `is_member` is_member_unrollC;;
|
| THM | is_member_wf_nil | T:. eq:T T . u:T. u(eq) [] |
| THM | comb_for_is_member_wf_nil | ( T,eq,u,z.u(eq) []) T: eq:(T T ) u:T  True |
| THM | is_member_wf | T:. eq:T T . x:T. L:T List. x(eq) L |
| THM | comb_for_is_member_wf | (T,eq,x,L,z.x(eq) L) T:
eq:(T T )
x:T
L:T List
True
|
| THM | sq_stable__is_member | T:. eq:T T . x:T. L:T List. SqStable(x(eq) L) |
| THM | decidable__is_member | T:. eq:T T . x:T. L:T List. Dec(x(eq) L) |
| THM | is_member_equalities_lemma | T:. eq:{T= }. u:T. L:T List. u(eq) L (f:{T }. u(f) L) |
| THM | is_member_equality_strengthening_lemma | T:. equiv:{T}. eq:{T=}. u:T. L:T List.
u(equiv) L (v:T. (equiv u v)  v(eq) L) |
| THM | is_member_equality_weakening_lemma | T:. equiv:{T}. eq:{T=}. u:T. L:T List.
u(eq) L (v:T. (equiv u v) v(equiv) L) |
| THM | hd_is_member_lemma | T:. eq:{T}. L:T List. ||L|| 1 hd(L)(eq) L |
| THM | non_nil_is_member | T:. eq:{T}. L:T List. L  [] T List (x:T. x(eq) L) |
| THM | is_member_cons | T:. eq:{T}. t:T. L:T List. t(eq) (t::L) |
| DISP | list_all_df | <x:element><L:T List:L>.<P:T i:L>== <x><L>.<P> |
| ABS | list_all | xL.P[x] ==
(letrec list_all L = case L of
[] => True
h::t => P[h] list_all t
esac )
L |
| ML | list_all_unroll | let list_all_nil_unrollC =
FwdMacroC
`list_all_nil_unrollC`
(UnfoldC `list_all`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
x[].P[x]
;;
let list_all_cons_unrollC =
FwdMacroC
`list_all_cons_unrollC`
(UnfoldC `list_all`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `list_all`
)
x(h::t).P[x]
;;
let list_all_unrollC =
list_all_nil_unrollC ORELSEC list_all_cons_unrollC
;;
add_AbReduce_conv `list_all` list_all_unrollC;;
|
| THM | list_all_wf | T:. P:T . L:T List. xL.P[x] |
| THM | comb_for_list_all_wf | (T,P,L,z.xL.P[x]) T: P:(T ) L:T List True |
| THM | list_all_wf_nil | T:. P:T . x[].P[x] |
| THM | comb_for_list_all_wf_nil | (T,P,z.x[].P[x]) T: P:(T ) True |
| THM | list_all_tail | T:. P:T . L:T List. x:T. x(x::L).P[x] xL.P[x] |
| THM | sq_stable__list_all | T:. P:T . L:T List.
(x:T. SqStable(P[x])) SqStable(xL.P[x]) |
| THM | decidable__list_all | T:. P:T . L:T List. (x:T. Dec(P[x])) Dec(xL.P[x]) |
| THM | list_all_of_false_false | T:. L:T List. x:T. x(x::L).False False |
| DISP | list_all_2_df | <x:element><L:T List:L>.<P:T :L>== <x><L>.<P> |
| ABS | list_all_2 | xL.P[x] ==
(letrec all L = case L of [] => tt | h::t => P[h]  all t esac )
L |
| ML | list_all_2_unroll | let list_all_2_nil_unrollC =
FwdMacroC
`list_all_2_nil_unrollC`
(UnfoldC `list_all_2`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
x[].P[x]
;;
let list_all_2_cons_unrollC =
FwdMacroC
`list_all_2_cons_unrollC`
(UnfoldC `list_all_2`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `list_all_2`
)
x(h::t).P[x]
;;
let list_all_2_unrollC =
list_all_2_nil_unrollC ORELSEC list_all_2_cons_unrollC
;;
add_AbReduce_conv `list_all_2` list_all_2_unrollC;;
|
| THM | list_all_2_wf | T:. P:T . L:T List. xL.P[x] |
| THM | not_list_all_2_implies_exists_not | T:. eq:{T}. P:T . L:T List.
 xL.P[x] (x:{x:T| x(eq) L} . P[x]) |
| THM | list_all_iff_assert_list_all_2 | T:. L:T List. P:T . xL.(P[x]) xL.P[x] |
| THM | list_all_is_member_lemma | T:. eq:{T=}. P:T . L:T List.
xL.P[x] (z:T. z(eq) L P[z]) |
| THM | list_all_is_member_nil_lemma | T:. eq:T T . L:T List. xL.(x(eq) []) [] = L |
| THM | list_all_thru_and | T:. P,Q:T . x,y:T. L:T List.
x = y (P[x] Q[y]) (zL.P[z] zL.Q[z]) |
| DISP | list_exists_df | <x:element><L:T List:L>.<P:Ti:L>== <x><L>.<P> |
| ABS | list_exists | xL.P[x] ==
(letrec list_exists L = case L of
[] => False
h::t => P[h]  list_exists t
esac )
L |
| ML | list_exists_unroll | let list_exists_nil_unrollC =
FwdMacroC
`list_exists_nil_unrollC`
(UnfoldC `list_exists`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
x[].P[x]
;;
let list_exists_cons_unrollC =
FwdMacroC
`list_exists_cons_unrollC`
(UnfoldC `list_exists`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `list_exists`
)
x(h::t).P[x]
;;
let list_exists_unrollC =
list_exists_nil_unrollC ORELSEC list_exists_cons_unrollC
;;
add_AbReduce_conv `list_exists` list_exists_unrollC;;
|
| THM | list_exists_wf | T:. P:T . L:T List. xL.P[x] |
| THM | decidable__list_exists | T:. P:T . L:T List. (x:T. Dec(P[x])) Dec(xL.P[x]) |
| THM | list_exists_is_member_lemma | T:. eq:{T=}. P:T . L:T List.
(x:T. x(eq) L P[x]) yL.P[y] |
| THM | list_exists_is_member_lemma1 | T:. eq:{T=}. P:T . x:T. L:T List.
x(eq) L P[x] yL.P[y] |
| THM | not_list_exists_iff_list_all_not | T:. P:T . L:T List. xL.P[x] xL.(P[x]) |
| THM | list_exists_exists | T:. eq:{T=}. P:T . L:T List.
xL.P[x] (x:{x:T| x(eq) L} . P[x]) |
| THM | list_all_all | T:. eq:{T=}. P:T . L:T List.
xL.P[x] (x:{x:T| x(eq) L} . P[x]) |
| THM | list_all_2_all | T:. P:T . L:T List. xL.P[x] xL.(P[x]) |
| DISP | list_exists_2_df | <x:element><L:T List:L>.<P:T :L>== <x><L>.<P> |
| ABS | list_exists_2 | xL.P[x] ==
(letrec exists L = case L of
[] => ff
h::t => P[h] (exists t)
esac )
L |
| ML | list_exists_2_unroll | let list_exists_2_nil_unrollC =
FwdMacroC
`list_exists_2_nil_unrollC`
(UnfoldC `list_exists_2`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
x[].P[x]
;;
let list_exists_2_cons_unrollC =
FwdMacroC
`list_exists_2_cons_unrollC`
(UnfoldC `list_exists_2`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `list_exists_2`
)
x(h::t).P[x]
;;
let list_exists_2_unrollC =
list_exists_2_nil_unrollC ORELSEC list_exists_2_cons_unrollC
;;
add_AbReduce_conv `list_exists_2` list_exists_2_unrollC;;
|
| THM | list_exists_2_wf | T:. P:T . L:T List. xL.P[x] |
| THM | remove_is_member | T:. eq:{T}. x,y:T. L:T List.
x(eq) remove(eq;y;L) x(eq) L |
| THM | not_list_all_not_iff_list_exists | T:. P:T .
(x:T. Dec(P[x])) (L:T List. xL.(P[x]) xL.P[x]) |
| DISP | disjoint_df | disjoint(<eq:equality:L><L1:List:L><L2:List:L>)
== disjoint(<eq><L1><L2>) |
| ABS | disjoint | disjoint(eq;L1;L2) == xL1.(x(eq) L2) |
| ML | disjoint_unroll | let disjoint_nil_unrollC =
FwdMacroC
`disjoint_nil_unrollC`
(UnfoldC `disjoint`
ANDTHENC HigherC list_all_unrollC
)
disjoint(eq;[];L)
;;
let disjoint_cons_unrollC =
FwdMacroC
`disjoint_cons_unrollC`
(UnfoldC `disjoint`
ANDTHENC HigherC list_all_unrollC
ANDTHENC FoldC `disjoint`
)
disjoint(eq;(h::t);L)
;;
let disjoint_unrollC =
disjoint_nil_unrollC ORELSEC disjoint_cons_unrollC
;;
add_AbReduce_conv `disjoint` disjoint_unrollC ;;
|
| THM | disjoint_wf | T:. eq:T T . L1,L2:T List. disjoint(eq;L1;L2) |
| THM | decidable__disjoint | T:. eq:T T . L1,L2:T List. Dec(disjoint(eq;L1;L2)) |
| THM | disjoint_tail | T:. eq:T T . L1,L2:T List. x:T.
disjoint(eq;(x::L1);L2) disjoint(eq;L1;L2) |
| DISP | disjoint2_df | disjoint(<eq:equality:L><L:List:L><M:List:L>)
== disjoint(<eq><L><M>) |
| ABS | disjoint2 | disjoint(eq;L;M) ==
(letrec disjoint2 L = case L of
[] => tt
h::t => if h(eq) M
then ff
else disjoint2 t
fi
esac )
L |
| ML | disjoint2_unroll | let disjoint2_nil_unrollC =
FwdMacroC
`disjoint2_nil_unrollC`
(UnfoldC `disjoint2`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
)
disjoint(eq;[];M)
;;
let disjoint2_cons_unrollC =
FwdMacroC
`disjoint2_cons_unrollC`
(UnfoldC `disjoint2`
ANDTHENC letrec_unrollC
ANDTHENC ReduceC
ANDTHENC FoldC `disjoint2`
)
disjoint(eq;(h::t);M)
;;
let disjoint2_unrollC =
disjoint2_nil_unrollC ORELSEC disjoint2_cons_unrollC
;;
|
| THM | disjoint2_wf | T:. eq:{T}. L,M:T List. disjoint(eq;L;M) |
| THM | disjoint_iff_assert_disjoint2 | T:. eq:{T}. L,M:T List. disjoint(eq;L;M) disjoint(eq;L;M) |
| THM | not_disjoint_is_member_lemma | T:. eq:{T=}. L,M:T List.
disjoint(eq;L;M) (x:T. x(eq) L x(eq) M) |
| THM | append_nil_right_identity | T:. L:T List. L @ [] = L |
| DISP | sublist_df | <L1:List:L>( <eq:Equality:L>)<L2:List:L>== <L1>(<eq>)<L2> |
| ABS | sublist | L1(eq)L2 == xL1.(x(eq) L2) |
| ML | sublist_unroll | let sublist_nil_unrollC =
FwdMacroC
`sublist_nil_unrollC`
(UnfoldC `sublist`
ANDTHENC HigherC list_all_unrollC
)
[](eq)L
;;
let sublist_cons_unrollC =
FwdMacroC
`sublist_cons_unrollC`
(UnfoldC `sublist`
ANDTHENC HigherC list_all_unrollC
ANDTHENC FoldC `sublist`
)
(h::t)(eq)L
;;
let sublist_cons_nil_unrollC =
FwdMacroC
`sublist_cons_unrollC`
(UnfoldC `sublist`
ANDTHENC HigherC is_member_unrollC
ANDTHENC HigherC assert_evalC
)
(h::t)(eq)[]
;;
let sublist_unrollC =
sublist_nil_unrollC
ORELSEC sublist_cons_nil_unrollC
ORELSEC sublist_cons_unrollC
;;
add_AbReduce_conv `sublist` sublist_unrollC;;
|
| THM | sublist_wf | T:. eq:T T . L1,L2:T List. L1(eq)L2 |
| THM | comb_for_sublist_wf | (T,eq,L1,L2,z.L1(eq)L2) T:
eq:(T T )
L1:T List
L2:T List
True
|
| THM | sublist_wf1 | T:. eq:{T=}. L1,L2:T List. L1(eq)L2 |
| THM | comb_for_sublist_wf1 | (T,eq,L1,L2,z.L1(eq)L2) T:
eq:{T=}
L1:T List
L2:T List
True
|
| THM | sublist_wf2 | T:. eq:{T}. L1,L2:T List. L1(eq)L2 |
| THM | comb_for_sublist_wf2 | (T,eq,L1,L2,z.L1(eq)L2) T:
eq:{T}
L1:T List
L2:T List
True
|
| THM | decidable__sublist | T:. eq:{T}. L,M:T List. Dec(L(eq)M) |
| THM | sublist_tail | T:. Discrete{T} (eq:{T}. u:T. v:T List. v(eq)(u::v)) |
| THM | sublist_tail1 | T:. eq:{T=}. u:T. v:T List. v(eq)(u::v) |
| THM | sublist_list_all_lemma | T:. EQ:{T=}. eq:{T}. L,M:T List.
L(eq)M (z:T. z(EQ) L z(eq) M) |
| THM | sublist_weakening_wrt_identity | T:. Discrete{T} (eq:{T}. L,M:T List. L = M L(eq)M) |
| THM | sublist_reflexive | T:. eq:{T=}. L:T List. L(eq)L |
| THM | sublist_transitivity | T:
Discrete{T}
(eq1,eq2,eq3:{T}. L1,L2,L3:T List.
eq1 = eq2
eq2 = eq3
L1(eq1)L2
L2(eq2)L3
L1(eq3)L3) |
| THM | is_member_sublist_lemma | T:. eq:{T=}. x:T. L,M:T List. x(eq) L L(eq)M x(eq) M |
| DISP | sublist_2_df | (<eq:Equality:L>)== (<eq>) |
| ABS | sublist_2 | (eq) == L,M.xL.x(eq) M |
| ML | sublist_2_unroll | let sublist_2_nil_unrollC =
FwdMacroC
`sublist_2_nil_unrollC`
(UnfoldC `sublist_2`
ANDTHENC ReduceC
)
(eq) [] M
;;
let sublist_2_cons_unrollC =
FwdMacroC
`sublist_2_cons_unrollC`
(UnfoldC `sublist_2`
ANDTHENC ReduceC
)
(eq) (h::t) M
;;
let sublist_2_cons_nil_unrollC =
FwdMacroC
`sublist_2_cons_unrollC`
(UnfoldC `sublist_2`
ANDTHENC ReduceC
)
(eq) (h::t) []
;;
let sublist_2_unrollC =
sublist_2_nil_unrollC
ORELSEC sublist_2_cons_nil_unrollC
ORELSEC sublist_2_cons_unrollC
;;
add_AbReduce_conv `sublist_2` sublist_2_unrollC;; |
| THM | sublist_2_wf | T:. eq:T T . (eq) T List T List |
| THM | apply_sublist_2_wf | T:. L,M:T List. eq:T T . (eq) L M |
| THM | apply_wf_sublist_2 | T:. L,M:T List. eq:T T . (eq) L M |
| THM | sublist_iff_assert_sublist_2 | T:
Discrete{T} (eq:{T}. L,M:T List. L(eq)M ((eq) L M)) |
| THM | sublist_iff_assert_sublist_2_x | T:. L,M:T List. eq:{T=}. L(eq)M ((eq) L M) |
| THM | sublist_of_nil_iff_nil | T:. eq:{T=}. L:T List. L(eq)[] L = [] |
| THM | append_associative | T:. L1,L2,L3:T List. L1 @ L2 @ L3 = (L1 @ L2) @ L3 |
| THM | is_member_append_lemma | T:. eq:{T=}. L:T List. x:T.
x(eq) L (M,N:T List. L = M @ (x::N)) |
| THM | is_member_append_lemma1 | T:. eq:{T}. L:T List. x:T.
x(eq) L (M,N:T List. y:T. ((eq x y)) c (L = M @ (y::N))) |
| THM | is_member_of_append_lemma | T:. eq:{T}. L,M:T List. x:T.
x(eq) (L @ M) x(eq) L x(eq) M |
| THM | is_member_append_disjunction_lemma | T:. eq:{T}. x:T. L,M:T List.
x(eq) (L @ M) x(eq) L x(eq) M |
| THM | append_commutes_under_is_member | T:. eq:{T}. L,M:T List. x:T.
x(eq) (L @ M) x(eq) (M @ L) |
| THM | append_commutes_under_sublist | T:. Discrete{T} (eq:{T}. L,M:T List. (L @ M)(eq)(M @ L)) |
| THM | append_commutes_under_list_iso | T:. Discrete{T} (eq:{T}. L,M:T List. (L @ M)(~eq)(M @ L)) |
| THM | append_functionality_wrt_sublist | T:. L1,L2:T List. eq1,eq2,eq3:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
eq2 = eq3
L1(eq1)L2
L3(eq2)L4
{(L1 @ L3)(eq3)(L2 @ L4)} |
| THM | append_is_member_lemma | T:. eq:{T=}. L:T List. x:T.
(M,N:T List. L = M @ (x::N)) x(eq) L |
| THM | is_member_non_nil | T:. eq:{T=}. u:T. L:T List.
u(eq) L (v:T. M:T List. L = (v::M)) |
| THM | is_member_remove_lemma | T:. eq:{T=}. L:T List. x:T.
x(eq) L (M,N:T List. L = M @ (x::N) remove(eq;x;L) = M @ N) |
| THM | is_member_tail | T:. eq:{T}. x:T. L:T List. x(eq) L (y:T. x(eq) (y::L)) |
| THM | is_member_equality_strengthening | T:. eq:{T=}. equiv:{T}. x:T. L:T List.
x(eq) L x(equiv) L |
| THM | append_distributes_over_filter | T:. P:T . L,M:T List.
filter((x.P[x]);(L @ M))
= filter((x.P[x]);L) @ filter((x.P[x]);M) |
| THM | is_member_filter_lemma | T:. eq:{T=}. P:T . L:T List. x:T.
x(eq) filter((x.P[x]);L) P[x] |
| THM | filter_is_member_lemma | T:. eq:{T=}. P:T . L:T List. x:T.
x(eq) L P[x] x(eq) filter((x.P[x]);L) |
| DISP | list_iso_df | <L1:List:L>(~<eq:equality:L>)<L2:List:L>== <L1>(~<eq>)<L2> |
| ABS | list_iso | L1(~eq)L2 == L1(eq)L2 L2(eq)L1 |
| THM | list_iso_wf | T:. eq:{T}. L1,L2:T List. L1(~eq)L2 |
| THM | comb_for_list_iso_wf | (T,eq,L1,L2,z.L1(~eq)L2) T:
eq:{T}
L1:T List
L2:T List
True
|
| ML | list_iso_unroll | let list_iso_nil_non_nil_unrollC =
FwdMacroC
`list_iso_nil_non_nil_unrollC`
(UnfoldC `list_iso`
ANDTHENC HigherC sublist_unrollC)
[](~eq)L
;;
let list_iso_cons_non_nil_unrollC =
FwdMacroC
`list_iso_cons_non_nil_unrollC`
(UnfoldC `list_iso`
ANDTHENC HigherC sublist_unrollC)
(u::v)(~eq)L
;;
let list_iso_unrollC =
list_iso_nil_non_nil_unrollC ORELSEC
list_iso_cons_non_nil_unrollC
;;
add_AbReduce_conv `list_iso` list_iso_unrollC;; |
| THM | list_iso_weakening_wrt_identity | T:. Discrete{T} (eq:{T}. L,M:T List. L = M L(~eq)M) |
| THM | list_iso_commutative | T:. eq:{T}. L,M:T List. L(~eq)M M(~eq)L |
| THM | list_iso_inversion | T:
Discrete{T}
(eq1,eq2:{T}. L,M:T List. eq1 = eq2 L(~eq1)M M(~eq2)L) |
| THM | list_iso_transitivity | T:
Discrete{T}
(eq1,eq2,eq3:{T}. L1,L2,L3:T List.
eq1 = eq2
eq2 = eq3
L1(~eq1)L2
L2(~eq2)L3
L1(~eq3)L3) |
| THM | append_functionality_wrt_list_iso | T:. L1,L2:T List. eq1,eq2,eq3:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
eq2 = eq3
L1(~eq1)L2
L3(~eq2)L4
{(L1 @ L3)(~eq3)(L2 @ L4)} |
| THM | sublist_functionality_wrt_id_list_iso_id | T:. L1,L2:T List. eq1,eq2:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
L1(~eq1)L2
L3 = L4
(L1(eq2)L3 L2(eq2)L4) |
| THM | sublist_functionality_wrt_id_id_list_iso | T:. L1,L2:T List. eq1,eq2:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
L1 = L2
{L3(~eq1)L4}
{L1(eq2)L3 L2(eq2)L4} |
| THM | sublist_functionality_wrt_id_list_iso_list_iso | T:. L1,L2:T List. eq1,eq2,eq3,eq4:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
eq2 = eq3
eq3 = eq4
{L1(~eq1)L2}
{L3(~eq2)L4}
{L1(eq3)L3 L2(eq4)L4} |
| THM | list_iso_functionality_wrt_id_list_iso_id | T:. L1,L2:T List. eq1,eq2:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
L1(~eq1)L2
L3 = L4
(L1(~eq2)L3 L2(~eq2)L4) |
| THM | list_iso_functionality_wrt_id_list_iso_list_iso | T:. L1,L2:T List. eq1,eq2,eq3:{T}. L3,L4:T List.
Discrete{T}
eq1 = eq2
eq2 = eq3
L1(~eq1)L2
L3(~eq2)L4
(L1(~eq3)L3 L2(~eq3)L4) |
| DISP | list_iso_2_df | (~<eq:equality:L>)== (~<eq>) |
| ABS | list_iso_2 | (~eq) == L,M.(eq) L M (eq) M L |
| THM | list_iso_2_wf | T:. eq:T T . (~eq) T List T List |
| THM | list_iso_iff_assert_list_iso_2 | T:
Discrete{T} (eq:{T}. L,M:T List. L(~eq)M ((~eq) L M)) |
| THM | decidable__list_iso | T:. eq:{T}. L,M:T List. Dec(L(~eq)M) |
| THM | decidable__equal_list | T:. (x,y:T. Dec(x = y)) (L,M:T List. Dec(L = M)) |
| THM | not_is_member_remove_lemma | T:. eq:{T=}. x,y:T. L:T List.
x(eq) L (eq x y) x(eq) remove(eq;y;L) |
| THM | remove_is_member_lemma | T:. eq:{T}. u:T. L:T List. v:T.
v(eq) remove(eq;u;L) v(eq) L |
| THM | list_all_map_lemma | T,R:. eq:{T=}. P:R . L:T List. f:T R.
xmap(f;L).P[x] (z:T. z(eq) L P[f z]) |
| THM | list_all_append_lemma | T:. P:T . L,M:T List.
x(L @ M).P[x] xL.P[x] xM.P[x] |
| THM | list_all_append_subtypes_lemma | T:. t1:{j}. t2:{k}.
t1 T
t2 T
(P:T . L:t1 List. M:t2 List.
x(L @ M).P[x] xL.P[x] xM.P[x]) |
| THM | list_exists_append_lemma | T:. P:T . L,M:T List.
x(L @ M).P[x] xL.P[x] xM.P[x] |
| THM | list_exists_is_member_append_lemma | T:. P:T . L:T List.
xL.P[x] (M,N:T List. x:T. P[x] L = M @ (x::N)) |
| THM | list_inc | T,R:. T R T List R List |
| THM | length_distributes_over_append | T:. L,M:T List. ||L @ M|| = ||L|| + ||M|| |
| THM | singelton_append_equals_lemma | T:. a:T. R,S:T List. b:T. (a::[]) = R @ (b::S) a = b |
| DISP | is_intersection_df | <M:list:L> (<eq:equality:*>)<N:list:L>== <M>(<eq>)<N> |
| ABS | is_intersection | L(eq)M == xL.(x(eq) M) |
| ML | is_intersection_unroll | let is_intersectionC t =
FwdMacroC
`is_intersection_unrollC`
(AllC[UnfoldC `is_intersection`;
list_exists_unrollC;
TryC is_member_unrollC;
TryC (FoldC `intersection`)]
)
t
;;
let is_intersection_unrollC =
FirstC [is_intersectionC [](eq)M;
is_intersectionC (x::L)(eq)M]
;;
add_AbReduce_conv `is_intersection` is_intersection_unrollC;; |
| THM | is_intersection_wf | T:. eq:{T}. L,M:T List. L(eq)M |
| THM | decidable__is_intersection | T:. eq:{T}. L,M:T List. Dec(L(eq)M) |
| THM | is_intersection_implies_exists_element | T:. eq:{T=}. L,M:T List.
L(eq)M (x:{x:T| x(eq) L} . x(eq) M) |