src/FOL/ex/NewLocaleTest.thy
author ballarin
Fri Dec 05 16:41:36 2008 +0100 (2008-12-05)
changeset 29018 17538bdef546
parent 28993 829e684b02ef
child 29019 8e7d6f959bd7
permissions -rw-r--r--
Interpretation in proof contexts.
     1 (*  Title:      FOL/ex/NewLocaleTest.thy
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Testing environment for locale expressions --- experimental.
     5 *)
     6 
     7 theory NewLocaleTest
     8 imports NewLocaleSetup
     9 begin
    10 
    11 ML_val {* set new_locales *}
    12 ML_val {* set Toplevel.debug *}
    13 ML_val {* set show_hyps *}
    14 
    15 
    16 typedecl int arities int :: "term"
    17 consts plus :: "int => int => int" (infixl "+" 60)
    18   zero :: int ("0")
    19   minus :: "int => int" ("- _")
    20 
    21 axioms
    22   int_assoc: "(x + y::int) + z = x + (y + z)"
    23   int_zero: "0 + x = x"
    24   int_minus: "(-x) + x = 0"
    25   int_minus2: "-(-x) = x"
    26 
    27 text {* Inference of parameter types *}
    28 
    29 locale param1 = fixes p
    30 print_locale! param1
    31 
    32 locale param2 = fixes p :: 'b
    33 print_locale! param2
    34 
    35 (*
    36 locale param_top = param2 r for r :: "'b :: {}"
    37   Fails, cannot generalise parameter.
    38 *)
    39 
    40 locale param3 = fixes p (infix ".." 50)
    41 print_locale! param3
    42 
    43 locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
    44 print_locale! param4
    45 
    46 
    47 text {* Incremental type constraints *}
    48 
    49 locale constraint1 =
    50   fixes  prod (infixl "**" 65)
    51   assumes l_id: "x ** y = x"
    52   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
    53 print_locale! constraint1
    54 
    55 locale constraint2 =
    56   fixes p and q
    57   assumes "p = q"
    58 print_locale! constraint2
    59 
    60 
    61 text {* Inheritance *}
    62 
    63 locale semi =
    64   fixes prod (infixl "**" 65)
    65   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
    66 print_locale! semi thm semi_def
    67 
    68 locale lgrp = semi +
    69   fixes one and inv
    70   assumes lone: "one ** x = x"
    71     and linv: "inv(x) ** x = one"
    72 print_locale! lgrp thm lgrp_def lgrp_axioms_def
    73 
    74 locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
    75   fixes zero and neg
    76   assumes lzero: "zero ++ x = x"
    77     and lneg: "neg(x) ++ x = zero"
    78 print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
    79 
    80 locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
    81 print_locale! rev_lgrp thm rev_lgrp_def
    82 
    83 locale hom = f: semi f + g: semi g for f and g
    84 print_locale! hom thm hom_def
    85 
    86 locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
    87 print_locale! perturbation thm perturbation_def
    88 
    89 locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
    90 print_locale! pert_hom thm pert_hom_def
    91 
    92 text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
    93 locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
    94 print_locale! pert_hom' thm pert_hom'_def
    95 
    96 
    97 text {* Syntax declarations *}
    98 
    99 locale logic =
   100   fixes land (infixl "&&" 55)
   101     and lnot ("-- _" [60] 60)
   102   assumes assoc: "(x && y) && z = x && (y && z)"
   103     and notnot: "-- (-- x) = x"
   104 begin
   105 
   106 definition lor (infixl "||" 50) where
   107   "x || y = --(-- x && -- y)"
   108 
   109 end
   110 print_locale! logic
   111 
   112 locale use_decl = logic + semi "op ||"
   113 print_locale! use_decl thm use_decl_def
   114 
   115 
   116 text {* Theorem statements *}
   117 
   118 lemma (in lgrp) lcancel:
   119   "x ** y = x ** z <-> y = z"
   120 proof
   121   assume "x ** y = x ** z"
   122   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   123   then show "y = z" by (simp add: lone linv)
   124 qed simp
   125 print_locale! lgrp
   126 
   127 
   128 locale rgrp = semi +
   129   fixes one and inv
   130   assumes rone: "x ** one = x"
   131     and rinv: "x ** inv(x) = one"
   132 begin
   133 
   134 lemma rcancel:
   135   "y ** x = z ** x <-> y = z"
   136 proof
   137   assume "y ** x = z ** x"
   138   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   139     by (simp add: assoc [symmetric])
   140   then show "y = z" by (simp add: rone rinv)
   141 qed simp
   142 
   143 end
   144 print_locale! rgrp
   145 
   146 
   147 text {* Patterns *}
   148 
   149 lemma (in rgrp)
   150   assumes "y ** x = z ** x" (is ?a)
   151   shows "y = z" (is ?t)
   152 proof -
   153   txt {* Weird proof involving patterns from context element and conclusion. *}
   154   {
   155     assume ?a
   156     then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   157       by (simp add: assoc [symmetric])
   158     then have ?t by (simp add: rone rinv)
   159   }
   160   note x = this
   161   show ?t by (rule x [OF `?a`])
   162 qed
   163 
   164 
   165 text {* Interpretation between locales: sublocales *}
   166 
   167 sublocale lgrp < right: rgrp
   168 print_facts
   169 proof unfold_locales
   170   {
   171     fix x
   172     have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   173     then show "x ** one = x" by (simp add: assoc lcancel)
   174   }
   175   note rone = this
   176   {
   177     fix x
   178     have "inv(x) ** x ** inv(x) = inv(x) ** one"
   179       by (simp add: linv lone rone)
   180     then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   181   }
   182 qed
   183 
   184 (* effect on printed locale *)
   185 
   186 print_locale! lgrp
   187 
   188 (* use of derived theorem *)
   189 
   190 lemma (in lgrp)
   191   "y ** x = z ** x <-> y = z"
   192   apply (rule rcancel)
   193   done
   194 
   195 (* circular interpretation *)
   196 
   197 sublocale rgrp < left: lgrp
   198 proof unfold_locales
   199   {
   200     fix x
   201     have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
   202     then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
   203   }
   204   note lone = this
   205   {
   206     fix x
   207     have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
   208       by (simp add: rinv lone rone)
   209     then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
   210   }
   211 qed
   212 
   213 (* effect on printed locale *)
   214 
   215 print_locale! rgrp
   216 print_locale! lgrp
   217 
   218 
   219 (* Duality *)
   220 
   221 locale order =
   222   fixes less :: "'a => 'a => o" (infix "<<" 50)
   223   assumes refl: "x << x"
   224     and trans: "[| x << y; y << z |] ==> x << z"
   225 
   226 sublocale order < dual: order "%x y. y << x"
   227   apply unfold_locales apply (rule refl) apply (blast intro: trans)
   228   done
   229 
   230 print_locale! order  (* Only two instances of order. *)
   231 
   232 locale order' =
   233   fixes less :: "'a => 'a => o" (infix "<<" 50)
   234   assumes refl: "x << x"
   235     and trans: "[| x << y; y << z |] ==> x << z"
   236 
   237 locale order_with_def = order'
   238 begin
   239 
   240 definition greater :: "'a => 'a => o" (infix ">>" 50) where
   241   "x >> y <-> y << x"
   242 
   243 end
   244 
   245 sublocale order_with_def < dual: order' "op >>"
   246   apply unfold_locales
   247   unfolding greater_def
   248   apply (rule refl) apply (blast intro: trans)
   249   done
   250 
   251 print_locale! order_with_def
   252 (* Note that decls come after theorems that make use of them.
   253   Appears to be harmless at least in this example. *)
   254 
   255 
   256 (* locale with many parameters ---
   257    interpretations generate alternating group A5 *)
   258 
   259 
   260 locale A5 =
   261   fixes A and B and C and D and E
   262   assumes eq: "A <-> B <-> C <-> D <-> E"
   263 
   264 sublocale A5 < 1: A5 _ _ D E C
   265 print_facts
   266   using eq apply (blast intro: A5.intro) done
   267 
   268 sublocale A5 < 2: A5 C _ E _ A
   269 print_facts
   270   using eq apply (blast intro: A5.intro) done
   271 
   272 sublocale A5 < 3: A5 B C A _ _
   273 print_facts
   274   using eq apply (blast intro: A5.intro) done
   275 
   276 (* Any even permutation of parameters is subsumed by the above. *)
   277 
   278 print_locale! A5
   279 
   280 
   281 (* Free arguments of instance *)
   282 
   283 locale trivial =
   284   fixes P and Q :: o
   285   assumes Q: "P <-> P <-> Q"
   286 begin
   287 
   288 lemma Q_triv: "Q" using Q by fast
   289 
   290 end
   291 
   292 sublocale trivial < x: trivial x _
   293   apply unfold_locales using Q by fast
   294 
   295 print_locale! trivial
   296 
   297 context trivial begin thm x.Q [where ?x = True] end
   298 
   299 sublocale trivial < y: trivial Q Q
   300   by unfold_locales
   301   (* Succeeds since previous interpretation is more general. *)
   302 
   303 print_locale! trivial  (* No instance for y created (subsumed). *)
   304 
   305 
   306 text {* Sublocale, then interpretation in theory *}
   307 
   308 interpretation int: lgrp "op +" "0" "minus"
   309 proof unfold_locales
   310 qed (rule int_assoc int_zero int_minus)+
   311 
   312 thm int.assoc int.semi_axioms
   313 
   314 interpretation int2: semi "op +"
   315   by unfold_locales  (* subsumed, thm int2.assoc not generated *)
   316 
   317 thm int.lone int.right.rone
   318   (* the latter comes through the sublocale relation *)
   319 
   320 
   321 text {* Interpretation in theory, then sublocale *}
   322 
   323 interpretation (* fol: *) logic "op +" "minus"
   324 (* FIXME declaration of qualified names *)
   325   by unfold_locales (rule int_assoc int_minus2)+
   326 
   327 locale logic2 =
   328   fixes land (infixl "&&" 55)
   329     and lnot ("-- _" [60] 60)
   330   assumes assoc: "(x && y) && z = x && (y && z)"
   331     and notnot: "-- (-- x) = x"
   332 begin
   333 (* FIXME
   334 definition lor (infixl "||" 50) where
   335   "x || y = --(-- x && -- y)"
   336 *)
   337 end
   338 
   339 sublocale logic < two: logic2
   340   by unfold_locales (rule assoc notnot)+
   341 
   342 thm two.assoc
   343 
   344 
   345 text {* Interpretation in proofs *}
   346 
   347 lemma True
   348 proof
   349   interpret "local": lgrp "op +" "0" "minus"
   350     by unfold_locales  (* subsumed *)
   351   {
   352     fix zero :: int
   353     assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
   354     then interpret local_fixed: lgrp "op +" zero "minus"
   355       by unfold_locales
   356     thm local_fixed.lone
   357   }
   358   assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
   359   then interpret local_free: lgrp "op +" zero "minus" for zero
   360     by unfold_locales
   361   thm local_free.lone [where ?zero = 0]
   362 qed
   363 
   364 end