1 theory QuotScript

     2 imports Main

     3 begin

     4 

     5 definition 

     6   "EQUIV E \<equiv> \<forall>x y. E x y = (E x = E y)" 

     7 

     8 definition

     9   "REFL E \<equiv> \<forall>x. E x x"

    10 

    11 definition 

    12   "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"

    13 

    14 definition

    15   "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"

    16 

    17 lemma EQUIV_REFL_SYM_TRANS:

    18   shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)"

    19 unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq

    20 by (blast)

    21 

    22 definition

    23   "PART_EQUIV 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)))"

    24 

    25 lemma EQUIV_IMP_PART_EQUIV:

    26   assumes a: "EQUIV E"

    27   shows "PART_EQUIV E"

    28 using a unfolding EQUIV_def PART_EQUIV_def

    29 by auto

    30 

    31 definition

    32   "QUOTIENT E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 

    33                         (\<forall>a. E (Rep a) (Rep a)) \<and> 

    34                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"

    35 

    36 lemma QUOTIENT_ABS_REP:

    37   assumes a: "QUOTIENT E Abs Rep"

    38   shows "Abs (Rep a) = a" 

    39 using a unfolding QUOTIENT_def

    40 by simp

    41 

    42 lemma QUOTIENT_REP_REFL:

    43   assumes a: "QUOTIENT E Abs Rep"

    44   shows "E (Rep a) (Rep a)" 

    45 using a unfolding QUOTIENT_def

    46 by blast

    47 

    48 lemma QUOTIENT_REL:

    49   assumes a: "QUOTIENT E Abs Rep"

    50   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"

    51 using a unfolding QUOTIENT_def

    52 by blast

    53 

    54 lemma QUOTIENT_REL_ABS:

    55   assumes a: "QUOTIENT E Abs Rep"

    56   shows "E r s \<Longrightarrow> Abs r = Abs s"

    57 using a unfolding QUOTIENT_def

    58 by blast

    59 

    60 lemma QUOTIENT_REL_ABS_EQ:

    61   assumes a: "QUOTIENT E Abs Rep"

    62   shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"

    63 using a unfolding QUOTIENT_def

    64 by blast

    65 

    66 lemma QUOTIENT_REL_REP:

    67   assumes a: "QUOTIENT E Abs Rep"

    68   shows "E (Rep a) (Rep b) = (a = b)"

    69 using a unfolding QUOTIENT_def

    70 by metis

    71 

    72 lemma QUOTIENT_REP_ABS:

    73   assumes a: "QUOTIENT E Abs Rep"

    74   shows "E r r \<Longrightarrow> E (Rep (Abs r)) r"

    75 using a unfolding QUOTIENT_def

    76 by blast

    77 

    78 lemma IDENTITY_EQUIV:

    79   shows "EQUIV (op =)"

    80 unfolding EQUIV_def

    81 by auto

    82 

    83 lemma IDENTITY_QUOTIENT:

    84   shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"

    85 unfolding QUOTIENT_def

    86 by blast

    87 

    88 lemma QUOTIENT_SYM:

    89   assumes a: "QUOTIENT E Abs Rep"

    90   shows "SYM E"

    91 using a unfolding QUOTIENT_def SYM_def

    92 by metis

    93 

    94 lemma QUOTIENT_TRANS:

    95   assumes a: "QUOTIENT E Abs Rep"

    96   shows "TRANS E"

    97 using a unfolding QUOTIENT_def TRANS_def

    98 by metis

    99 

   100 fun

   101   fun_map 

   102 where

   103   "fun_map f g h x = g (h (f x))"

   104 

   105 abbreviation

   106   fun_map_syn ("_ ---> _")

   107 where

   108   "f ---> g \<equiv> fun_map f g"  

   109 

   110 lemma FUN_MAP_I:

   111   shows "(\<lambda>x. x ---> \<lambda>x. x) = (\<lambda>x. x)"

   112 by (simp add: expand_fun_eq)

   113 

   114 lemma IN_FUN:

   115   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"

   116 by (simp add: mem_def)

   117 

   118 fun

   119   FUN_REL 

   120 where

   121   "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"

   122 

   123 abbreviation

   124   FUN_REL_syn ("_ ===> _")

   125 where

   126   "E1 ===> E2 \<equiv> FUN_REL E1 E2"  

   127 

   128 lemma FUN_REL_EQ:

   129   "(op =) ===> (op =) = (op =)"

   130 by (simp add: expand_fun_eq)

   131 

   132 lemma FUN_QUOTIENT:

   133   assumes q1: "QUOTIENT R1 abs1 rep1"

   134   and     q2: "QUOTIENT R2 abs2 rep2"

   135   shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"

   136 proof -

   137   have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"

   138     apply(simp add: expand_fun_eq)

   139     using q1 q2

   140     apply(simp add: QUOTIENT_def)

   141     done

   142   moreover

   143   have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"

   144     apply(auto)

   145     using q1 q2 unfolding QUOTIENT_def

   146     apply(metis)

   147     done

   148   moreover

   149   have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 

   150         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"

   151     apply(auto simp add: expand_fun_eq)

   152     using q1 q2 unfolding QUOTIENT_def

   153     apply(metis)

   154     using q1 q2 unfolding QUOTIENT_def

   155     apply(metis)

   156     using q1 q2 unfolding QUOTIENT_def

   157     apply(metis)

   158     using q1 q2 unfolding QUOTIENT_def

   159     apply(metis)

   160     done

   161   ultimately

   162   show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"

   163     unfolding QUOTIENT_def by blast

   164 qed

   165 

   166 definition

   167   Respects

   168 where

   169   "Respects R x \<equiv> (R x x)"

   170 

   171 lemma IN_RESPECTS:

   172   shows "(x \<in> Respects R) = R x x"

   173 unfolding mem_def Respects_def by simp

   174 

   175 lemma RESPECTS_THM:

   176   shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"

   177 unfolding Respects_def

   178 by (simp add: expand_fun_eq) 

   179 

   180 lemma RESPECTS_MP:

   181   assumes a: "Respects (R1 ===> R2) f"

   182   and     b: "R1 x y"

   183   shows "R2 (f x) (f y)"

   184 using a b unfolding Respects_def

   185 by simp

   186 

   187 lemma RESPECTS_REP_ABS:

   188   assumes a: "QUOTIENT R1 Abs1 Rep1"

   189   and     b: "Respects (R1 ===> R2) f"

   190   and     c: "R1 x x"

   191   shows "R2 (f (Rep1 (Abs1 x))) (f x)"

   192 using a b[simplified RESPECTS_THM] c unfolding QUOTIENT_def

   193 by blast

   194 

   195 lemma RESPECTS_o:

   196   assumes a: "Respects (R2 ===> R3) f"

   197   and     b: "Respects (R1 ===> R2) g"

   198   shows "Respects (R1 ===> R3) (f o g)"

   199 using a b unfolding Respects_def

   200 by simp

   201 

   202 (*

   203 definition

   204   "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> 

   205                           (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"

   206 *)

   207 

   208 lemma FUN_REL_EQ_REL:

   209   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   210   and     q2: "QUOTIENT R2 Abs2 Rep2"

   211   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 

   212                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"

   213 using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq

   214 by blast

   215 

   216 (* q1 and q2 not used; see next lemma *)

   217 lemma FUN_REL_MP:

   218   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   219   and     q2: "QUOTIENT R2 Abs2 Rep2"

   220   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"

   221 by simp

   222 

   223 lemma FUN_REL_IMP:

   224   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"

   225 by simp

   226 

   227 lemma FUN_REL_EQUALS:

   228   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   229   and     q2: "QUOTIENT R2 Abs2 Rep2"

   230   and     r1: "Respects (R1 ===> R2) f"

   231   and     r2: "Respects (R1 ===> R2) g" 

   232   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"

   233 apply(rule_tac iffI)

   234 using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def

   235 apply(metis FUN_REL_IMP)

   236 using r1 unfolding Respects_def expand_fun_eq

   237 apply(simp (no_asm_use))

   238 apply(metis QUOTIENT_REL[OF q2] QUOTIENT_REL_REP[OF q1])

   239 done

   240 

   241 (* ask Peter: FUN_REL_IMP used twice *) 

   242 lemma FUN_REL_IMP2:

   243   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   244   and     q2: "QUOTIENT R2 Abs2 Rep2"

   245   and     r1: "Respects (R1 ===> R2) f"

   246   and     r2: "Respects (R1 ===> R2) g" 

   247   and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"

   248   shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"

   249 using q1 q2 r1 r2 a

   250 by (simp add: FUN_REL_EQUALS)

   251 

   252 lemma EQUALS_PRS:

   253   assumes q: "QUOTIENT R Abs Rep"

   254   shows "(x = y) = R (Rep x) (Rep y)"

   255 by (simp add: QUOTIENT_REL_REP[OF q]) 

   256 

   257 lemma EQUALS_RSP:

   258   assumes q: "QUOTIENT R Abs Rep"

   259   and     a: "R x1 x2" "R y1 y2"

   260   shows "R x1 y1 = R x2 y2"

   261 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def

   262 using a by blast

   263 

   264 lemma LAMBDA_PRS:

   265   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   266   and     q2: "QUOTIENT R2 Abs2 Rep2"

   267   shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))"

   268 unfolding expand_fun_eq

   269 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]

   270 by simp

   271 

   272 lemma LAMBDA_PRS1:

   273   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   274   and     q2: "QUOTIENT R2 Abs2 Rep2"

   275   shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"

   276 unfolding expand_fun_eq

   277 by (subst LAMBDA_PRS[OF q1 q2]) (simp)

   278 

   279 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)

   280 lemma LAMBDA_RSP:

   281   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   282   and     q2: "QUOTIENT R2 Abs2 Rep2"

   283   and     a: "(R1 ===> R2) f1 f2"

   284   shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"

   285 by (rule a)

   286 

   287 (* ASK Peter about next four lemmas in quotientScript

   288 lemma ABSTRACT_PRS:

   289   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   290   and     q2: "QUOTIENT R2 Abs2 Rep2"

   291   shows "f = (Rep1 ---> Abs2) ???"

   292 *)

   293 

   294 lemma LAMBDA_REP_ABS_RSP:

   295   assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"

   296   and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"

   297   shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"

   298 using r1 r2 by auto

   299 

   300 lemma REP_ABS_RSP:

   301   assumes q: "QUOTIENT R Abs Rep"

   302   and     a: "R x1 x2"

   303   shows "R x1 (Rep (Abs x2))"

   304 using a

   305 by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])

   306 

   307 (* ----------------------------------------------------- *)

   308 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)

   309 (*              RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)

   310 (* ----------------------------------------------------- *)

   311 

   312 (* what is RES_FORALL *)

   313 (*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>

   314          !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*)

   315 (*as peter here *)

   316 

   317 (* bool theory: COND, LET *)

   318 

   319 lemma IF_PRS:

   320   assumes q: "QUOTIENT R Abs Rep"

   321   shows "If a b c = Abs (If a (Rep b) (Rep c))"

   322 using QUOTIENT_ABS_REP[OF q] by auto

   323 

   324 (* ask peter: no use of q *)

   325 lemma IF_RSP:

   326   assumes q: "QUOTIENT R Abs Rep"

   327   and     a: "a1 = a2" "R b1 b2" "R c1 c2"

   328   shows "R (If a1 b1 c1) (If a2 b2 c2)"

   329 using a by auto

   330 

   331 lemma LET_PRS:

   332   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   333   and     q2: "QUOTIENT R2 Abs2 Rep2"

   334   shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"

   335 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto

   336 

   337 lemma LET_RSP:

   338   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   339   and     q2: "QUOTIENT R2 Abs2 Rep2"

   340   and     a1: "(R1 ===> R2) f g"

   341   and     a2: "R1 x y"

   342   shows "R2 (Let x f) (Let y g)"

   343 using FUN_REL_MP[OF q1 q2 a1] a2

   344 by auto

   345 

   346 

   347 (* ask peter what are literal_case *)

   348 (* literal_case_PRS *)

   349 (* literal_case_RSP *)

   350 

   351 

   352 (* FUNCTION APPLICATION *)

   353 

   354 lemma APPLY_PRS:

   355   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   356   and     q2: "QUOTIENT R2 Abs2 Rep2"

   357   shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"

   358 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto

   359 

   360 (* ask peter: no use of q1 q2 *)

   361 lemma APPLY_RSP:

   362   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   363   and     q2: "QUOTIENT R2 Abs2 Rep2"

   364   and     a: "(R1 ===> R2) f g" "R1 x y"

   365   shows "R2 (f x) (g y)"

   366 using a by (rule FUN_REL_IMP)

   367 

   368 

   369 (* combinators: I, K, o, C, W *)

   370 

   371 lemma I_PRS:

   372   assumes q: "QUOTIENT R Abs Rep"

   373   shows "(\<lambda>x. x) e = Abs ((\<lambda> x. x) (Rep e))"

   374 using QUOTIENT_ABS_REP[OF q] by auto

   375 

   376 lemma I_RSP:

   377   assumes q: "QUOTIENT R Abs Rep"

   378   and     a: "R e1 e2"

   379   shows "R ((\<lambda>x. x) e1) ((\<lambda> x. x) e2)"

   380 using a by auto

   381 

   382 lemma o_PRS:

   383   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   384   and     q2: "QUOTIENT R2 Abs2 Rep2"

   385   and     q3: "QUOTIENT R3 Abs3 Rep3"

   386   shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"

   387 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3]

   388 unfolding o_def expand_fun_eq

   389 by simp

   390 

   391 lemma o_RSP:

   392   assumes q1: "QUOTIENT R1 Abs1 Rep1"

   393   and     q2: "QUOTIENT R2 Abs2 Rep2"

   394   and     q3: "QUOTIENT R3 Abs3 Rep3"

   395   and     a1: "(R2 ===> R3) f1 f2"

   396   and     a2: "(R1 ===> R2) g1 g2"

   397   shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"

   398 using a1 a2 unfolding o_def expand_fun_eq

   399 by (auto)

   400 

   401 end