]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_lemmas.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / multivm / multivm_lemmas.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "emulator/multivm/multivm.ma".
24 include "common/nat_lemmas.ma".
25
26 nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
27  #m; #t; #s; #err; #n;
28  ncases n;
29  ##[ ##2: #n1; ##]
30  nnormalize;
31  napply refl_eq.
32 nqed.
33
34 nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
35  #m; #t; #s; #susp; #n;
36  ncases n;
37  ##[ ##2: #n1; ##]
38  nnormalize;
39  napply refl_eq.
40 nqed.
41
42 nlemma breakpoint :
43  ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
44  #m; #t; #n1;
45  nelim n1;
46  ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply refl_eq
47  ##| ##2: #n3; #H; #n2; #s; ncases s;
48           ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply refl_eq
49           ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply refl_eq
50           ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
51                    nchange with ((execute m t (tick m t x) (n3+n2)) =
52                                  (execute m t (execute m t (tick m t x) n3) n2));
53                    nrewrite > (H n2 (tick m t x));
54                    napply refl_eq
55           ##]
56  ##]
57 nqed.