products/sources/formale Sprachen/PVS/ints/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: dAst.ml   Sprache: Isabelle

Original von: Isabelle©
(*  Title:      ZF/upair.thy
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    Copyright   1993  University of Cambridge

Observe the order of dependence:
    Upair is defined in terms of Replace
    \<union> is defined in terms of Upair and \<Union>(similarly for Int)
    cons is defined in terms of Upair and Un
    Ordered pairs and descriptions are defined using cons ("set notation")
*)

section\<open>Unordered Pairs\<close>

theory upair
imports ZF_Base
keywords "print_tcset" :: diag
begin

ML_file \<open>Tools/typechk.ML\<close>

lemma atomize_ball [symmetric, rulify]:
     "(!!x. x \ A ==> P(x)) == Trueprop (\x\A. P(x))"
by (simp add: Ball_def atomize_all atomize_imp)


subsection\<open>Unordered Pairs: constant \<^term>\<open>Upair\<close>\<close>

lemma Upair_iff [simp]: "c \ Upair(a,b) \ (c=a | c=b)"
by (unfold Upair_def, blast)

lemma UpairI1: "a \ Upair(a,b)"
by simp

lemma UpairI2: "b \ Upair(a,b)"
by simp

lemma UpairE: "[| a \ Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"
by (simp, blast)

subsection\<open>Rules for Binary Union, Defined via \<^term>\<open>Upair\<close>\<close>

lemma Un_iff [simp]: "c \ A \ B \ (c \ A | c \ B)"
apply (simp add: Un_def)
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done

lemma UnI1: "c \ A ==> c \ A \ B"
by simp

lemma UnI2: "c \ B ==> c \ A \ B"
by simp

declare UnI1 [elim?]  UnI2 [elim?]

lemma UnE [elim!]: "[| c \ A \ B; c \ A ==> P; c \ B ==> P |] ==> P"
by (simp, blast)

(*Stronger version of the rule above*)
lemma UnE': "[| c \ A \ B; c \ A ==> P; [| c \ B; c\A |] ==> P |] ==> P"
by (simp, blast)

(*Classical introduction rule: no commitment to A vs B*)
lemma UnCI [intro!]: "(c \ B ==> c \ A) ==> c \ A \ B"
by (simp, blast)

subsection\<open>Rules for Binary Intersection, Defined via \<^term>\<open>Upair\<close>\<close>

lemma Int_iff [simp]: "c \ A \ B \ (c \ A & c \ B)"
apply (unfold Int_def)
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done

lemma IntI [intro!]: "[| c \ A; c \ B |] ==> c \ A \ B"
by simp

lemma IntD1: "c \ A \ B ==> c \ A"
by simp

lemma IntD2: "c \ A \ B ==> c \ B"
by simp

lemma IntE [elim!]: "[| c \ A \ B; [| c \ A; c \ B |] ==> P |] ==> P"
by simp


subsection\<open>Rules for Set Difference, Defined via \<^term>\<open>Upair\<close>\<close>

lemma Diff_iff [simp]: "c \ A-B \ (c \ A & c\B)"
by (unfold Diff_def, blast)

lemma DiffI [intro!]: "[| c \ A; c \ B |] ==> c \ A - B"
by simp

lemma DiffD1: "c \ A - B ==> c \ A"
by simp

lemma DiffD2: "c \ A - B ==> c \ B"
by simp

lemma DiffE [elim!]: "[| c \ A - B; [| c \ A; c\B |] ==> P |] ==> P"
by simp


subsection\<open>Rules for \<^term>\<open>cons\<close>\<close>

lemma cons_iff [simp]: "a \ cons(b,A) \ (a=b | a \ A)"
apply (unfold cons_def)
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done

(*risky as a typechecking rule, but solves otherwise unconstrained goals of
the form x \<in> ?A*)
lemma consI1 [simp,TC]: "a \ cons(a,B)"
by simp


