theory SigmaEx
imports Nominal "../QuotMain" "../QuotList" "../QuotProd"
begin

atom_decl name

datatype robj =
  rVar "name"
| rObj "(string \<times> rmethod) list"
| rInv "robj" "string"
| rUpd "robj" "string" "rmethod"
and rmethod =
  rSig "name" "robj"

(* Need to fix it, just 2 random rules *)
inductive
    alpha_obj :: "robj \<Rightarrow> robj \<Rightarrow> bool" ("_ \<approx>o _" [100, 100] 100)
and alpha_method :: "rmethod \<Rightarrow> rmethod \<Rightarrow> bool" ("_ \<approx>m _" [100, 100] 100)
where
  a1: "a = b \<Longrightarrow> (rVar a) \<approx>o (rVar b)"
| a2: "a = b \<and> c = d \<Longrightarrow> rSig a c \<approx>m rSig b d"

lemma alpha_equivps:
  shows "equivp alpha_obj"
  and   "equivp alpha_method"
sorry

quotient_type
    obj = robj / alpha_obj
and method = rmethod / alpha_method
  by (auto intro: alpha_equivps)

quotient_definition
  "Var :: name \<Rightarrow> obj"
as
  "rVar"

quotient_definition
  "Obj :: (string \<times> method) list \<Rightarrow> obj"
as
  "rObj"

quotient_definition
  "Inv :: obj \<Rightarrow> string \<Rightarrow> obj"
as
  "rInv"

quotient_definition
  "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj"
as
  "rUpd"

quotient_definition
  "Sig :: name \<Rightarrow> obj \<Rightarrow> method"
as
  "rSig"

overloading
  perm_obj \<equiv> "perm :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" (unchecked)
  perm_method   \<equiv> "perm :: 'x prm \<Rightarrow> method \<Rightarrow> method" (unchecked)
begin

quotient_definition
  "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj"
as
  "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)"

quotient_definition
  "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method"
as
  "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)"

end

lemma tolift:
"\<forall> fvar.
 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<forall> fnil.
 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).

 \<exists> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd)
 \<in> Respects
   (prod_rel (alpha_obj ===> op =)
     (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =)
       (prod_rel ((prod_rel (op =) alpha_method) ===> op =)
         (alpha_method ===> op =)
       )
     )
   ).

(
 (\<forall>x. hom_o (rVar x) = fvar x) \<and>
 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and>
 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
 (hom_d [] = fnil) \<and>
 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
)"
sorry

syntax
  "_expttrn"        :: "pttrn => bool => bool"      ("(3\<exists>\<exists> _./ _)" [0, 10] 10)

translations
  "\<exists>\<exists> x. P"   == "Ex (%x. P)"

lemma split_rsp[quot_respect]: "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
by auto

lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
by (simp add: a1)

lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj"
sorry
lemma rinv_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_obj) rInv rInv"
sorry
lemma rupd_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_method ===> alpha_obj) rUpd rUpd"
sorry
lemma rsig_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_method) rSig rSig"
sorry
lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>"
sorry

lemma liftd: "
\<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))).
(
 (\<forall>x. hom_o (Var x) = fvar x) \<and>
 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
 (hom_d [] = fnil) \<and>
 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
)"
apply (lifting tolift)
apply (regularize)
apply (simp)
prefer 2
apply cleaning
apply simp
sorry

lemma tolift':
"\<forall> fvar.
 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<forall> fnil.
 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).

 \<exists> hom_o\<Colon>robj \<Rightarrow> 'a \<in> Respects (alpha_obj ===> op =).
 \<exists> hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b \<in> Respects (list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<exists> hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c \<in> Respects ((prod_rel (op =) alpha_method) ===> op =).
 \<exists> hom_m\<Colon>rmethod \<Rightarrow> 'd \<in> Respects (alpha_method ===> op =).
(
 (\<forall>x. hom_o (rVar x) = fvar x) \<and>
 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and>
 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
 (hom_d [] = fnil) \<and>
 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
)"
sorry

lemma liftd': "
\<exists>hom_o. \<exists>hom_d. \<exists>hom_e. \<exists>hom_m.
(
 (\<forall>x. hom_o (Var x) = fvar x) \<and>
 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
 (hom_d [] = fnil) \<and>
 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
)"
apply (lifting tolift')
done

lemma tolift'':
"\<forall> fvar.
 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
 \<forall> fnil.
 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).

 Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
 Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
 Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
 Bexeq (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd.
(
 (\<forall>x. hom_o (rVar x) = fvar x) \<and>
 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and>
 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
 (hom_d [] = fnil) \<and>
 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
)
))))"
sorry

lemma liftd'': "
\<exists>!hom_o. \<exists>!hom_d. \<exists>!hom_e. \<exists>!hom_m.
(
 (\<forall>x. hom_o (Var x) = fvar x) \<and>
 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
 (hom_d [] = fnil) \<and>
 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
)"
apply (lifting tolift'')
done


end