Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/QuotBase.thy
changeset 1122 d1eaed018e5d
parent 1116 3acc7d25627a
child 1123 41f89d4f9548
equal deleted inserted replaced
1121:8d3f92694e85 1122:d1eaed018e5d 
     1 (*  Title:      QuotBase.thy
 
     1 (*  Title:      QuotBase.thy
 
     2     Author:     Cezary Kaliszyk and Christian Urban
 
     2     Author:     Cezary Kaliszyk and Christian Urban
 
     3 *)
 
     3 *)
 
     4 
     4 
     5 theory QuotBase
 
     5 theory QuotBase
 
     6 imports Plain ATP_Linkup Predicate
 
     6 imports Plain ATP_Linkup
 
     7 begin
 
     7 begin
 
     8 
     8 
     9 text {*
 
     9 text {*
 
    10   Basic definition for equivalence relations
 
    10   Basic definition for equivalence relations
 
    11   that are represented by predicates.
 
    11   that are represented by predicates.
 
    12 *}
 
    12 *}
 
    13 
    13 
    14 definition
 
    14 (* TODO check where definitions can be changed to \<longleftrightarrow> *)
 
    15   "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
 
    15 definition
 
    16 
    16   "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
 
    17 definition
 
    17 
    18   "reflp E \<equiv> \<forall>x. E x x"
 
    18 definition
 
    19 
    19   "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
 
    20 definition
 
    20 
    21   "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
 
    21 definition
 
    22 
    22   "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
 
    23 definition
 
    23 
    24   "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
 
    24 definition
 
       
    25   "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
 
    25 
    26 
    26 lemma equivp_reflp_symp_transp:
 
    27 lemma equivp_reflp_symp_transp:
 
    27   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
 
    28   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
 
    28   unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
 
    29   unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
 
    29   by blast
 
    30   by blast
 
    30 
    31 
    31 lemma equivp_reflp:
 
    32 lemma equivp_reflp:
 
    32   shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
 
    33   shows "equivp E \<Longrightarrow> E x x"
 
    33   by (simp only: equivp_reflp_symp_transp reflp_def)
 
    34   by (simp only: equivp_reflp_symp_transp reflp_def)
 
    34 
    35 
    35 lemma equivp_symp:
 
    36 lemma equivp_symp:
 
    36   shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
 
    37   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
 
    37   by (metis equivp_reflp_symp_transp symp_def)
 
    38   by (metis equivp_reflp_symp_transp symp_def)
 
    38 
    39 
    39 lemma equivp_transp:
 
    40 lemma equivp_transp:
 
    40   shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
 
    41   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
 
    41   by (metis equivp_reflp_symp_transp transp_def)
 
    42   by (metis equivp_reflp_symp_transp transp_def)
 
    42 
    43 
    43 lemma equivpI:
 
    44 lemma equivpI:
 
    44   assumes "reflp R" "symp R" "transp R"
 
    45   assumes "reflp R" "symp R" "transp R"
 
    45   shows "equivp R"
 
    46   shows "equivp R"
 
    55   by auto
 
    56   by auto
 
    56 
    57 
    57 
    58 
    58 text {* Partial equivalences: not yet used anywhere *}
 
    59 text {* Partial equivalences: not yet used anywhere *}
 
    59 definition
 
    60 definition
 
    60   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
    61   "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))"
 
    61 
    62 
    62 lemma equivp_implies_part_equivp:
 
    63 lemma equivp_implies_part_equivp:
 
    63   assumes a: "equivp E"
 
    64   assumes a: "equivp E"
 
    64   shows "part_equivp E"
 
    65   shows "part_equivp E"
 
    65   using a 
    66   using a 
    79 section {* Respects predicate *}
 
    80 section {* Respects predicate *}
 
    80 
    81 
    81 definition
 
    82 definition
 
    82   Respects
 
    83   Respects
 
    83 where
 
    84 where
 
    84   "Respects R x \<equiv> (R x x)"
 
    85   "Respects R x \<longleftrightarrow> (R x x)"
 
    85 
    86 
    86 lemma in_respects:
 
    87 lemma in_respects:
 
    87   shows "(x \<in> Respects R) = R x x"
 
    88   shows "(x \<in> Respects R) = R x x"
 
    88   unfolding mem_def Respects_def 
    89   unfolding mem_def Respects_def 
    89   by simp
 
    90   by simp
 
   121 
   122 
   122 
   123 
   123 section {* Quotient Predicate *}
 
   124 section {* Quotient Predicate *}
 
   124 
   125 
   125 definition
 
   126 definition
 
   126   "Quotient E Abs Rep \<equiv> 
   127   "Quotient E Abs Rep \<longleftrightarrow>
 
   127      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
 
   128      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
 
   128      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
   129      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
   129 
   130 
   130 lemma Quotient_abs_rep:
 
   131 lemma Quotient_abs_rep:
 
   131   assumes a: "Quotient E Abs Rep"
 
   132   assumes a: "Quotient E Abs Rep"
 
   376 section {* Bounded abstraction *}
 
   377 section {* Bounded abstraction *}
 
   377 
   378 
   378 definition
 
   379 definition
 
   379   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
   380   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
   380 where
 
   381 where
 
   381   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
   382   "x \<in> p \<Longrightarrow> Babs p m x = m x"
 
   382 
   383 
   383 lemma babs_rsp:
 
   384 lemma babs_rsp:
 
   384   assumes q: "Quotient R1 Abs1 Rep1"
 
   385   assumes q: "Quotient R1 Abs1 Rep1"
 
   385   and     a: "(R1 ===> R2) f g"
 
   386   and     a: "(R1 ===> R2) f g"
 
   386   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
 
   387   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
 
   454 section {* Bex1_rel quantifier *}
 
   455 section {* Bex1_rel quantifier *}
 
   455 
   456 
   456 definition
 
   457 definition
 
   457   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 
   458   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 
   458 where
 
   459 where
 
   459   "Bex1_rel R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
 
   460   "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
 
   460 
   461 
   461 lemma bex1_rel_aux:
 
   462 lemma bex1_rel_aux:
 
   462   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
 
   463   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
 
   463   unfolding Bex1_rel_def
 
   464   unfolding Bex1_rel_def
 
   464   apply (erule conjE)+
 
   465   apply (erule conjE)+
 
   611   and     a1: "(R1 ===> R2) f g"
 
   612   and     a1: "(R1 ===> R2) f g"
 
   612   and     a2: "R1 x y"
 
   613   and     a2: "R1 x y"
 
   613   shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
 
   614   shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
 
   614   using apply_rsp[OF q1 a1] a2 by auto
 
   615   using apply_rsp[OF q1 a1] a2 by auto
 
   615 
   616 
   616 
       
   617 (*** REST OF THE FILE IS UNUSED (until now) ***)
 
       
   618 
       
   619 text {*
 
       
   620 lemma in_fun:
 
       
   621   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
 
       
   622   by (simp add: mem_def)
 
       
   623 
       
   624 lemma respects_thm:
 
       
   625   shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
 
       
   626   unfolding Respects_def
 
       
   627   by (simp add: expand_fun_eq)
 
       
   628 
       
   629 lemma respects_rep_abs:
 
       
   630   assumes a: "Quotient R1 Abs1 Rep1"
 
       
   631   and     b: "Respects (R1 ===> R2) f"
 
       
   632   and     c: "R1 x x"
 
       
   633   shows "R2 (f (Rep1 (Abs1 x))) (f x)"
 
       
   634   using a b[simplified respects_thm] c unfolding Quotient_def
 
       
   635   by blast
 
       
   636 
       
   637 lemma respects_mp:
 
       
   638   assumes a: "Respects (R1 ===> R2) f"
 
       
   639   and     b: "R1 x y"
 
       
   640   shows "R2 (f x) (f y)"
 
       
   641   using a b unfolding Respects_def
 
       
   642   by simp
 
       
   643 
       
   644 lemma respects_o:
 
       
   645   assumes a: "Respects (R2 ===> R3) f"
 
       
   646   and     b: "Respects (R1 ===> R2) g"
 
       
   647   shows "Respects (R1 ===> R3) (f o g)"
 
       
   648   using a b unfolding Respects_def
 
       
   649   by simp
 
       
   650 
       
   651 lemma fun_rel_eq_rel:
 
       
   652   assumes q1: "Quotient R1 Abs1 Rep1"
 
       
   653   and     q2: "Quotient R2 Abs2 Rep2"
 
       
   654   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
 
       
   655                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
 
       
   656   using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
 
       
   657   by blast
 
       
   658 
       
   659 lemma let_babs:
 
       
   660   "v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"
 
       
   661   by (simp add: Babs_def)
 
       
   662 
       
   663 lemma fun_rel_equals:
 
       
   664   assumes q1: "Quotient R1 Abs1 Rep1"
 
       
   665   and     q2: "Quotient R2 Abs2 Rep2"
 
       
   666   and     r1: "Respects (R1 ===> R2) f"
 
       
   667   and     r2: "Respects (R1 ===> R2) g"
 
       
   668   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 
       
   669   apply(rule_tac iffI)
 
       
   670   apply(rule)+
 
       
   671   apply (rule apply_rsp'[of "R1" "R2"])
 
       
   672   apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
 
       
   673   apply auto
 
       
   674   using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
 
       
   675   apply (metis let_rsp q1)
 
       
   676   apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
 
       
   677   using r1 unfolding Respects_def expand_fun_eq
 
       
   678   apply(simp (no_asm_use))
 
       
   679   apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
 
       
   680   done
 
       
   681 
       
   682 (* ask Peter: fun_rel_IMP used twice *) 
       
   683 lemma fun_rel_IMP2:
 
       
   684   assumes q1: "Quotient R1 Abs1 Rep1"
 
       
   685   and     q2: "Quotient R2 Abs2 Rep2"
 
       
   686   and     r1: "Respects (R1 ===> R2) f"
 
       
   687   and     r2: "Respects (R1 ===> R2) g" 
       
   688   and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
 
       
   689   shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
 
       
   690   using q1 q2 r1 r2 a
 
       
   691   by (simp add: fun_rel_equals)
 
       
   692 
       
   693 lemma lambda_rep_abs_rsp:
 
       
   694   assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
 
       
   695   and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
 
       
   696   shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
 
       
   697   using r1 r2 by auto
 
       
   698 
       
   699 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
 
       
   700 lemma id_prs:
 
       
   701   assumes q: "Quotient R Abs Rep"
 
       
   702   shows "Abs (id (Rep e)) = id e"
 
       
   703   using Quotient_abs_rep[OF q] by auto
 
       
   704 
       
   705 lemma id_rsp:
 
       
   706   assumes q: "Quotient R Abs Rep"
 
       
   707   and     a: "R e1 e2"
 
       
   708   shows "R (id e1) (id e2)"
 
       
   709   using a by auto
 
       
   710 
       
   711 *}
 
       
   712 
       
   713 end
 
   617 end
 
   714 
   618
nominal2