lemma consI2: "a \ B ==> a \ cons(b,B)"
by simp

lemma consE [elim!]: "[| a \ cons(b,A); a=b ==> P; a \ A ==> P |] ==> P"
by (simp, blast)

(*Stronger version of the rule above*)
lemma consE':
    "[| a \ cons(b,A); a=b ==> P; [| a \ A; a\b |] ==> P |] ==> P"
by (simp, blast)

(*Classical introduction rule*)
lemma consCI [intro!]: "(a\B ==> a=b) ==> a \ cons(b,B)"
by (simp, blast)

lemma cons_not_0 [simp]: "cons(a,B) \ 0"
by (blast elim: equalityE)

lemmas cons_neq_0 = cons_not_0 [THEN notE]

declare cons_not_0 [THEN not_sym, simp]


subsection\<open>Singletons\<close>

lemma singleton_iff: "a \ {b} \ a=b"
by simp

lemma singletonI [intro!]: "a \ {a}"
by (rule consI1)

lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!]


subsection\<open>Descriptions\<close>

lemma the_equality [intro]:
    "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
apply (unfold the_def)
apply (fast dest: subst)
done

(* Only use this if you already know \<exists>!x. P(x) *)
lemma the_equality2: "[| \!x. P(x); P(a) |] ==> (THE x. P(x)) = a"
by blast

lemma theI: "\!x. P(x) ==> P(THE x. P(x))"
apply (erule ex1E)
apply (subst the_equality)
apply (blast+)
done

(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then
  @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)

(*If it's "undefined", it's zero!*)
lemma the_0: "~ (\!x. P(x)) ==> (THE x. P(x))=0"
apply (unfold the_def)
apply (blast elim!: ReplaceE)
done

(*Easier to apply than theI: conclusion has only one occurrence of P*)
lemma theI2:
    assumes p1: "~ Q(0) ==> \!x. P(x)"
        and p2: "!!x. P(x) ==> Q(x)"
    shows "Q(THE x. P(x))"
apply (rule classical)
apply (rule p2)
apply (rule theI)
apply (rule classical)
apply (rule p1)
apply (erule the_0 [THEN subst], assumption)
done

lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
by blast

lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
by blast


subsection\<open>Conditional Terms: \<open>if-then-else\<close>\<close>

lemma if_true [simp]: "(if True then a else b) = a"
by (unfold if_def, blast)

lemma if_false [simp]: "(if False then a else b) = b"
by (unfold if_def, blast)

(*Never use with case splitting, or if P is known to be true or false*)
lemma if_cong:
    "[| P\Q; Q ==> a=c; ~Q ==> b=d |]
     ==> (if P then a else b) = (if Q then c else d)"
by (simp add: if_def cong add: conj_cong)

(*Prevents simplification of x and y \<in> faster and allows the execution
  of functional programs. NOW THE DEFAULT.*)
lemma if_weak_cong: "P\Q ==> (if P then x else y) = (if Q then x else y)"
by simp

(*Not needed for rewriting, since P would rewrite to True anyway*)
lemma if_P: "P ==> (if P then a else b) = a"
by (unfold if_def, blast)

(*Not needed for rewriting, since P would rewrite to False anyway*)
lemma if_not_P: "~P ==> (if P then a else b) = b"
by (unfold if_def, blast)

lemma split_if [split]:
     "P(if Q then x else y) \ ((Q \ P(x)) & (~Q \ P(y)))"
by (case_tac Q, simp_all)

(** Rewrite rules for boolean case-splitting: faster than split_if [split]
**)

lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
lemmas split_if_eq2 = split_if [of "%x. a = x"] for a

lemmas split_if_mem1 = split_if [of "%x. x \ b"] for b
lemmas split_if_mem2 = split_if [of "%x. a \ x"] for a

lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2

(*Logically equivalent to split_if_mem2*)
lemma if_iff: "a: (if P then x else y) \ P & a \ x | ~P & a \ y"
by simp

