Module nonExtensible:lists /*Holds if the first list contains everything in the second list and the first list contains everything in the second list*/ Fixed Judgment perm : [A] [A] /*Count haw many times an item occurs in a list*/ Fixed Judgment countItem : A [A] int /*Build a range list, inclusive*/ Fixed Judgment intRange : int int [int] ========== [Prm-Nil] perm [] [] select A L2 L perm Rest L2 ================ [Prm-Cons] perm (A::Rest) L ================ [Cnt-Nil] countItem X [] 0 countItem X Rest N 1 + N = N1 ====================== [Cnt-ConsEq] countItem X X::Rest N1 X != Y countItem X Rest N ===================== [Cnt-ConsNEq] countItem X Y::Rest N Low > High ==================== [IR-End] intRange Low High [] Low <= High 1 + Low = PlusOne intRange PlusOne High Rest =========================== [IR-Step] intRange Low High Low::Rest
Click on a command or tactic to see a detailed view of its use.
Module nonExtensible:lists. Theorem perm_mem [Item] : forall (L M : list Item) I, perm L M -> mem I L -> mem I M. [Show Proof] %Based on http://abella-prover.org/examples/first-order/lists.html Theorem prm_lemma [Item] : forall A B B' (X : Item), perm B' A -> select X B' B -> perm B (X::A). [Show Proof] Theorem perm_symmetric [Item] : forall (L M : list Item), perm L M -> perm M L. [Show Proof] Theorem no_lookup_perm [Key, Value] : forall (L P : list (pair Key Value)) (Key : Key), no_lookup L Key -> perm L P -> no_lookup P Key. [Show Proof] Theorem countItem_is_integer [Item] : forall (I : Item) L N, countItem I L N -> is_integer N. [Show Proof] Theorem countItem_geq_0 [Item] : forall (I : Item) L N, countItem I L N -> N >= 0. [Show Proof] Theorem select_countItem [Item] : forall (I : Item) L Rest N N', countItem I L N -> select I Rest L -> N - 1 = N' -> countItem I Rest N'. [Show Proof] Theorem countItem_select [Item] : forall (I : Item) L Rest N' N, countItem I Rest N' -> select I Rest L -> 1 + N' = N -> countItem I L N. [Show Proof] Theorem select_countItem_neq [Item] : forall (I J : Item) L Rest N, countItem I L N -> select J Rest L -> (I = J -> false) -> countItem I Rest N. [Show Proof] Theorem countItem_select_neq [Item] : forall (I J : Item) L Rest N, countItem I Rest N -> select J Rest L -> (I = J -> false) -> countItem I L N. [Show Proof] Theorem countItem_unique [Item] : forall (I : Item) NA NB L, countItem I L NA -> countItem I L NB -> NA = NB. [Show Proof] Theorem countItem_mem [Item] : forall (I : Item) N L, countItem I L N -> N > 0 -> mem I L. [Show Proof] Theorem countItem_not_mem [Item] : forall (I : Item) L, countItem I L 0 -> mem I L -> false. [Show Proof] Theorem countItem_greater_0 [Item] : forall (I : Item) L N, countItem I (I::L) N -> N > 0. [Show Proof] Theorem perm_countItems [Item] : forall L P (I : Item) NL NP, perm L P -> countItem I L NL -> countItem I P NP -> NL = NP. [Show Proof] Theorem intRange_is : forall Low High R, is_integer Low -> intRange Low High R -> is_list is_integer R. [Show Proof] Theorem intRange_low_lesseq : forall Low High R X, is_integer Low -> intRange Low High R -> mem X R -> Low <= X. [Show Proof] Theorem intRange_high_lesseq : forall Low High R X, is_integer Low -> intRange Low High R -> mem X R -> X <= High. [Show Proof] Theorem in_intRange : forall Low High R X, is_integer Low -> is_integer X -> intRange Low High R -> Low <= X -> X <= High -> mem X R. [Show Proof] Theorem intRange_unique : forall Low High R1 R2, intRange Low High R1 -> intRange Low High R2 -> R1 = R2. [Show Proof] Theorem intRange_smaller_exists : forall Low High R Low', is_integer Low -> is_integer Low' -> intRange Low High R -> Low < Low' -> exists R', intRange Low' High R'. [Show Proof] Theorem intRange_subset : forall Low Low' High R R', is_integer Low -> is_integer Low' -> intRange Low High R -> intRange Low' High R' -> Low < Low' -> subset R' R. [Show Proof] Theorem intRange_select_unique : forall Low High R X Rest Rest', is_integer Low -> intRange Low High R -> select X Rest R -> select X Rest' R -> Rest = Rest'. [Show Proof] Theorem intRange_exists : forall Low High, is_integer Low -> is_integer High -> exists R, intRange Low High R. [Show Proof]