matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.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 include "ground/relocation/pr_isi_eq.ma".
  16 include "ground/relocation/pr_sor_eq.ma".
  17 include "ground/relocation/pr_sor_sor.ma".
  18
  19 (* RELATIONAL UNION FOR PARTIAL RELOCATION MAPS *****************************)
  20
  21 (* Constructions with pr_isi ************************************************)
  22
  23 (*** sor_isid_sn *)
  24 corec lemma pr_sor_isi_sn:
  25             ∀f1. 𝐈❨f1❩ → ∀f2. f1 ⋓ f2 ≘ f2.
  26 #f1 * -f1
  27 #f1 #g1 #Hf1 #H1 #f2 cases (pr_map_split_tl f2)
  28 /3 width=7 by pr_sor_push_bi, pr_sor_push_next/
  29 qed.
  30
  31 (*** sor_isid_dx *)
  32 corec lemma pr_sor_isi_dx:
  33             ∀f2. 𝐈❨f2❩ → ∀f1. f1 ⋓ f2 ≘ f1.
  34 #f2 * -f2
  35 #f2 #g2 #Hf2 #H2 #f1 cases (pr_map_split_tl f1)
  36 /3 width=7 by pr_sor_push_bi, pr_sor_next_push/
  37 qed.
  38
  39 (*** sor_isid *)
  40 lemma pr_sor_isi_bi_isi:
  41       ∀f1,f2,f. 𝐈❨f1❩ → 𝐈❨f2❩ → 𝐈❨f❩ → f1 ⋓ f2 ≘ f.
  42 /4 width=3 by pr_sor_eq_repl_back_dx, pr_sor_eq_repl_back_sn, pr_isi_inv_eq_repl/ qed.
  43
  44
  45 (* Destructions with pr_isi *************************************************)
  46
  47 (*** sor_fwd_isid1 *)
  48 corec lemma pr_sor_des_isi_sn:
  49             ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f❩ → 𝐈❨f1❩.
  50 #f1 #f2 #f * -f1 -f2 -f
  51 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H #Hg
  52 [ /4 width=6 by pr_isi_inv_push, pr_isi_push/ ]
  53 cases (pr_isi_inv_next … Hg … H)
  54 qed-.
  55
  56 (*** sor_fwd_isid2 *)
  57 corec lemma pr_sor_des_isi_dx:
  58             ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f❩ → 𝐈❨f2❩.
  59 #f1 #f2 #f * -f1 -f2 -f
  60 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H #Hg
  61 [ /4 width=6 by pr_isi_inv_push, pr_isi_push/ ]
  62 cases (pr_isi_inv_next … Hg … H)
  63 qed-.
  64
  65 (* Inversions with pr_isi ***************************************************)
  66
  67 (*** sor_isid_inv_sn *)
  68 lemma pr_sor_inv_isi_sn:
  69       ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f1❩ → f2 ≡ f.
  70 /3 width=4 by pr_sor_isi_sn, pr_sor_mono/
  71 qed-.
  72
  73 (*** sor_isid_inv_dx *)
  74 lemma pr_sor_inv_isi_dx:
  75       ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f2❩ → f1 ≡ f.
  76 /3 width=4 by pr_sor_isi_dx, pr_sor_mono/
  77 qed-.
  78
  79 (*** sor_inv_isid3 *)
  80 lemma pr_sor_inv_isi:
  81       ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f❩ →
  82       ∧∧ 𝐈❨f1❩ & 𝐈❨f2❩.
  83 /3 width=4 by pr_sor_des_isi_dx, pr_sor_des_isi_sn, conj/ qed-.