lemma if_type [TC]:
    "[| P ==> a \ A; ~P ==> b \ A |] ==> (if P then a else b): A"
by simp

(** Splitting IFs in the assumptions **)

lemma split_if_asm: "P(if Q then x else y) \ (~((Q & ~P(x)) | (~Q & ~P(y))))"
by simp

lemmas if_splits = split_if split_if_asm


subsection\<open>Consequences of Foundation\<close>

(*was called mem_anti_sym*)
lemma mem_asym: "[| a \ b; ~P ==> b \ a |] ==> P"
apply (rule classical)
apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
apply (blast elim!: equalityE)+
done

(*was called mem_anti_refl*)
lemma mem_irrefl: "a \ a ==> P"
by (blast intro: mem_asym)

(*mem_irrefl should NOT be added to default databases:
      it would be tried on most goals, making proofs slower!*)

lemma mem_not_refl: "a \ a"
apply (rule notI)
apply (erule mem_irrefl)
done

(*Good for proving inequalities by rewriting*)
lemma mem_imp_not_eq: "a \ A ==> a \ A"
by (blast elim!: mem_irrefl)

lemma eq_imp_not_mem: "a=A ==> a \ A"
by (blast intro: elim: mem_irrefl)

subsection\<open>Rules for Successor\<close>

lemma succ_iff: "i \ succ(j) \ i=j | i \ j"
by (unfold succ_def, blast)

lemma succI1 [simp]: "i \ succ(i)"
by (simp add: succ_iff)

lemma succI2: "i \ j ==> i \ succ(j)"
by (simp add: succ_iff)

lemma succE [elim!]:
    "[| i \ succ(j); i=j ==> P; i \ j ==> P |] ==> P"
apply (simp add: succ_iff, blast)
done

(*Classical introduction rule*)
lemma succCI [intro!]: "(i\j ==> i=j) ==> i \ succ(j)"
by (simp add: succ_iff, blast)

lemma succ_not_0 [simp]: "succ(n) \ 0"
by (blast elim!: equalityE)

lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!]

declare succ_not_0 [THEN not_sym, simp]
declare sym [THEN succ_neq_0, elim!]

(* @{term"succ(c) \<subseteq> B ==> c \<in> B"} *)
lemmas succ_subsetD = succI1 [THEN [2] subsetD]

(* @{term"succ(b) \<noteq> b"} *)
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]

lemma succ_inject_iff [simp]: "succ(m) = succ(n) \ m=n"
by (blast elim: mem_asym elim!: equalityE)

lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]


subsection\<open>Miniscoping of the Bounded Universal Quantifier\<close>

lemma ball_simps1:
     "(\x\A. P(x) & Q) \ (\x\A. P(x)) & (A=0 | Q)"
     "(\x\A. P(x) | Q) \ ((\x\A. P(x)) | Q)"
     "(\x\A. P(x) \ Q) \ ((\x\A. P(x)) \ Q)"
     "(~(\x\A. P(x))) \ (\x\A. ~P(x))"
     "(\x\0.P(x)) \ True"
     "(\x\succ(i).P(x)) \ P(i) & (\x\i. P(x))"
     "(\x\cons(a,B).P(x)) \ P(a) & (\x\B. P(x))"
     "(\x\RepFun(A,f). P(x)) \ (\y\A. P(f(y)))"
     "(\x\\(A).P(x)) \ (\y\A. \x\y. P(x))"
by blast+

lemma ball_simps2:
     "(\x\A. P & Q(x)) \ (A=0 | P) & (\x\A. Q(x))"
     "(\x\A. P | Q(x)) \ (P | (\x\A. Q(x)))"
     "(\x\A. P \ Q(x)) \ (P \ (\x\A. Q(x)))"
by blast+

lemma ball_simps3:
     "(\x\Collect(A,Q).P(x)) \ (\x\A. Q(x) \ P(x))"
by blast+

lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3

