Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/Isabelle/ZF/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: p_groups.prf   Sprache: Isabelle

Original von: Isabelle©
(*  Title:      ZF/OrdQuant.thy
    Authors:    Krzysztof Grabczewski and L C Paulson
*)

section \<open>Special quantifiers\<close>

theory OrdQuant imports Ordinal begin

subsection \<open>Quantifiers and union operator for ordinals\<close>

definition
  (* Ordinal Quantifiers *)
  oall :: "[i, i => o] => o"  where
    "oall(A, P) == \x. x P(x)"

definition
  oex :: "[i, i => o] => o"  where
    "oex(A, P) == \x. x

definition
  (* Ordinal Union *)
  OUnion :: "[i, i => i] => i"  where
    "OUnion(i,B) == {z: \x\i. B(x). Ord(i)}"

syntax
  "_oall"     :: "[idt, i, o] => o"        (\<open>(3\<forall>_<_./ _)\<close> 10)
  "_oex"      :: "[idt, i, o] => o"        (\<open>(3\<exists>_<_./ _)\<close> 10)
  "_OUNION"   :: "[idt, i, i] => i"        (\<open>(3\<Union>_<_./ _)\<close> 10)
translations
  "\x "CONST oall(a, \x. P)"
  "\x "CONST oex(a, \x. P)"
  "\x "CONST OUnion(a, \x. B)"


subsubsection \<open>simplification of the new quantifiers\<close>


(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
  is proved.  Ord_atomize would convert this rule to
    x < 0 ==> P(x) == True, which causes dire effects!*)
lemma [simp]: "(\x<0. P(x))"
by (simp add: oall_def)

lemma [simp]: "~(\x<0. P(x))"
by (simp add: oex_def)

lemma [simp]: "(\x (Ord(i) \ P(i) & (\x
apply (simp add: oall_def le_iff)
apply (blast intro: lt_Ord2)
done

lemma [simp]: "(\x (Ord(i) & (P(i) | (\x
apply (simp add: oex_def le_iff)
apply (blast intro: lt_Ord2)
done

subsubsection \<open>Union over ordinals\<close>

lemma Ord_OUN [intro,simp]:
     "[| !!x. x Ord(B(x)) |] ==> Ord(\x
by (simp add: OUnion_def ltI Ord_UN)

lemma OUN_upper_lt:
     "[| ax i < (\x
by (unfold OUnion_def lt_def, blast )

lemma OUN_upper_le:
     "[| ab(a); Ord(\x i \ (\x
apply (unfold OUnion_def, auto)
apply (rule UN_upper_le )
apply (auto simp add: lt_def)
done

lemma Limit_OUN_eq: "Limit(i) ==> (\x
by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)

(* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
lemma OUN_least:
     "(!!x. x B(x) \ C) ==> (\x C"
by (simp add: OUnion_def UN_least ltI)

lemma OUN_least_le:
     "[| Ord(i); !!x. x b(x) \ i |] ==> (\x i"
by (simp add: OUnion_def UN_least_le ltI Ord_0_le)

lemma le_implies_OUN_le_OUN:
     "[| !!x. x c(x) \ d(x) |] ==> (\x (\x
by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)

