diff -r a6f3e1b08494 -r b6873d123f9b Attic/Quot/Examples/SigmaEx.thy
--- a/Attic/Quot/Examples/SigmaEx.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,253 +0,0 @@
-theory SigmaEx
-imports Nominal "../Quotient" "../Quotient_List" "../Quotient_Product"
-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"
-
-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: "rObj [] \<approx>o rObj []"
-| a3: "rObj t1 \<approx>o rObj t2 \<Longrightarrow> m1 \<approx>m r2 \<Longrightarrow> rObj ((l1, m1) # t1) \<approx>o rObj ((l2, m2) # t2)"
-| a4: "x \<approx>o y \<Longrightarrow> rInv x l1 \<approx>o rInv y l2"
-| a5: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>o s \<and> (pi \<bullet> a) = b)
-       \<Longrightarrow> rSig a t \<approx>m rSig b s"
-
-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"
-is
-  "rVar"
-
-quotient_definition
-  "Obj :: (string \<times> method) list \<Rightarrow> obj"
-is
-  "rObj"
-
-quotient_definition
-  "Inv :: obj \<Rightarrow> string \<Rightarrow> obj"
-is
-  "rInv"
-
-quotient_definition
-  "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj"
-is
-  "rUpd"
-
-quotient_definition
-  "Sig :: name \<Rightarrow> obj \<Rightarrow> method"
-is
-  "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"
-is
-  "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)"
-
-quotient_definition
-  "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method"
-is
-  "(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 =).
-
- Ex1 (\<lambda>x.
-(x \<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 =)
-       )
-     )))) \<and>
-(\<lambda> (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).
-
-((\<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))
-)) x) "
-sorry
-
-lemma test_to: "Ex1 (\<lambda>x. (x \<in> (Respects alpha_obj)) \<and> P x)"
-ML_prf {* prop_of (#goal (Isar.goal ())) *}
-sorry
-lemma test_tod: "Ex1 (P :: obj \<Rightarrow> bool)"
-apply (lifting test_to)
-done
-
-
-
-
-(*syntax
-  "_expttrn"        :: "pttrn => bool => bool"      ("(3\<exists>\<exists> _./ _)" [0, 10] 10)
-
-translations
-  "\<exists>\<exists> x. P"   == "Ex (%x. P)"
-*)
-
-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 bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
-apply (simp add: Ex1_def Bex1_rel_def in_respects)
-apply clarify
-apply auto
-apply (rule bexI)
-apply assumption
-apply (simp add: in_respects)
-apply (simp add: in_respects)
-apply auto
-done
-
-lemma liftd: "
-Ex1 (\<lambda>(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)
-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 =).
-
- \<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 =).
-
- Bex1_rel (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
- Bex1_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
- Bex1_rel ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
- Bex1_rel (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
-