lemma ball_conj_distrib:
    "(\x\A. P(x) & Q(x)) \ ((\x\A. P(x)) & (\x\A. Q(x)))"
by blast


subsection\<open>Miniscoping of the Bounded Existential Quantifier\<close>

lemma bex_simps1:
     "(\x\A. P(x) & Q) \ ((\x\A. P(x)) & Q)"
     "(\x\A. P(x) | Q) \ (\x\A. P(x)) | (A\0 & Q)"
     "(\x\A. P(x) \ Q) \ ((\x\A. P(x)) \ (A\0 & Q))"
     "(\x\0.P(x)) \ False"
     "(\x\succ(i).P(x)) \ P(i) | (\x\i. P(x))"
     "(\x\cons(a,B).P(x)) \ P(a) | (\x\B. P(x))"
     "(\x\RepFun(A,f). P(x)) \ (\y\A. P(f(y)))"
     "(\x\\(A).P(x)) \ (\y\A. \x\y. P(x))"
     "(~(\x\A. P(x))) \ (\x\A. ~P(x))"
by blast+

lemma bex_simps2:
     "(\x\A. P & Q(x)) \ (P & (\x\A. Q(x)))"
     "(\x\A. P | Q(x)) \ (A\0 & P) | (\x\A. Q(x))"
     "(\x\A. P \ Q(x)) \ ((A=0 | P) \ (\x\A. Q(x)))"
by blast+

lemma bex_simps3:
     "(\x\Collect(A,Q).P(x)) \ (\x\A. Q(x) & P(x))"
by blast

lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3

lemma bex_disj_distrib:
    "(\x\A. P(x) | Q(x)) \ ((\x\A. P(x)) | (\x\A. Q(x)))"
by blast


(** One-point rule for bounded quantifiers: see HOL/Set.ML **)

lemma bex_triv_one_point1 [simp]: "(\x\A. x=a) \ (a \ A)"
by blast

lemma bex_triv_one_point2 [simp]: "(\x\A. a=x) \ (a \ A)"
by blast

lemma bex_one_point1 [simp]: "(\x\A. x=a & P(x)) \ (a \ A & P(a))"
by blast

lemma bex_one_point2 [simp]: "(\x\A. a=x & P(x)) \ (a \ A & P(a))"
by blast

lemma ball_one_point1 [simp]: "(\x\A. x=a \ P(x)) \ (a \ A \ P(a))"
by blast

lemma ball_one_point2 [simp]: "(\x\A. a=x \ P(x)) \ (a \ A \ P(a))"
by blast


subsection\<open>Miniscoping of the Replacement Operator\<close>

text\<open>These cover both \<^term>\<open>Replace\<close> and \<^term>\<open>Collect\<close>\<close>
lemma Rep_simps [simp]:
     "{x. y \ 0, R(x,y)} = 0"
     "{x \ 0. P(x)} = 0"
     "{x \ A. Q} = (if Q then A else 0)"
     "RepFun(0,f) = 0"
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))"
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"
by (simp_all, blast+)


subsection\<open>Miniscoping of Unions\<close>

lemma UN_simps1:
     "(\x\C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \x\C. B(x)))"
     "(\x\C. A(x) \ B') = (if C=0 then 0 else (\x\C. A(x)) \ B')"
     "(\x\C. A' \ B(x)) = (if C=0 then 0 else A' \ (\x\C. B(x)))"
     "(\x\C. A(x) \ B') = ((\x\C. A(x)) \ B')"
     "(\x\C. A' \ B(x)) = (A' \ (\x\C. B(x)))"
     "(\x\C. A(x) - B') = ((\x\C. A(x)) - B')"
     "(\x\C. A' - B(x)) = (if C=0 then 0 else A' - (\x\C. B(x)))"
apply (simp_all add: Inter_def)
apply (blast intro!: equalityI )+
done