lemma OUN_UN_eq:
     "(!!x. x \ A ==> Ord(B(x)))
      ==> (\<Union>z < (\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z < B(x). C(z))"
by (simp add: OUnion_def)

lemma OUN_Union_eq:
     "(!!x. x \ X ==> Ord(x))
      ==> (\<Union>z < \<Union>(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
by (simp add: OUnion_def)

(*So that rule_format will get rid of this quantifier...*)
lemma atomize_oall [symmetric, rulify]:
     "(!!x. x P(x)) == Trueprop (\x
by (simp add: oall_def atomize_all atomize_imp)

subsubsection \<open>universal quantifier for ordinals\<close>

lemma oallI [intro!]:
    "[| !!x. x P(x) |] ==> \x
by (simp add: oall_def)

lemma ospec: "[| \x P(x)"
by (simp add: oall_def)

lemma oallE:
    "[| \x Q; ~x Q |] ==> Q"
by (simp add: oall_def, blast)

lemma rev_oallE [elim]:
    "[| \x Q; P(x) ==> Q |] ==> Q"
by (simp add: oall_def, blast)


(*Trival rewrite rule.  @{term"(\<forall>x<a.P)<->P"} holds only if a is not 0!*)
lemma oall_simp [simp]: "(\x True"
by blast

(*Congruence rule for rewriting*)
lemma oall_cong [cong]:
    "[| a=a'; !!x. x P(x) <-> P'(x) |]
     ==> oall(a, %x. P(x)) <-> oall(a', %x. P'(x))"
by (simp add: oall_def)


subsubsection \<open>existential quantifier for ordinals\<close>

lemma oexI [intro]:
    "[| P(x); x \x
apply (simp add: oex_def, blast)
done

(*Not of the general form for such rules... *)
lemma oexCI:
   "[| \x P(a); a \x
apply (simp add: oex_def, blast)
done

lemma oexE [elim!]:
    "[| \x Q |] ==> Q"
apply (simp add: oex_def, blast)
done

lemma oex_cong [cong]:
    "[| a=a'; !!x. x P(x) <-> P'(x) |]
     ==> oex(a, %x. P(x)) <-> oex(a', %x. P'(x))"
apply (simp add: oex_def cong add: conj_cong)
done


subsubsection \<open>Rules for Ordinal-Indexed Unions\<close>

lemma OUN_I [intro]: "[| a B(a) |] ==> b: (\z
by (unfold OUnion_def lt_def, blast)

lemma OUN_E [elim!]:
    "[| b \ (\z B(a); a R |] ==> R"
apply (unfold OUnion_def lt_def, blast)
done

lemma OUN_iff: "b \ (\x (\x B(x))"
by (unfold OUnion_def oex_def lt_def, blast)

lemma OUN_cong [cong]:
    "[| i=j; !!x. x C(x)=D(x) |] ==> (\xx
by (simp add: OUnion_def lt_def OUN_iff)

lemma lt_induct:
    "[| iy P(x) |] ==> P(i)"
apply (simp add: lt_def oall_def)
apply (erule conjE)
apply (erule Ord_induct, assumption, blast)
done


subsection \<open>Quantification over a class\<close>

definition
  "rall"     :: "[i=>o, i=>o] => o"  where
    "rall(M, P) == \x. M(x) \ P(x)"

definition
  "rex"      :: "[i=>o, i=>o] => o"  where
    "rex(M, P) == \x. M(x) & P(x)"

syntax
  "_rall"     :: "[pttrn, i=>o, o] => o"        (\<open>(3\<forall>_[_]./ _)\<close> 10)
  "_rex"      :: "[pttrn, i=>o, o] => o"        (\<open>(3\<exists>_[_]./ _)\<close> 10)
translations
  "\x[M]. P" \ "CONST rall(M, \x. P)"
  "\x[M]. P" \ "CONST rex(M, \x. P)"


subsubsection\<open>Relativized universal quantifier\<close>

lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> \x[M]. P(x)"
by (simp add: rall_def)

lemma rspec: "[| \x[M]. P(x); M(x) |] ==> P(x)"
by (simp add: rall_def)

(*Instantiates x first: better for automatic theorem proving?*)
lemma rev_rallE [elim]:
    "[| \x[M]. P(x); ~ M(x) ==> Q; P(x) ==> Q |] ==> Q"
by (simp add: rall_def, blast)

lemma rallE: "[| \x[M]. P(x); P(x) ==> Q; ~ M(x) ==> Q |] ==> Q"
by blast

(*Trival rewrite rule;   (\<forall>x[M].P)<->P holds only if A is nonempty!*)
lemma rall_triv [simp]: "(\x[M]. P) \ ((\x. M(x)) \ P)"
by (simp add: rall_def)

(*Congruence rule for rewriting*)
lemma rall_cong [cong]:
    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (\x[M]. P(x)) <-> (\x[M]. P'(x))"
by (simp add: rall_def)


subsubsection\<open>Relativized existential quantifier\<close>

lemma rexI [intro]: "[| P(x); M(x) |] ==> \x[M]. P(x)"
by (simp add: rex_def, blast)

(*The best argument order when there is only one M(x)*)
lemma rev_rexI: "[| M(x); P(x) |] ==> \x[M]. P(x)"
by blast

(*Not of the general form for such rules... *)
lemma rexCI: "[| \x[M]. ~P(x) ==> P(a); M(a) |] ==> \x[M]. P(x)"
by blast

lemma rexE [elim!]: "[| \x[M]. P(x); !!x. [| M(x); P(x) |] ==> Q |] ==> Q"
by (simp add: rex_def, blast)

(*We do not even have (\<exists>x[M]. True) <-> True unless A is nonempty!!*)
lemma rex_triv [simp]: "(\x[M]. P) \ ((\x. M(x)) \ P)"
by (simp add: rex_def)

lemma rex_cong [cong]:
    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (\x[M]. P(x)) <-> (\x[M]. P'(x))"
by (simp add: rex_def cong: conj_cong)

lemma rall_is_ball [simp]: "(\x[%z. z\A]. P(x)) <-> (\x\A. P(x))"
by blast

lemma rex_is_bex [simp]: "(\x[%z. z\A]. P(x)) <-> (\x\A. P(x))"
by blast

lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\x[M]. P(x))"
by (simp add: rall_def atomize_all atomize_imp)

declare atomize_rall [symmetric, rulify]

lemma rall_simps1:
     "(\x[M]. P(x) & Q) <-> (\x[M]. P(x)) & ((\x[M]. False) | Q)"
     "(\x[M]. P(x) | Q) <-> ((\x[M]. P(x)) | Q)"
     "(\x[M]. P(x) \ Q) <-> ((\x[M]. P(x)) \ Q)"
     "(~(\x[M]. P(x))) <-> (\x[M]. ~P(x))"
by blast+

lemma rall_simps2:
     "(\x[M]. P & Q(x)) <-> ((\x[M]. False) | P) & (\x[M]. Q(x))"
     "(\x[M]. P | Q(x)) <-> (P | (\x[M]. Q(x)))"
     "(\x[M]. P \ Q(x)) <-> (P \ (\x[M]. Q(x)))"
by blast+

lemmas rall_simps [simp] = rall_simps1 rall_simps2

lemma rall_conj_distrib:
    "(\x[M]. P(x) & Q(x)) <-> ((\x[M]. P(x)) & (\x[M]. Q(x)))"
by blast

lemma rex_simps1:
     "(\x[M]. P(x) & Q) <-> ((\x[M]. P(x)) & Q)"
     "(\x[M]. P(x) | Q) <-> (\x[M]. P(x)) | ((\x[M]. True) & Q)"
     "(\x[M]. P(x) \ Q) <-> ((\x[M]. P(x)) \ ((\x[M]. True) & Q))"
     "(~(\x[M]. P(x))) <-> (\x[M]. ~P(x))"
by blast+

lemma rex_simps2:
     "(\x[M]. P & Q(x)) <-> (P & (\x[M]. Q(x)))"
     "(\x[M]. P | Q(x)) <-> ((\x[M]. True) & P) | (\x[M]. Q(x))"
     "(\x[M]. P \ Q(x)) <-> (((\x[M]. False) | P) \ (\x[M]. Q(x)))"
by blast+

lemmas rex_simps [simp] = rex_simps1 rex_simps2

lemma rex_disj_distrib:
    "(\x[M]. P(x) | Q(x)) <-> ((\x[M]. P(x)) | (\x[M]. Q(x)))"
by blast


subsubsection\<open>One-point rule for bounded quantifiers\<close>

lemma rex_triv_one_point1 [simp]: "(\x[M]. x=a) <-> ( M(a))"
by blast

lemma rex_triv_one_point2 [simp]: "(\x[M]. a=x) <-> ( M(a))"
by blast

lemma rex_one_point1 [simp]: "(\x[M]. x=a & P(x)) <-> ( M(a) & P(a))"
by blast

lemma rex_one_point2 [simp]: "(\x[M]. a=x & P(x)) <-> ( M(a) & P(a))"
by blast

lemma rall_one_point1 [simp]: "(\x[M]. x=a \ P(x)) <-> ( M(a) \ P(a))"
by blast

lemma rall_one_point2 [simp]: "(\x[M]. a=x \ P(x)) <-> ( M(a) \ P(a))"
by blast


subsubsection\<open>Sets as Classes\<close>

definition
  setclass :: "[i,i] => o"       (\<open>##_\<close> [40] 40)  where
   "setclass(A) == %x. x \ A"

lemma setclass_iff [simp]: "setclass(A,x) <-> x \ A"
by (simp add: setclass_def)

lemma rall_setclass_is_ball [simp]: "(\x[##A]. P(x)) <-> (\x\A. P(x))"
by auto

lemma rex_setclass_is_bex [simp]: "(\x[##A]. P(x)) <-> (\x\A. P(x))"
by auto


ML
\<open>
val Ord_atomize =
  atomize ([(\<^const_name>\<open>oall\<close>, @{thms ospec}), (\<^const_name>\<open>rall\<close>, @{thms rspec})] @
    ZF_conn_pairs, ZF_mem_pairs);
\<close>
declaration \<open>fn _ =>
  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
\<close>

text \<open>Setting up the one-point-rule simproc\<close>

simproc_setup defined_rex ("\x[M]. P(x) & Q(x)") = \
  fn _ => Quantifier1.rearrange_Bex
    (fn ctxt => unfold_tac ctxt @{thms rex_def})
\<close>

simproc_setup defined_rall ("\x[M]. P(x) \ Q(x)") = \
  fn _ => Quantifier1.rearrange_Ball
    (fn ctxt => unfold_tac ctxt @{thms rall_def})
\<close>

end

¤ Dauer der Verarbeitung: 0.27 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff

                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik