1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/lib/functions.ma".
16 include "apps_2/models/model_push.ma".
18 (* MODEL ********************************************************************)
20 record is_model (M): Prop ≝ {
21 mq: reflexive … (sq M);
22 mr: replace_2 … (sq M) (sq M) (sq M);
23 mc: compatible_3 … (ap M) (sq M) (sq M) (sq M);
24 ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;
25 ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i;
26 mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l;
27 md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[⟦V⟧[gv, lv]]lv];
28 mi: ∀gv,lv1,lv2,p,W,T. ⟦W⟧{M}[gv, lv1] ≗ ⟦W⟧{M}[gv, lv2] →
29 (∀d. ⟦T⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T⟧{M}[gv, ⫯[d]lv2]) →
30 ⟦ⓛ{p}W.T⟧[gv, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv, lv2];
31 ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv];
32 me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv];
33 mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[d]lv]
36 record is_extensional (M): Prop ≝ {
37 mx: ∀gv,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv, lv1] ≗ ⟦W2⟧{M}[gv, lv2] →
38 (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) →
39 ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2]
42 (* Basic properties *********************************************************)
44 lemma seq_sym (M): is_model M → symmetric … (sq M).
45 /3 width=5 by mr, mq/ qed-.
47 lemma seq_trans (M): is_model M → Transitive … (sq M).
48 /3 width=5 by mr, mq/ qed-.