lemma UN_simps2:
      "(\x\\(A). B(x)) = (\y\A. \x\y. B(x))"
      "(\z\(\x\A. B(x)). C(z)) = (\x\A. \z\B(x). C(z))"
      "(\x\RepFun(A,f). B(x)) = (\a\A. B(f(a)))"
by blast+

lemmas UN_simps [simp] = UN_simps1 UN_simps2

text\<open>Opposite of miniscoping: pull the operator out\<close>

lemma UN_extend_simps1:
     "(\x\C. A(x)) \ B = (if C=0 then B else (\x\C. A(x) \ B))"
     "((\x\C. A(x)) \ B) = (\x\C. A(x) \ B)"
     "((\x\C. A(x)) - B) = (\x\C. A(x) - B)"
apply simp_all
apply blast+
done

lemma UN_extend_simps2:
     "cons(a, \x\C. B(x)) = (if C=0 then {a} else (\x\C. cons(a, B(x))))"
     "A \ (\x\C. B(x)) = (if C=0 then A else (\x\C. A \ B(x)))"
     "(A \ (\x\C. B(x))) = (\x\C. A \ B(x))"
     "A - (\x\C. B(x)) = (if C=0 then A else (\x\C. A - B(x)))"
     "(\y\A. \x\y. B(x)) = (\x\\(A). B(x))"
     "(\a\A. B(f(a))) = (\x\RepFun(A,f). B(x))"
apply (simp_all add: Inter_def)
apply (blast intro!: equalityI)+
done

lemma UN_UN_extend:
     "(\x\A. \z\B(x). C(z)) = (\z\(\x\A. B(x)). C(z))"
by blast

lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend


subsection\<open>Miniscoping of Intersections\<close>

lemma INT_simps1:
     "(\x\C. A(x) \ B) = (\x\C. A(x)) \ B"
     "(\x\C. A(x) - B) = (\x\C. A(x)) - B"
     "(\x\C. A(x) \ B) = (if C=0 then 0 else (\x\C. A(x)) \ B)"
by (simp_all add: Inter_def, blast+)

lemma INT_simps2:
     "(\x\C. A \ B(x)) = A \ (\x\C. B(x))"
     "(\x\C. A - B(x)) = (if C=0 then 0 else A - (\x\C. B(x)))"
     "(\x\C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \x\C. B(x)))"
     "(\x\C. A \ B(x)) = (if C=0 then 0 else A \ (\x\C. B(x)))"
apply (simp_all add: Inter_def)
apply (blast intro!: equalityI)+
done

lemmas INT_simps [simp] = INT_simps1 INT_simps2

text\<open>Opposite of miniscoping: pull the operator out\<close>


lemma INT_extend_simps1:
     "(\x\C. A(x)) \ B = (\x\C. A(x) \ B)"
     "(\x\C. A(x)) - B = (\x\C. A(x) - B)"
     "(\x\C. A(x)) \ B = (if C=0 then B else (\x\C. A(x) \ B))"
apply (simp_all add: Inter_def, blast+)
done

lemma INT_extend_simps2:
     "A \ (\x\C. B(x)) = (\x\C. A \ B(x))"
     "A - (\x\C. B(x)) = (if C=0 then A else (\x\C. A - B(x)))"
     "cons(a, \x\C. B(x)) = (if C=0 then {a} else (\x\C. cons(a, B(x))))"
     "A \ (\x\C. B(x)) = (if C=0 then A else (\x\C. A \ B(x)))"
apply (simp_all add: Inter_def)
apply (blast intro!: equalityI)+
done

lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2


subsection\<open>Other simprules\<close>


(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)

lemma misc_simps [simp]:
     "0 \ A = A"
     "A \ 0 = A"
     "0 \ A = 0"
     "A \ 0 = 0"
     "0 - A = 0"
     "A - 0 = A"
     "\(0) = 0"
     "\(cons(b,A)) = b \ \(A)"
     "\({b}) = b"
by blast+

end

¤ Dauer der Verarbeitung: 0.24 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff