src/FOL/ex/LocaleInst.thy
author ballarin
Tue Apr 13 09:42:40 2004 +0200 (2004-04-13)
changeset 14551 2cb6ff394bfb
parent 14508 859b11514537
child 14957 0e94a1ccc6ae
permissions -rw-r--r--
Various changes to HOL-Algebra;
Locale instantiation.
     1 (*  Title:      FOL/ex/LocaleInst.thy
     2     ID:         $Id$
     3     Author:     Clemens Ballarin
     4     Copyright (c) 2004 by Clemens Ballarin
     5 
     6 Test of locale instantiation mechanism, also provides a few examples.
     7 *)
     8 
     9 header {* Test of Locale instantiation *}
    10 
    11 theory LocaleInst = FOL:
    12 
    13 ML {* set show_hyps *}
    14 
    15 section {* Locale without assumptions *}
    16 
    17 locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
    18 
    19 lemma "[| A; B |] ==> A & B"
    20 proof -
    21   instantiate my: L1           txt {* No chained fact required. *}
    22   assume B and A               txt {* order reversed *}
    23   then show "A & B" ..         txt {* Applies @{thm my.rev_conjI}. *}
    24 qed
    25 
    26 locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
    27 
    28 lemma "[| A; B |] ==> A & B"
    29 proof -
    30   instantiate [intro]: L11     txt {* Attribute supplied at instantiation. *}
    31   assume B and A
    32   then show "A & B" ..
    33 qed
    34 
    35 section {* Simple locale with assumptions *}
    36 
    37 typedecl i
    38 arities  i :: "term"
    39 
    40 consts bin :: "[i, i] => i" (infixl "#" 60)
    41 
    42 axioms i_assoc: "(x # y) # z = x # (y # z)"
    43   i_comm: "x # y = y # x"
    44 
    45 locale L2 =
    46   fixes OP (infixl "+" 60)
    47   assumes assoc: "(x + y) + z = x + (y + z)"
    48     and comm: "x + y = y + x"
    49 
    50 lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
    51 proof -
    52   have "x + (y + z) = (x + y) + z" by (simp add: assoc)
    53   also have "... = (y + x) + z" by (simp add: comm)
    54   also have "... = y + (x + z)" by (simp add: assoc)
    55   finally show ?thesis .
    56 qed
    57 
    58 lemmas (in L2) AC = comm assoc lcomm
    59 
    60 lemma "(x::i) # y # z # w = y # x # w # z"
    61 proof -
    62   have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
    63   then instantiate my: L2
    64     txt {* Chained fact required to discharge assumptions of @{text L2}
    65       and instantiate parameters. *}
    66   show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
    67 qed
    68 
    69 section {* Nested locale with assumptions *}
    70 
    71 locale L3 =
    72   fixes OP (infixl "+" 60)
    73   assumes assoc: "(x + y) + z = x + (y + z)"
    74 
    75 locale L4 = L3 +
    76   assumes comm: "x + y = y + x"
    77 
    78 lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
    79 proof -
    80   have "x + (y + z) = (x + y) + z" by (simp add: assoc)
    81   also have "... = (y + x) + z" by (simp add: comm)
    82   also have "... = y + (x + z)" by (simp add: assoc)
    83   finally show ?thesis .
    84 qed
    85 
    86 lemmas (in L4) AC = comm assoc lcomm
    87 
    88 text {* Conceptually difficult locale:
    89    2nd context fragment contains facts with differing metahyps. *}
    90 
    91 lemma L4_intro:
    92   fixes OP (infixl "+" 60)
    93   assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
    94     and comm: "!!x y. x + y = y + x"
    95   shows "L4 (op+)"
    96     by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
    97 
    98 lemma "(x::i) # y # z # w = y # x # w # z"
    99 proof -
   100   have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
   101   then instantiate my: L4
   102   show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
   103 qed
   104 
   105 section {* Locale with definition *}
   106 
   107 text {* This example is admittedly not very creative :-) *}
   108 
   109 locale L5 = L4 + var A +
   110   defines A_def: "A == True"
   111 
   112 lemma (in L5) lem: A
   113   by (unfold A_def) rule
   114 
   115 lemma "L5(op #) ==> True"
   116 proof -
   117   assume "L5(op #)"
   118   then instantiate my: L5
   119   show ?thesis by (rule lem)  (* lem instantiated to True *)
   120 qed
   121 
   122 section {* Instantiation in a context with target *}
   123 
   124 lemma (in L4)  (* Target might confuse instantiation command. *)
   125   fixes A (infixl "$" 60)
   126   assumes A: "L4(A)"
   127   shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
   128 proof -
   129   from A instantiate A: L4
   130   show ?thesis by (simp only: A.OP.AC)
   131 qed
   132 
   133 end