1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/FOL/ex/LocaleInst.thy Fri Apr 02 14:08:30 2004 +0200
1.3 @@ -0,0 +1,114 @@
1.4 +(* Title: FOL/ex/LocaleInst.thy
1.5 + ID: $Id$
1.6 + Author: Clemens Ballarin
1.7 + Copyright (c) 2004 by Clemens Ballarin
1.8 +
1.9 +Test of locale instantiation mechanism, also provides a few examples.
1.10 +*)
1.11 +
1.12 +header {* Test of Locale instantiation *}
1.13 +
1.14 +theory LocaleInst = FOL:
1.15 +
1.16 +ML {* set show_hyps *}
1.17 +
1.18 +section {* Locale without assumptions *}
1.19 +
1.20 +locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
1.21 +
1.22 +lemma "[| A; B |] ==> A & B"
1.23 +proof -
1.24 + instantiate my: L1 txt {* No chained fact required. *}
1.25 + assume B and A txt {* order reversed *}
1.26 + then show "A & B" ..
1.27 + txt {* Applies @{thm my.rev_conjI}. *}
1.28 +qed
1.29 +
1.30 +section {* Simple locale with assumptions *}
1.31 +
1.32 +typedecl i
1.33 +arities i :: "term"
1.34 +
1.35 +consts bin :: "[i, i] => i" (infixl "#" 60)
1.36 +
1.37 +axioms i_assoc: "(x # y) # z = x # (y # z)"
1.38 + i_comm: "x # y = y # x"
1.39 +
1.40 +locale L2 =
1.41 + fixes OP (infixl "+" 60)
1.42 + assumes assoc: "(x + y) + z = x + (y + z)"
1.43 + and comm: "x + y = y + x"
1.44 +
1.45 +lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
1.46 +proof -
1.47 + have "x + (y + z) = (x + y) + z" by (simp add: assoc)
1.48 + also have "... = (y + x) + z" by (simp add: comm)
1.49 + also have "... = y + (x + z)" by (simp add: assoc)
1.50 + finally show ?thesis .
1.51 +qed
1.52 +
1.53 +lemmas (in L2) AC = comm assoc lcomm
1.54 +
1.55 +lemma "(x::i) # y # z # w = y # x # w # z"
1.56 +proof -
1.57 + have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
1.58 + then instantiate my: L2
1.59 + txt {* Chained fact required to discharge assumptions of @{text L2}
1.60 + and instantiate parameters. *}
1.61 + show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
1.62 +qed
1.63 +
1.64 +section {* Nested locale with assumptions *}
1.65 +
1.66 +locale L3 =
1.67 + fixes OP (infixl "+" 60)
1.68 + assumes assoc: "(x + y) + z = x + (y + z)"
1.69 +
1.70 +locale L4 = L3 +
1.71 + assumes comm: "x + y = y + x"
1.72 +
1.73 +lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
1.74 +proof -
1.75 + have "x + (y + z) = (x + y) + z" by (simp add: assoc)
1.76 + also have "... = (y + x) + z" by (simp add: comm)
1.77 + also have "... = y + (x + z)" by (simp add: assoc)
1.78 + finally show ?thesis .
1.79 +qed
1.80 +
1.81 +lemmas (in L4) AC = comm assoc lcomm
1.82 +
1.83 +text {* Conceptually difficult locale:
1.84 + 2nd context fragment contains facts with differing metahyps. *}
1.85 +
1.86 +lemma L4_intro:
1.87 + fixes OP (infixl "+" 60)
1.88 + assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
1.89 + and comm: "!!x y. x + y = y + x"
1.90 + shows "L4 (op+)"
1.91 + by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
1.92 +
1.93 +lemma "(x::i) # y # z # w = y # x # w # z"
1.94 +proof -
1.95 + have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
1.96 + then instantiate my: L4
1.97 + show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
1.98 +qed
1.99 +
1.100 +section {* Locale with definition *}
1.101 +
1.102 +text {* This example is admittedly not very creative :-) *}
1.103 +
1.104 +locale L5 = L4 + var A +
1.105 + defines A_def: "A == True"
1.106 +
1.107 +lemma (in L5) lem: A
1.108 + by (unfold A_def) rule
1.109 +
1.110 +lemma "L5(op #) ==> True"
1.111 +proof -
1.112 + assume "L5(op #)"
1.113 + then instantiate my: L5
1.114 + show ?thesis by (rule lem) (* lem instantiated to True *)
1.115 +qed
1.116 +
1.117 +end