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