Executable Specification

[View schm_poly_tst.sig] [View schm_poly_tst.mod]
sig schm_poly_tst.

type app   list A -> list A -> list A -> o.

kind i     type.
type cst   A -> i.
type pred  i -> o.
module schm_poly_tst.

app nil L L.
app (X :: L1) L2 (X :: L3) :- app L1 L2 L3.

pred (cst X).

Reasoning

[View schm_poly_tst.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "schm_poly_tst".

% Set types on. 
% Set instantiations on.

Define append : list A -> list A -> list A -> prop by
  append nil L L;
  append (X :: L1) L2 (X :: L3) := append L1 L2 L3.

Theorem append_det[A] : forall (L1: list A) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.

Theorem oappend_det : forall (L1: list o) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.

Theorem append_det1[A] : forall (L1: list A) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.

Theorem append_det2[A] : forall (L1: list A) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.

Theorem append_det3[A] : forall (L1: list A) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.


%% Do not support types with a variable as its target
% Type fst,snd   list A -> A.
Type p   A -> o.

Define eq : A -> A -> prop by
  eq M M.

Theorem tst [A,B] : forall (X:A) (Y:B),
  eq (p X) (p Y) -> false.
intros. %% The following case analysis should report an error that %% generic type variables cannot be instantiated % case H1. skip.
Theorem inst_gen_var1[A,B] : forall (X:A) (Y:B), p X = p Y -> false.
intros. %% The following case analysis should report an error that %% generic type variables cannot be instantiated % case H1. skip.
Theorem inst_gen_var2[A] : forall (X:A) (Y:o), p X = p Y -> false.
intros. % case H1. skip.
Theorem inst_gen_var3[A] : forall (X:i) (Y:o), p X = p Y -> false. Theorem member_prune[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem olist_mem_prune : forall M (L:list o), nabla (x:o), member (M x) L -> exists M', M = y\M'. Theorem member_prune1[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem member_prune2[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem member_prune3[A,B] : forall M (L:list A), nabla (x:i), member (M x) L -> exists M', M = y\M'. Theorem member_prune4[A,B] : forall M (L:list A), nabla (x:i), member (M x) L -> exists M', M = y\M'. Theorem olist_mem_prune_bc : forall M (L:list o), nabla (x:o), member (M x) L -> exists M', M = y\M'. Theorem member_prune1_bc[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem app_det[A] : forall (L1: list A) L2 L3 L3', {app L1 L2 L3} -> {app L1 L2 L3'} -> L3 = L3'. Theorem app_search[A] : forall (X:A) L, {app (X :: nil) L (X :: L)}. Theorem ty_fdet_left[A] : forall (X:A), {pred (cst X)} -> true. Theorem ty_fdet_right[A] : forall (X:A), {pred (cst X)}. Theorem ty_not_fdet_left : forall M, {pred M} -> false.
intros. %% The following case analysis should report an error because the %% type variable in the clause cannot be fully instantiated by unification % case H1. skip.
Theorem ty_not_fdet_right : forall M, {pred M}.
%% The following search should fail because the type variable in the %% clause cannot be fully instantiated by unification %search. skip.