--- a/src/ZF/ArithSimp.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/ArithSimp.thy Tue May 27 11:39:03 2003 +0200
@@ -12,7 +12,7 @@
subsection{*Difference*}
-lemma diff_self_eq_0: "m #- m = 0"
+lemma diff_self_eq_0 [simp]: "m #- m = 0"
apply (subgoal_tac "natify (m) #- natify (m) = 0")
apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto)
done
--- a/src/ZF/Cardinal.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Cardinal.thy Tue May 27 11:39:03 2003 +0200
@@ -445,7 +445,6 @@
apply (erule well_ord_rvimage, assumption)
done
-
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| le i"
apply (rule le_trans)
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
@@ -455,12 +454,16 @@
lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
-lemma lesspoll_imp_eqpoll:
- "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
+lemma lesspoll_imp_eqpoll: "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
apply (unfold lesspoll_def)
apply (blast intro: lepoll_Ord_imp_eqpoll)
done
+lemma cardinal_subset_Ord: "[|A<=i; Ord(i)|] ==> |A| <= i"
+apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
+apply (auto simp add: lt_def)
+apply (blast intro: Ord_trans)
+done
subsection{*The finite cardinals *}
@@ -1091,6 +1094,7 @@
val lepoll_cardinal_le = thm "lepoll_cardinal_le";
val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
+val cardinal_subset_Ord = thm "cardinal_subset_Ord";
val cons_lepoll_consD = thm "cons_lepoll_consD";
val cons_eqpoll_consD = thm "cons_eqpoll_consD";
val succ_lepoll_succD = thm "succ_lepoll_succD";
--- a/src/ZF/Cardinal_AC.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Cardinal_AC.thy Tue May 27 11:39:03 2003 +0200
@@ -17,7 +17,8 @@
apply (erule well_ord_cardinal_eqpoll)
done
-lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard]
+text{*The theorem @{term "||A|| = |A|"} *}
+lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp]
lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
apply (rule AC_well_ord [THEN exE])
@@ -65,7 +66,7 @@
done
-subsection{*Other Applications of AC*}
+subsection {*The relationship between cardinality and le-pollence*}
lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
apply (rule cardinal_eqpoll
@@ -80,6 +81,27 @@
apply (erule lepoll_imp_Card_le)
done
+lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
+apply auto
+apply (drule cardinal_0 [THEN ssubst])
+apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
+done
+
+lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A"
+apply (cut_tac A = "A" in cardinal_eqpoll)
+apply (auto simp add: eqpoll_iff)
+apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
+apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2
+ simp add: cardinal_idem)
+done
+
+lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
+apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
+done
+
+
+subsection{*Other Applications of AC*}
+
lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
apply (unfold surj_def)
apply (erule CollectE)
@@ -170,5 +192,10 @@
apply (blast intro!: Ord_UN elim: ltE)
done
+ML
+{*
+val cardinal_0_iff_0 = thm "cardinal_0_iff_0";
+val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll";
+*}
+
end
-
--- a/src/ZF/Constructible/README.html Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Constructible/README.html Tue May 27 11:39:03 2003 +0200
@@ -10,7 +10,7 @@
formalization unusually long, and not entirely satisfactory: two parts of the
proof do not fit together. It seems impossible to solve these problems
without formalizing the metatheory. However, the present development follows
-a standard textbook, Kunen's <STRONG>Set Theory</STRONG> and could support the
+a standard textbook, Kunen's <STRONG>Set Theory</STRONG>, and could support the
formalization of further material from that book. It also serves as an
example of what to expect when deep mathematics is formalized.
--- a/src/ZF/Fixedpt.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Fixedpt.thy Tue May 27 11:39:03 2003 +0200
@@ -2,8 +2,6 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
*)
header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
@@ -22,6 +20,8 @@
gfp :: "[i,i=>i]=>i"
"gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
+text{*The theorem is proved in the lattice of subsets of @{term D},
+ namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*}
subsection{*Monotone Operators*}
@@ -69,7 +69,7 @@
apply (erule bnd_monoD2, rule Int_lower2, assumption)
done
-(**** Proof of Knaster-Tarski Theorem for the lfp ****)
+subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
(*lfp is contained in each pre-fixedpoint*)
lemma lfp_lowerbound:
@@ -181,8 +181,15 @@
apply (rule lfp_lowerbound, blast, assumption)
done
+lemma lfp_cong:
+ "[|D=D'; !!X. X <= D' ==> h(X) = h'(X)|] ==> lfp(D,h) = lfp(D',h')"
+apply (simp add: lfp_def)
+apply (rule_tac t=Inter in subst_context)
+apply (rule Collect_cong, simp_all)
+done
-(**** Proof of Knaster-Tarski Theorem for the gfp ****)
+
+subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*}
(*gfp contains each post-fixedpoint that is contained in D*)
lemma gfp_upperbound: "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)"
--- a/src/ZF/Induct/FoldSet.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Induct/FoldSet.ML Tue May 27 11:39:03 2003 +0200
@@ -365,34 +365,35 @@
qed "setsum_addf";
-val major::prems = Goal
+Goal "[| A=A'; B=B'; e=e'; \
+\ (ALL x:A'. ALL y:B'. f(x,y) = f'(x,y)) |] ==> \
+\ fold_set(A,B,f,e) = fold_set(A',B',f',e')";
+by (asm_full_simp_tac (simpset() addsimps [thm"fold_set_def"]) 1);
+by (rtac (thm"lfp_cong") 1);
+by (rtac refl 1);
+by (rtac Collect_cong 1);
+by (rtac refl 1);
+by (rtac disj_cong 1);
+by (rtac iff_refl 1);
+by (REPEAT (rtac ex_cong 1));
+by Auto_tac;
+qed "fold_set_cong";
+
+val prems = Goal
+"[| B=B'; A=A'; e=e'; \
+\ !!x y. [|x:A'; y:B'|] ==> f(x,y) = f'(x,y) |] ==> \
+\ fold[B](f,e,A) = fold[B'](f', e', A')";
+by (asm_full_simp_tac (simpset() addsimps fold_def::prems) 1);
+by (stac fold_set_cong 1);
+by (rtac refl 5);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps prems)));
+qed "fold_cong";
+
+val prems = Goal
"[| A=B; !!x. x:B ==> f(x) = g(x) |] ==> \
\ setsum(f, A) = setsum(g, B)";
-by (case_tac "Finite(B)" 1);
-by (asm_simp_tac (simpset() addsimps [setsum_def, major]) 2);
-by (subgoal_tac "ALL C. C <= B --> (ALL x:C. f(x) = g(x)) \
- \ --> setsum(f,C) = setsum(g, C)" 1);
-by (cut_facts_tac [major] 1);
- by (asm_full_simp_tac (simpset() addsimps [major]@prems) 1);
-by (etac Finite_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (subgoal_tac "C=0" 1);
-by (Force_tac 1);
-by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [major,subset_cons_iff]@prems) 1);
-by Safe_tac;
-by (ftac subset_Finite 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (ftac subset_Finite 1);
-by (assume_tac 1);
-by (subgoal_tac "C = cons(x, C - {x})" 1);
-by (Blast_tac 2);
-by (etac ssubst 1);
-by (dtac spec 1);
-by (mp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Ball_def, major]@prems) 1);
-qed_spec_mp "setsum_cong";
+by (asm_simp_tac (simpset() addsimps setsum_def::prems addcongs [fold_cong]) 1);
+qed "setsum_cong";
Goal "[| Finite(A); Finite(B) |] \
\ ==> setsum(f, A Un B) = \
--- a/src/ZF/Induct/FoldSet.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Induct/FoldSet.thy Tue May 27 11:39:03 2003 +0200
@@ -8,7 +8,7 @@
least left-commutative.
*)
-FoldSet = Main +
+FoldSet = Main +
consts fold_set :: "[i, i, [i,i]=>i, i] => i"
--- a/src/ZF/Induct/Multiset.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Induct/Multiset.ML Tue May 27 11:39:03 2003 +0200
@@ -133,24 +133,11 @@
qed "mset_of_union";
AddIffs [mset_of_union];
-Goalw [multiset_def]
-"multiset(M) ==> \
-\ k:mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k~= a & k:mset_of(M))";
-by (rewrite_goals_tac [normalize_def, mset_of_def, msingle_def,
- mdiff_def, mcount_def]);
-by (auto_tac (claset() addDs [domain_type]
- addIs [zero_less_diff RS iffD1],
- simpset() addsimps
- [multiset_fun_iff, apply_iff]));
-qed "melem_diff_single";
-
Goalw [mdiff_def, multiset_def]
- "[| multiset(M); mset_of(M)<=A |] ==> mset_of(M -# N) <= A";
+ "mset_of(M)<=A ==> mset_of(M -# N) <= A";
by (auto_tac (claset(), simpset() addsimps [normalize_def]));
by (rewtac mset_of_def);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff])));
-by (ALLGOALS(Clarify_tac));
-by (ALLGOALS Asm_full_simp_tac);
by Auto_tac;
qed "mset_of_diff";
Addsimps [mset_of_diff];
@@ -175,13 +162,22 @@
fun_extend3], simpset()));
qed "msingle_multiset";
AddIffs [msingle_multiset];
+AddTCs [msingle_multiset];
(** normalize **)
+bind_thm("Collect_Finite", Collect_subset RS subset_Finite);
+
Goalw [normalize_def, funrestrict_def, mset_of_def]
"normalize(normalize(f)) = normalize(f)";
-by Auto_tac;
+by (case_tac "EX A. f : A -> nat & Finite(A)" 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("x","{x: domain(f) . 0 < f ` x}")] spec 1);
+by (force_tac (claset() addSIs [lam_type], simpset() addsimps [Collect_Finite]) 1);
+by (Asm_simp_tac 1);
qed "normalize_idem";
+
AddIffs [normalize_idem];
Goalw [multiset_def]
@@ -192,17 +188,19 @@
qed "normalize_multiset";
Addsimps [normalize_multiset];
-Goalw [multiset_def]
-"[| f:A -> nat; Finite(A) |] ==> multiset(normalize(f))";
-by (rewrite_goals_tac [normalize_def, mset_of_def]);
+Goal "multiset(normalize(f))";
+by (asm_full_simp_tac (simpset() addsimps [normalize_def]) 1);
+by (rewrite_goals_tac [normalize_def, mset_of_def, multiset_def]);
by Auto_tac;
by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
funrestrict_type], simpset()));
qed "multiset_normalize";
+Addsimps [multiset_normalize];
(** Typechecking rules for union and difference of multisets **)
+(*????????????????move to Arith??*)
Goal "[| n:nat; m:nat |] ==> 0 < m #+ n <-> (0 < m | 0 < n)";
by (induct_tac "n" 1);
by Auto_tac;
@@ -222,13 +220,8 @@
(* difference *)
-Goalw [mdiff_def]
-"multiset(M) ==> multiset(M -# N)";
-by (res_inst_tac [("A", "mset_of(M)")] multiset_normalize 1);
-by (asm_simp_tac (simpset() addsimps [multiset_set_of_Finite]) 2);
-by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def]));
-by (auto_tac (claset() addSIs [lam_type],
- simpset() addsimps [multiset_fun_iff]));
+Goal "multiset(M -# N)";
+by (asm_full_simp_tac (simpset() addsimps [mdiff_def]) 1);
qed "mdiff_multiset";
Addsimps [mdiff_multiset];
@@ -242,22 +235,18 @@
qed "munion_0";
Addsimps [munion_0];
-Goalw [multiset_def]
- "[| multiset(M); multiset(N) |] ==> M +# N = N +# M";
-by (rewrite_goals_tac [munion_def, mset_of_def]);
-by (auto_tac (claset() addSIs [lam_cong], simpset()));
+Goalw [multiset_def] "M +# N = N +# M";
+by (auto_tac (claset() addSIs [lam_cong], simpset() addsimps [munion_def]));
qed "munion_commute";
-Goalw [multiset_def]
-"[|multiset(M); multiset(N); multiset(K)|] ==> (M +# N) +# K = M +# (N +# K)";
+Goalw [multiset_def] "(M +# N) +# K = M +# (N +# K)";
by (rewrite_goals_tac [munion_def, mset_of_def]);
by (rtac lam_cong 1);
by Auto_tac;
qed "munion_assoc";
-Goalw [multiset_def]
-"[|multiset(M); multiset(N); multiset(K)|]==> M +# (N +# K) = N +# (M +# K)";
-by (rewrite_goals_tac [munion_def, mset_of_def]);
+Goalw [multiset_def] "M +# (N +# K) = N +# (M +# K)";
+by (rewrite_goals_tac [munion_def, mset_of_def]);
by (rtac lam_cong 1);
by Auto_tac;
qed "munion_lcommute";
@@ -267,28 +256,38 @@
(* Difference *)
Goalw [mdiff_def] "M -# M = 0";
-by (simp_tac (simpset() addsimps
- [diff_self_eq_0, normalize_def, mset_of_def]) 1);
+by (simp_tac (simpset() addsimps [normalize_def, mset_of_def]) 1);
qed "mdiff_self_eq_0";
-AddIffs [mdiff_self_eq_0];
+Addsimps [mdiff_self_eq_0];
-Goalw [multiset_def] "multiset(M) ==> M -# 0 = M & 0 -# M = 0";
+Goalw [multiset_def] "0 -# M = 0";
by (rewrite_goals_tac [mdiff_def, normalize_def]);
by (auto_tac (claset(), simpset()
addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
qed "mdiff_0";
Addsimps [mdiff_0];
+Goalw [multiset_def] "multiset(M) ==> M -# 0 = M";
+by (rewrite_goals_tac [mdiff_def, normalize_def]);
+by (auto_tac (claset(), simpset()
+ addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
+qed "mdiff_0_right";
+Addsimps [mdiff_0_right];
+
Goal "multiset(M) ==> M +# {#a#} -# {#a#} = M";
by (rewrite_goals_tac [multiset_def, munion_def, mdiff_def,
msingle_def, normalize_def, mset_of_def]);
by (auto_tac (claset(),
simpset() addcongs [if_cong]
addsimps [ltD, multiset_fun_iff,
- funrestrict_def, subset_Un_iff2 RS iffD1]));
+ funrestrict_def, subset_Un_iff2 RS iffD1]));
+by (force_tac (claset() addSIs [lam_type], simpset()) 2);
by (subgoal_tac "{x \\<in> A \\<union> {a} . x \\<noteq> a \\<and> x \\<in> A} = A" 2);
by (rtac fun_extension 1);
by Auto_tac;
+by (dres_inst_tac [("x","A Un {a}")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [Finite_Un]) 1);
+by (force_tac (claset() addSIs [lam_type], simpset()) 1);
qed "mdiff_union_inverse2";
Addsimps [mdiff_union_inverse2];
@@ -322,14 +321,16 @@
Addsimps [mcount_union];
Goalw [multiset_def]
-"[| multiset(M); multiset(N) |] \
-\ ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)";
+"multiset(M) ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)";
by (auto_tac (claset() addSDs [not_lt_imp_le],
simpset() addsimps [mdiff_def, multiset_fun_iff,
mcount_def, normalize_def, mset_of_def]));
+by (force_tac (claset() addSIs [lam_type], simpset()) 1);
+by (force_tac (claset() addSIs [lam_type], simpset()) 1);
qed "mcount_diff";
Addsimps [mcount_diff];
+
Goalw [multiset_def]
"[| multiset(M); a:mset_of(M) |] ==> 0 < mcount(M, a)";
by (Clarify_tac 1);
@@ -773,6 +774,20 @@
by Auto_tac;
qed "munion_eq_conv_diff";
+Goalw [multiset_def]
+"multiset(M) ==> \
+\ k:mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k~= a & k:mset_of(M))";
+by (rewrite_goals_tac [normalize_def, mset_of_def, msingle_def,
+ mdiff_def, mcount_def]);
+by (auto_tac (claset() addDs [domain_type]
+ addIs [zero_less_diff RS iffD1],
+ simpset() addsimps
+ [multiset_fun_iff, apply_iff]));
+by (force_tac (claset() addSIs [lam_type], simpset()) 1);
+by (force_tac (claset() addSIs [lam_type], simpset()) 1);
+by (force_tac (claset() addSIs [lam_type], simpset()) 1);
+qed "melem_diff_single";
+
Goal
"[| M:Mult(A); N:Mult(A) |] \
\ ==> (M +# {#a#} = N +# {#b#}) <-> \
@@ -1010,8 +1025,7 @@
qed "mdiff_union_single_conv";
Goal "[| n le m; m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
-by (auto_tac (claset(), simpset() addsimps
- [le_iff, diff_self_eq_0, less_iff_succ_add]));
+by (auto_tac (claset(), simpset() addsimps [le_iff, less_iff_succ_add]));
qed "diff_add_commute";
(* One direction *)
@@ -1252,8 +1266,8 @@
"[|<M, N>:multirel(A, r); K:Mult(A)|] ==> <M +# K, N +# K>:multirel(A, r)";
by (ftac (multirel_type RS subsetD) 1);
by (res_inst_tac [("P", "%x. <x,?u>:multirel(A, r)")] (munion_commute RS subst) 1);
-by (stac (munion_commute RS sym) 3);
-by (rtac munion_multirel_mono2 5);
+by (stac (munion_commute RS sym) 1);
+by (rtac munion_multirel_mono2 1);
by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
qed "munion_multirel_mono1";
@@ -1292,7 +1306,8 @@
Addsimps [munion_omultiset];
Goalw [omultiset_def] "omultiset(M) ==> omultiset(M -# N)";
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1);
by (res_inst_tac [("x", "i")] exI 1);
by (Asm_simp_tac 1);
qed "mdiff_omultiset";
--- a/src/ZF/Induct/Multiset.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Induct/Multiset.thy Tue May 27 11:39:03 2003 +0200
@@ -13,7 +13,7 @@
(* Short cut for multiset space *)
Mult :: i=>i
translations
- "Mult(A)" => "A-||>nat-{0}"
+ "Mult(A)" => "A -||> nat-{0}"
constdefs
@@ -26,7 +26,7 @@
(* M is a multiset *)
multiset :: i => o
- "multiset(M) == EX A. M:A->nat-{0} & Finite(A)"
+ "multiset(M) == EX A. M : A -> nat-{0} & Finite(A)"
mset_of :: "i=>i"
"mset_of(M) == domain(M)"
@@ -36,9 +36,12 @@
if x:mset_of(M) Int mset_of(N) then (M`x) #+ (N`x)
else (if x:mset_of(M) then M`x else N`x)"
- (* eliminating 0's from a function *)
+ (*convert a function to a multiset by eliminating 0*)
normalize :: i => i
- "normalize(M) == funrestrict(M, {x:mset_of(M). 0<M`x})"
+ "normalize(f) ==
+ if (EX A. f : A -> nat & Finite(A)) then
+ funrestrict(f, {x:mset_of(f). 0 < f`x})
+ else 0"
mdiff :: "[i, i] => i" (infixl "-#" 65)
"M -# N == normalize(lam x:mset_of(M).
--- a/src/ZF/List.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/List.thy Tue May 27 11:39:03 2003 +0200
@@ -135,7 +135,7 @@
(*An elimination rule, for type-checking*)
inductive_cases ConsE: "Cons(a,l) : list(A)"
-lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
+lemma Cons_type_iff [simp]: "Cons(a,l) \\<in> list(A) <-> a \\<in> A & l \\<in> list(A)"
by (blast elim: ConsE)
(*Proving freeness results*)
@@ -243,7 +243,7 @@
by (simp add: length_list_def)
lemma lt_length_in_nat:
- "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
+ "[|x < length(xs); xs \\<in> list(A)|] ==> x \\<in> nat"
by (frule lt_nat_in_nat, typecheck)
(** app **)
@@ -349,11 +349,11 @@
(*Lemma for the inductive step of drop_length*)
lemma drop_length_Cons [rule_format]:
"xs: list(A) ==>
- \<forall>x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
+ \\<forall>x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
by (erule list.induct, simp_all)
lemma drop_length [rule_format]:
- "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
+ "l: list(A) ==> \\<forall>i \\<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
apply (erule list.induct, simp_all, safe)
apply (erule drop_length_Cons)
apply (rule natE)
@@ -435,18 +435,18 @@
lemma list_complete_induct_lemma [rule_format]:
assumes ih:
- "\<And>l. [| l \<in> list(A);
- \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|]
+ "\\<And>l. [| l \\<in> list(A);
+ \\<forall>l' \\<in> list(A). length(l') < length(l) --> P(l')|]
==> P(l)"
- shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n --> P(l)"
+ shows "n \\<in> nat ==> \\<forall>l \\<in> list(A). length(l) < n --> P(l)"
apply (induct_tac n, simp)
apply (blast intro: ih elim!: leE)
done
theorem list_complete_induct:
- "[| l \<in> list(A);
- \<And>l. [| l \<in> list(A);
- \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|]
+ "[| l \\<in> list(A);
+ \\<And>l. [| l \\<in> list(A);
+ \\<forall>l' \\<in> list(A). length(l') < length(l) --> P(l')|]
==> P(l)
|] ==> P(l)"
apply (rule list_complete_induct_lemma [of A])
@@ -567,7 +567,7 @@
done
lemma append_eq_append_iff [rule_format,simp]:
- "xs:list(A) ==> \<forall>ys \<in> list(A).
+ "xs:list(A) ==> \\<forall>ys \\<in> list(A).
length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
apply (erule list.induct)
apply (simp (no_asm_simp))
@@ -577,7 +577,7 @@
lemma append_eq_append [rule_format]:
"xs:list(A) ==>
- \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
+ \\<forall>ys \\<in> list(A). \\<forall>us \\<in> list(A). \\<forall>vs \\<in> list(A).
length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"
apply (induct_tac "xs")
apply (force simp add: length_app, clarify)
@@ -604,7 +604,7 @@
(* Can also be proved from append_eq_append_iff2,
but the proof requires two more hypotheses: x:A and y:A *)
lemma append1_eq_iff [rule_format,simp]:
- "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
+ "xs:list(A) ==> \\<forall>ys \\<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
apply (erule list.induct)
apply clarify
apply (erule list.cases)
@@ -641,40 +641,40 @@
by (erule list.induct, auto)
lemma rev_is_rev_iff [rule_format,simp]:
- "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
+ "xs:list(A) ==> \\<forall>ys \\<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
apply (erule list.induct, force, clarify)
apply (erule_tac a = ys in list.cases, auto)
done
lemma rev_list_elim [rule_format]:
"xs:list(A) ==>
- (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
+ (xs=Nil --> P) --> (\\<forall>ys \\<in> list(A). \\<forall>y \\<in> A. xs =ys@[y] -->P)-->P"
by (erule list_append_induct, auto)
(** more theorems about drop **)
lemma length_drop [rule_format,simp]:
- "n:nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
+ "n:nat ==> \\<forall>xs \\<in> list(A). length(drop(n, xs)) = length(xs) #- n"
apply (erule nat_induct)
apply (auto elim: list.cases)
done
lemma drop_all [rule_format,simp]:
- "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> drop(n, xs)=Nil"
+ "n:nat ==> \\<forall>xs \\<in> list(A). length(xs) le n --> drop(n, xs)=Nil"
apply (erule nat_induct)
apply (auto elim: list.cases)
done
lemma drop_append [rule_format]:
"n:nat ==>
- \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
+ \\<forall>xs \\<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
apply (induct_tac "n")
apply (auto elim: list.cases)
done
lemma drop_drop:
- "m:nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
+ "m:nat ==> \\<forall>xs \\<in> list(A). \\<forall>n \\<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
apply (induct_tac "m")
apply (auto elim: list.cases)
done
@@ -695,20 +695,20 @@
by (unfold take_def, auto)
lemma take_all [rule_format,simp]:
- "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> take(n, xs) = xs"
+ "n:nat ==> \\<forall>xs \\<in> list(A). length(xs) le n --> take(n, xs) = xs"
apply (erule nat_induct)
apply (auto elim: list.cases)
done
lemma take_type [rule_format,simp,TC]:
- "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
+ "xs:list(A) ==> \\<forall>n \\<in> nat. take(n, xs):list(A)"
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
done
lemma take_append [rule_format,simp]:
"xs:list(A) ==>
- \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
+ \\<forall>ys \\<in> list(A). \\<forall>n \\<in> nat. take(n, xs @ ys) =
take(n, xs) @ take(n #- length(xs), ys)"
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
@@ -716,7 +716,7 @@
lemma take_take [rule_format]:
"m : nat ==>
- \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
+ \\<forall>xs \\<in> list(A). \\<forall>n \\<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
apply (induct_tac "m", auto)
apply (erule_tac a = xs in list.cases)
apply (auto simp add: take_Nil)
@@ -736,20 +736,21 @@
by (simp add: nth_def)
lemma nth_type [rule_format,simp,TC]:
- "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n,xs) : A"
-apply (erule list.induct, simp, clarify)
-apply (erule natE, auto)
+ "xs:list(A) ==> \\<forall>n. n < length(xs) --> nth(n,xs) : A"
+apply (erule list.induct, simp, clarify)
+apply (subgoal_tac "n \\<in> nat")
+ apply (erule natE, auto dest!: le_in_nat)
done
lemma nth_eq_0 [rule_format]:
- "xs:list(A) ==> \<forall>n \<in> nat. length(xs) le n --> nth(n,xs) = 0"
+ "xs:list(A) ==> \\<forall>n \\<in> nat. length(xs) le n --> nth(n,xs) = 0"
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
done
lemma nth_append [rule_format]:
"xs:list(A) ==>
- \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
+ \\<forall>n \\<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
else nth(n #- length(xs), ys))"
apply (induct_tac "xs", simp, clarify)
apply (erule natE, auto)
@@ -768,8 +769,8 @@
lemma nth_take_lemma [rule_format]:
"k:nat ==>
- \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
- (\<forall>i \<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))"
+ \\<forall>xs \\<in> list(A). (\\<forall>ys \\<in> list(A). k le length(xs) --> k le length(ys) -->
+ (\\<forall>i \\<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))"
apply (induct_tac "k")
apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
apply clarify
@@ -786,7 +787,7 @@
lemma nth_equalityI [rule_format]:
"[| xs:list(A); ys:list(A); length(xs) = length(ys);
- \<forall>i \<in> nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]
+ \\<forall>i \\<in> nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]
==> xs = ys"
apply (subgoal_tac "length (xs) le length (ys) ")
apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma)
@@ -796,7 +797,7 @@
(*The famous take-lemma*)
lemma take_equalityI [rule_format]:
- "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |]
+ "[| xs:list(A); ys:list(A); (\\<forall>i \\<in> nat. take(i, xs) = take(i,ys)) |]
==> xs = ys"
apply (case_tac "length (xs) le length (ys) ")
apply (drule_tac x = "length (ys) " in bspec)
@@ -809,7 +810,7 @@
done
lemma nth_drop [rule_format]:
- "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
+ "n:nat ==> \\<forall>i \\<in> nat. \\<forall>xs \\<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
apply (induct_tac "n", simp_all, clarify)
apply (erule list.cases, auto)
done
@@ -823,10 +824,10 @@
primrec (*explicit lambda is required because both arguments of "un" vary*)
"zip_aux(B,[]) =
- (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
+ (\\<lambda>ys \\<in> list(B). list_case([], %y l. [], ys))"
"zip_aux(B,Cons(x,l)) =
- (\<lambda>ys \<in> list(B).
+ (\\<lambda>ys \\<in> list(B).
list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
constdefs
@@ -836,7 +837,7 @@
(* zip equations *)
-lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
+lemma list_on_set_of_list: "xs \\<in> list(A) ==> xs \\<in> list(set_of_list(xs))"
apply (induct_tac xs, simp_all)
apply (blast intro: list_mono [THEN subsetD])
done
@@ -852,8 +853,8 @@
done
lemma zip_aux_unique [rule_format]:
- "[|B<=C; xs \<in> list(A)|]
- ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
+ "[|B<=C; xs \\<in> list(A)|]
+ ==> \\<forall>ys \\<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
apply (induct_tac xs)
apply simp_all
apply (blast intro: list_mono [THEN subsetD], clarify)
@@ -871,7 +872,7 @@
done
lemma zip_type [rule_format,simp,TC]:
- "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
+ "xs:list(A) ==> \\<forall>ys \\<in> list(B). zip(xs, ys):list(A*B)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
@@ -880,7 +881,7 @@
(* zip length *)
lemma length_zip [rule_format,simp]:
- "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
+ "xs:list(A) ==> \\<forall>ys \\<in> list(B). length(zip(xs,ys)) =
min(length(xs), length(ys))"
apply (unfold min_def)
apply (induct_tac "xs", simp_all, clarify)
@@ -889,14 +890,14 @@
lemma zip_append1 [rule_format]:
"[| ys:list(A); zs:list(B) |] ==>
- \<forall>xs \<in> list(A). zip(xs @ ys, zs) =
+ \\<forall>xs \\<in> list(A). zip(xs @ ys, zs) =
zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
apply (induct_tac "zs", force, clarify)
apply (erule_tac a = xs in list.cases, simp_all)
done
lemma zip_append2 [rule_format]:
- "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
+ "[| xs:list(A); zs:list(B) |] ==> \\<forall>ys \\<in> list(B). zip(xs, ys@zs) =
zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
apply (induct_tac "xs", force, clarify)
apply (erule_tac a = ys in list.cases, auto)
@@ -910,7 +911,7 @@
lemma zip_rev [rule_format,simp]:
- "ys:list(B) ==> \<forall>xs \<in> list(A).
+ "ys:list(B) ==> \\<forall>xs \\<in> list(A).
length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
apply (induct_tac "ys", force, clarify)
apply (erule_tac a = xs in list.cases)
@@ -918,7 +919,7 @@
done
lemma nth_zip [rule_format,simp]:
- "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
+ "ys:list(B) ==> \\<forall>i \\<in> nat. \\<forall>xs \\<in> list(A).
i < length(xs) --> i < length(ys) -->
nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
apply (induct_tac "ys", force, clarify)
@@ -948,7 +949,7 @@
done
lemma list_update_type [rule_format,simp,TC]:
- "[| xs:list(A); v:A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
+ "[| xs:list(A); v:A |] ==> \\<forall>n \\<in> nat. list_update(xs, n, v):list(A)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
@@ -956,7 +957,7 @@
done
lemma length_list_update [rule_format,simp]:
- "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
+ "xs:list(A) ==> \\<forall>i \\<in> nat. length(list_update(xs, i, v))=length(xs)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
@@ -964,7 +965,7 @@
done
lemma nth_list_update [rule_format]:
- "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs) -->
+ "[| xs:list(A) |] ==> \\<forall>i \\<in> nat. \\<forall>j \\<in> nat. i < length(xs) -->
nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
apply (induct_tac "xs")
apply simp_all
@@ -982,7 +983,7 @@
lemma nth_list_update_neq [rule_format,simp]:
"xs:list(A) ==>
- \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
+ \\<forall>i \\<in> nat. \\<forall>j \\<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
@@ -992,7 +993,7 @@
done
lemma list_update_overwrite [rule_format,simp]:
- "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
+ "xs:list(A) ==> \\<forall>i \\<in> nat. i < length(xs)
--> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
apply (induct_tac "xs")
apply (simp (no_asm))
@@ -1002,7 +1003,7 @@
lemma list_update_same_conv [rule_format]:
"xs:list(A) ==>
- \<forall>i \<in> nat. i < length(xs) -->
+ \\<forall>i \\<in> nat. i < length(xs) -->
(list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
apply (induct_tac "xs")
apply (simp (no_asm))
@@ -1012,7 +1013,7 @@
lemma update_zip [rule_format]:
"ys:list(B) ==>
- \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
+ \\<forall>i \\<in> nat. \\<forall>xy \\<in> A*B. \\<forall>xs \\<in> list(A).
length(xs) = length(ys) -->
list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
list_update(ys, i, snd(xy)))"
@@ -1024,7 +1025,7 @@
lemma set_update_subset_cons [rule_format]:
"xs:list(A) ==>
- \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))"
+ \\<forall>i \\<in> nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))"
apply (induct_tac "xs")
apply simp
apply (rule ballI)
@@ -1091,7 +1092,7 @@
lemma take_upt [rule_format,simp]:
"[| m:nat; n:nat |] ==>
- \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
+ \\<forall>i \\<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
apply (induct_tac "m")
apply (simp (no_asm_simp) add: take_0)
apply clarify
@@ -1111,7 +1112,7 @@
lemma nth_map [rule_format,simp]:
"xs:list(A) ==>
- \<forall>n \<in> nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"
+ \\<forall>n \\<in> nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"
apply (induct_tac "xs", simp)
apply (rule ballI)
apply (induct_tac "n", auto)
@@ -1119,7 +1120,7 @@
lemma nth_map_upt [rule_format]:
"[| m:nat; n:nat |] ==>
- \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
+ \\<forall>i \\<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp)
apply (subst map_succ_upt [symmetric], simp_all, clarify)
apply (subgoal_tac "i < length (upt (0, x))")
@@ -1187,17 +1188,20 @@
lemma sublist_singleton [simp]:
"sublist([x], A) = (if 0 : A then [x] else [])"
-by (simp (no_asm) add: sublist_Cons)
-
+by (simp add: sublist_Cons)
-lemma sublist_upt_eq_take [simp]:
- "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)"
-apply (unfold less_than_def)
-apply (erule_tac l = xs in list_append_induct, simp)
-apply (simp split add: nat_diff_split add: sublist_append, auto)
-apply (subgoal_tac "n #- length (y) = 0")
-apply (simp (no_asm_simp))
-apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff)
+lemma sublist_upt_eq_take [rule_format, simp]:
+ "xs:list(A) ==> ALL n:nat. sublist(xs,n) = take(n,xs)"
+apply (erule list.induct, simp)
+apply (clarify );
+apply (erule natE)
+apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
+done
+
+lemma sublist_Int_eq:
+ "xs : list(B) ==> sublist(xs, A \\<inter> nat) = sublist(xs, A)"
+apply (erule list.induct)
+apply (simp_all add: sublist_Cons)
done
text{*Repetition of a List Element*}
@@ -1208,15 +1212,15 @@
"repeat(a,succ(n)) = Cons(a,repeat(a,n))"
-lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
+lemma length_repeat: "n \\<in> nat ==> length(repeat(a,n)) = n"
by (induct_tac n, auto)
-lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
+lemma repeat_succ_app: "n \\<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
apply (induct_tac n)
apply (simp_all del: app_Cons add: app_Cons [symmetric])
done
-lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
+lemma repeat_type [TC]: "[|a \\<in> A; n \\<in> nat|] ==> repeat(a,n) \\<in> list(A)"
by (induct_tac n, auto)
@@ -1373,6 +1377,7 @@
val sublist_Cons = thm "sublist_Cons";
val sublist_singleton = thm "sublist_singleton";
val sublist_upt_eq_take = thm "sublist_upt_eq_take";
+val sublist_Int_eq = thm "sublist_Int_eq";
structure list =
struct
--- a/src/ZF/Nat.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Nat.thy Tue May 27 11:39:03 2003 +0200
@@ -38,12 +38,13 @@
Gt :: i
"Gt == {<x,y>:nat*nat. y < x}"
- less_than :: "i=>i"
- "less_than(n) == {i:nat. i<n}"
-
greater_than :: "i=>i"
"greater_than(n) == {i:nat. n < i}"
+text{*No need for a less-than operator: a natural number is its list of
+predecessors!*}
+
+
lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
apply (rule bnd_monoI)
apply (cut_tac infinity, blast, blast)
@@ -281,6 +282,14 @@
lemma nat_nonempty [simp]: "nat ~= 0"
by blast
+text{*A natural number is the set of its predecessors*}
+lemma nat_eq_Collect_lt: "i \<in> nat ==> {j\<in>nat. j<i} = i"
+apply (rule equalityI)
+apply (blast dest: ltD)
+apply (auto simp add: Ord_mem_iff_lt)
+apply (blast intro: lt_trans)
+done
+
ML
{*
@@ -288,7 +297,6 @@
val Lt_def = thm "Lt_def";
val Ge_def = thm "Ge_def";
val Gt_def = thm "Gt_def";
-val less_than_def = thm "less_than_def";
val greater_than_def = thm "greater_than_def";
val nat_bnd_mono = thm "nat_bnd_mono";
--- a/src/ZF/OrderType.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/OrderType.thy Tue May 27 11:39:03 2003 +0200
@@ -279,7 +279,7 @@
apply (rule image_fun [OF ordermap_type subset_refl])
done
-(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
+text{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}
lemma ordertype_pred_subset: "[| well_ord(A,r); x:A |] ==>
ordertype(pred(A,x,r),r) <= ordertype(A,r)"
@@ -334,7 +334,7 @@
subsubsection{*Order Type calculations for radd *}
-(** Addition with 0 **)
+text{*Addition with 0 *}
lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
apply (rule_tac d = Inl in lam_bijective, safe)
@@ -360,7 +360,7 @@
apply force
done
-(** Initial segments of radd. Statements by Grabczewski **)
+text{*Initial segments of radd. Statements by Grabczewski *}
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
lemma pred_Inl_bij:
@@ -418,7 +418,7 @@
by (simp add: oadd_def Ord_raw_oadd)
-(** Ordinal addition with zero **)
+text{*Ordinal addition with zero *}
lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"
by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq
@@ -464,7 +464,7 @@
apply (auto simp add: Ord_oadd lt_oadd1)
done
-(** Various other results **)
+text{*Various other results *}
lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
apply (rule id_bij [THEN ord_isoI])
@@ -588,7 +588,7 @@
done
-(** Ordinal addition with limit ordinals **)
+text{*Ordinal addition with limit ordinals *}
lemma oadd_UN:
"[| !!x. x:A ==> Ord(j(x)); a:A |]
@@ -625,7 +625,7 @@
apply (simp add: Limit_def lt_def)
done
-(** Order/monotonicity properties of ordinal addition **)
+text{*Order/monotonicity properties of ordinal addition *}
lemma oadd_le_self2: "Ord(i) ==> i le j++i"
apply (erule_tac i = i in trans_induct3)
@@ -679,9 +679,10 @@
done
-(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)).
- Probably simpler to define the difference recursively!
-**)
+subsection{*Ordinal Subtraction*}
+
+text{*The difference is @{term "ordertype(j-i, Memrel(j))"}.
+ It's probably simpler to define the difference recursively!*}
lemma bij_sum_Diff:
"A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
@@ -829,7 +830,7 @@
subsubsection{*Basic laws for ordinal multiplication *}
-(** Ordinal multiplication by zero **)
+text{*Ordinal multiplication by zero *}
lemma omult_0 [simp]: "i**0 = 0"
apply (unfold omult_def)
@@ -841,7 +842,7 @@
apply (simp (no_asm_simp))
done
-(** Ordinal multiplication by 1 **)
+text{*Ordinal multiplication by 1 *}
lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
apply (unfold omult_def)
@@ -859,7 +860,7 @@
apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
done
-(** Distributive law for ordinal multiplication and addition **)
+text{*Distributive law for ordinal multiplication and addition *}
lemma oadd_omult_distrib:
"[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"
@@ -880,7 +881,7 @@
lemma omult_succ: "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"
by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)
-(** Associative law **)
+text{*Associative law *}
lemma omult_assoc:
"[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"
@@ -897,7 +898,7 @@
done
-(** Ordinal multiplication with limit ordinals **)
+text{*Ordinal multiplication with limit ordinals *}
lemma omult_UN:
"[| Ord(i); !!x. x:A ==> Ord(j(x)) |]
@@ -966,7 +967,7 @@
done
-(** Further properties of ordinal multiplication **)
+text{*Further properties of ordinal multiplication *}
lemma omult_inject: "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"
apply (rule Ord_linear_lt)
@@ -975,6 +976,35 @@
apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
done
+subsection{*The Relation @{term Lt}*}
+
+lemma wf_Lt: "wf(Lt)"
+apply (rule wf_subset)
+apply (rule wf_Memrel)
+apply (auto simp add: Lt_def Memrel_def lt_def)
+done
+
+lemma irrefl_Lt: "irrefl(A,Lt)"
+by (auto simp add: Lt_def irrefl_def)
+
+lemma trans_Lt: "trans[A](Lt)"
+apply (simp add: Lt_def trans_on_def)
+apply (blast intro: lt_trans)
+done
+
+lemma part_ord_Lt: "part_ord(A,Lt)"
+by (simp add: part_ord_def irrefl_Lt trans_Lt)
+
+lemma linear_Lt: "linear(nat,Lt)"
+apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff)
+apply (drule lt_asym, auto)
+done
+
+lemma tot_ord_Lt: "tot_ord(nat,Lt)"
+by (simp add: tot_ord_def linear_Lt part_ord_Lt)
+
+
+
ML {*
val ordermap_def = thm "ordermap_def";
val ordertype_def = thm "ordertype_def";
@@ -1080,6 +1110,13 @@
val omult_lt_mono = thm "omult_lt_mono";
val omult_le_self2 = thm "omult_le_self2";
val omult_inject = thm "omult_inject";
+
+val wf_Lt = thm "wf_Lt";
+val irrefl_Lt = thm "irrefl_Lt";
+val trans_Lt = thm "trans_Lt";
+val part_ord_Lt = thm "part_ord_Lt";
+val linear_Lt = thm "linear_Lt";
+val tot_ord_Lt = thm "tot_ord_Lt";
*}
end
--- a/src/ZF/UNITY/Comp.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Comp.ML Tue May 27 11:39:03 2003 +0200
@@ -109,6 +109,15 @@
(*** preserves ***)
+Goalw [preserves_def, safety_prop_def]
+ "safety_prop(preserves(f))";
+by (auto_tac (claset() addDs [ActsD], simpset() addsimps [stable_def, constrains_def]));
+by (dres_inst_tac [("c", "act")] subsetD 1);
+by Auto_tac;
+qed "preserves_is_safety_prop";
+Addsimps [preserves_is_safety_prop];
+
+
val prems = Goalw [preserves_def]
"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)";
by Auto_tac;
@@ -142,6 +151,86 @@
AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
+Goalw [fun_pair_def] "fun_pair(f,g,x) = <f(x), g(x)>";
+by (Simp_tac 1);
+qed "fun_pair_apply";
+Addsimps [fun_pair_apply];
+
+Goal "preserves(fun_pair(v,w)) = preserves(v) Int preserves(w)";
+by (rtac equalityI 1);
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
+by (REPEAT(Blast_tac 1));
+qed "preserves_fun_pair";
+
+Goal "F:preserves(fun_pair(v, w)) <-> F:preserves(v) Int preserves(w)";
+by (simp_tac (simpset() addsimps [preserves_fun_pair]) 1);
+qed "preserves_fun_pair_iff";
+AddIffs [preserves_fun_pair_iff];
+
+Goal "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)";
+by (simp_tac (simpset() addsimps [fun_pair_def, comp_def]) 1);
+qed "fun_pair_comp_distrib";
+
+Goal "(f comp g)(x) = f(g(x))";
+by (simp_tac (simpset() addsimps [comp_def]) 1);
+qed "comp_apply";
+Addsimps [comp_apply];
+
+Goalw [preserves_def]
+ "preserves(v)<=program";
+by Auto_tac;
+qed "preserves_type";
+
+Goal "F:preserves(f) ==> F:program";
+by (blast_tac (claset() addIs [preserves_type RS subsetD]) 1);
+qed "preserves_into_program";
+AddTCs [preserves_into_program];
+
+Goal "preserves(f) <= preserves(g comp f)";
+by (auto_tac (claset(), simpset()
+ addsimps [preserves_def, stable_def, constrains_def]));
+by (dres_inst_tac [("x", "f(xb)")] spec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by Auto_tac;
+qed "subset_preserves_comp";
+
+Goal "F:preserves(f) ==> F:preserves(g comp f)";
+by (blast_tac (claset() addIs [subset_preserves_comp RS subsetD]) 1);
+qed "imp_preserves_comp";
+
+Goal "preserves(f) <= stable({s:state. P(f(s))})";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
+by (rename_tac "s' s" 1);
+by (subgoal_tac "f(s) = f(s')" 1);
+by (ALLGOALS Force_tac);
+qed "preserves_subset_stable";
+
+Goal "F:preserves(f) ==> F:stable({s:state. P(f(s))})";
+by (blast_tac (claset() addIs [preserves_subset_stable RS subsetD]) 1);
+qed "preserves_imp_stable";
+
+Goalw [increasing_def]
+ "[| F:preserves(f); ALL x:state. f(x):A |] ==> F:Increasing.increasing(A, r, f)";
+by (auto_tac (claset() addIs [preserves_into_program],
+ simpset()));
+by (res_inst_tac [("P", "%x. <k, x>:r")] preserves_imp_stable 1);
+by Auto_tac;
+qed "preserves_imp_increasing";
+
+Goalw [preserves_def, stable_def, constrains_def]
+ "st_set(A) ==> preserves(%x. x) <= stable(A)";
+by Auto_tac;
+by (dres_inst_tac [("x", "xb")] spec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by (auto_tac (claset() addDs [ActsD], simpset()));
+qed "preserves_id_subset_stable";
+
+Goal "[| F:preserves(%x. x); st_set(A) |] ==> F:stable(A)";
+by (blast_tac (claset() addIs [preserves_id_subset_stable RS subsetD]) 1);
+qed "preserves_id_imp_stable";
+
(** Added by Sidi **)
(** component_of **)
@@ -190,3 +279,70 @@
AddIffs [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
+(** Theorems used in ClientImpl **)
+
+Goal
+ "[| F:stable({s:state. P(f(s), g(s))}); G:preserves(f); G:preserves(g) |] \
+\ ==> F Join G : stable({s:state. P(f(s), g(s))})";
+by (auto_tac (claset() addDs [ActsD, preserves_into_program],
+ simpset() addsimps [stable_def, constrains_def]));
+by (case_tac "act:Acts(F)" 1);
+by Auto_tac;
+by (dtac preserves_imp_eq 1);
+by (dtac preserves_imp_eq 3);
+by Auto_tac;
+qed "stable_localTo_stable2";
+
+Goal "[| F : stable({s:state. <f(s), g(s)>:r}); G:preserves(f); \
+\ F Join G : Increasing(A, r, g); \
+\ ALL x:state. f(x):A & g(x):A |] \
+\ ==> F Join G : Stable({s:state. <f(s), g(s)>:r})";
+by (auto_tac (claset(),
+ simpset() addsimps [stable_def, Stable_def, Increasing_def,
+ Constrains_def, all_conj_distrib]));
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [constrains_type RS subsetD, preserves_type RS subsetD])));
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+(*The G case remains*)
+by (auto_tac (claset() addDs [ActsD],
+ simpset() addsimps [preserves_def, stable_def, constrains_def,
+ ball_conj_distrib, all_conj_distrib]));
+(*We have a G-action, so delete assumptions about F-actions*)
+by (thin_tac "ALL act:Acts(F). ?P(act)" 1);
+by (thin_tac "\\<forall>k\\<in>A. ALL act:Acts(F). ?P(k,act)" 1);
+by (subgoal_tac "f(x) = f(xa)" 1);
+by (auto_tac (claset() addSDs [bspec], simpset()));
+qed "Increasing_preserves_Stable";
+
+
+(** Lemma used in AllocImpl **)
+
+Goalw [Constrains_def, constrains_def]
+"[| ALL x:I. F: A(x) Co B; F:program |] ==> F:(UN x:I. A(x)) Co B";
+by Auto_tac;
+qed "Constrains_UN_left";
+
+Goalw [stable_def, Stable_def, preserves_def]
+ "[| F:stable({s:state. P(f(s), g(s))}); \
+\ ALL k:A. F Join G: Stable({s:state. P(k, g(s))}); \
+\ G:preserves(f); ALL s:state. f(s):A|] ==> \
+\ F Join G : Stable({s:state. P(f(s), g(s))})";
+by (res_inst_tac [("A", "(UN k:A. {s:state. f(s)=k} Int {s:state. P(f(s), g(s))})")]
+ Constrains_weaken_L 1);
+by (Blast_tac 2);
+by (rtac Constrains_UN_left 1);
+by Auto_tac;
+by (res_inst_tac [("A", "{s:state. f(s)=k} Int {s:state. P(f(s), g(s))} Int \
+\ {s:state. P(k, g(s))}"),
+ ("A'", "({s:state. f(s)=k} Un {s:state. P(f(s), g(s))}) \
+\ Int {s:state. P(k, g(s))}")] Constrains_weaken 1);
+by (REPEAT(Blast_tac 2));
+by (rtac Constrains_Int 1);
+by (rtac constrains_imp_Constrains 1);
+by (auto_tac (claset(), simpset() addsimps [constrains_type RS subsetD]));
+by (ALLGOALS(rtac constrains_weaken));
+by (rotate_tac ~1 4);
+by (dres_inst_tac [("x", "k")] spec 4);
+by (REPEAT(Blast_tac 1));
+qed "stable_Join_Stable";
+
--- a/src/ZF/UNITY/Comp.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Comp.thy Tue May 27 11:39:03 2003 +0200
@@ -15,7 +15,7 @@
*)
-Comp = Union +
+Comp = Union + Increasing +
constdefs
@@ -36,9 +36,12 @@
preserves :: (i=>i)=>i
"preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}"
+ fun_pair :: "[i=>i, i =>i] =>(i=>i)"
+ "fun_pair(f, g) == %x. <f(x), g(x)>"
+
localize :: "[i=>i, i] => i"
"localize(f,F) == mk_program(Init(F), Acts(F),
- AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
+ AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
end
--- a/src/ZF/UNITY/Constrains.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Constrains.ML Tue May 27 11:39:03 2003 +0200
@@ -429,78 +429,6 @@
(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
-(*** Increasing ***)
-
-Goalw [Increasing_def] "Increasing(A,r,f) <= program";
-by (auto_tac (claset() addDs [Stable_type RS subsetD]
- addSDs [bspec], simpset() addsimps [INT_iff]));
-qed "Increasing_type";
-
-Goalw [Increasing_def]
-"[| F:Increasing(A, r, f); a:A |] ==> F: Stable({s:state. <a,f`s>:r})";
-by (Blast_tac 1);
-qed "IncreasingD";
-
-Goalw [Increasing_def]
-"F:Increasing(A, r, f) ==> F:program & (EX a. a:A)";
-by (auto_tac (claset(), simpset() addsimps [INT_iff]));
-by (blast_tac (claset() addDs [Stable_type RS subsetD]) 1);
-qed "IncreasingD2";
-
-Goalw [increasing_def, Increasing_def]
- "F : increasing(A, r, f) ==> F : Increasing(A, r, f)";
-by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
-by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
-qed "increasing_imp_Increasing";
-
-Goal "F:Increasing(A, r, lam x:state. c) <-> F:program & (EX a. a:A)";
-by (auto_tac (claset() addDs [IncreasingD2]
- addIs [increasing_imp_Increasing], simpset()));
-qed "Increasing_constant";
-AddIffs [Increasing_constant];
-
-Goalw [Increasing_def, Stable_def, stable_def, Constrains_def,
- constrains_def, part_order_def, st_set_def]
-"[| g:mono_map(A,r,A,r); part_order(A, r); f:state->A |] \
-\ ==> Increasing(A, r,f) <= Increasing(A, r,g O f)";
-by (case_tac "A=0" 1);
-by (Asm_full_simp_tac 1);
-by (etac not_emptyE 1);
-by (Clarify_tac 1);
-by (cut_inst_tac [("F", "xa")] Acts_type 1);
-by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
-by Auto_tac;
-by (rename_tac "xa xc xd act xe xf" 1);
-by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1);
-by (dres_inst_tac [("x", "f`xf")] bspec 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "Acts(?u) <= ?v")] asm_rl 1);
-by (dres_inst_tac [("psi", "?u <= state")] asm_rl 1);
-by (dres_inst_tac [("c", "xe")] subsetD 1);
-by (rtac imageI 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [refl_def, apply_type]) 1);
-by (dres_inst_tac [("x1", "f`xf"), ("x", "f`xe")] (bspec RS bspec) 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type])));
-by (res_inst_tac [("b", "g ` (f ` xf)")] trans_onD 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type])));
-qed "mono_Increasing_comp";
-
-Goalw [Increasing_def]
- "[| F:Increasing(nat, {<m,n>:nat*nat. m le n}, f); f:state->nat; k:nat |] \
-\ ==> F: Stable({s:state. k < f`s})";
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "succ(k)")] bspec 1);
-by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
-by (subgoal_tac "{x: state . f`x : nat} = state" 1);
-by Auto_tac;
-qed "strict_IncreasingD";
-
(*To allow expansion of the program's definition when appropriate*)
val program_defs_ref = ref ([] : thm list);
--- a/src/ZF/UNITY/Constrains.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Constrains.thy Tue May 27 11:39:03 2003 +0200
@@ -57,8 +57,5 @@
Always :: "i => i"
"Always(A) == initially(A) Int Stable(A)"
- (* Increasing is the weak from of increasing *)
- Increasing :: [i,i, i] => i
- "Increasing(A, r, f) == INT a:A. Stable({s:state. <a, f`s>:r})"
end
--- a/src/ZF/UNITY/FP.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/FP.ML Tue May 27 11:39:03 2003 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/UNITY/FP.ML
+(* Title: ZF/UNITY/FP.ML
ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
@@ -28,10 +28,6 @@
qed "st_set_FP";
AddIffs [st_set_FP];
-Goal "Union(B) Int A = (UN C:B. C Int A)";
-by (Blast_tac 1);
-qed "Int_Union2";
-
Goalw [FP_Orig_def, stable_def] "F:program ==> F:stable(FP_Orig(F) Int B)";
by (stac Int_Union2 1);
by (blast_tac (claset() addIs [constrains_UN]) 1);
@@ -44,11 +40,6 @@
bind_thm("FP_Orig_weakest", allI RS FP_Orig_weakest2);
-Goal "A Int cons(a, B) = \
- \ (if a : A then cons(a, cons(a, (A Int B))) else A Int B)";
-by Auto_tac;
-qed "Int_cons_right";
-
Goal "F:program ==> F : stable (FP(F) Int B)";
by (subgoal_tac "FP(F) Int B = (UN x:B. FP(F) Int {x})" 1);
by (Blast_tac 2);
--- a/src/ZF/UNITY/GenPrefix.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/GenPrefix.ML Tue May 27 11:39:03 2003 +0200
@@ -279,19 +279,19 @@
by (rtac conjI 1);
by (blast_tac (claset() addIs [gen_prefix.append]) 1);
by (thin_tac "length(xs) < length(ys) -->?u" 1);
-by (case_tac "zs=[]" 1);
-by (auto_tac (claset(), simpset() addsimps [neq_Nil_iff]));
+by (eres_inst_tac [("a","zs")] list.elim 1);
+by Auto_tac;
by (res_inst_tac [("P1", "%x. <?u(x), ?v>:?w")] (nat_diff_split RS iffD2) 1);
by Auto_tac;
by (stac append_cons_conv 1);
-by (rtac gen_prefix.append 2);
+by (rtac gen_prefix.append 2);
by (auto_tac (claset() addEs [ConsE],
simpset() addsimps [gen_prefix_append_both]));
-val lemma = result() RS mp;
+val append_one_gen_prefix_lemma = result() RS mp;
Goal "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |] \
\ ==> <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
-by (blast_tac (claset() addIs [lemma]) 1);
+by (blast_tac (claset() addIs [append_one_gen_prefix_lemma]) 1);
qed "append_one_gen_prefix";
@@ -499,14 +499,11 @@
by (Clarify_tac 1);
by (eres_inst_tac [("xs", "ysa")] rev_list_elim 1);
by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("psi", "ya:list(A)")] asm_rl 1);
-by (rotate_tac ~1 1);
by (asm_full_simp_tac (simpset() addsimps [app_type, app_assoc RS sym]) 1);
by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
qed "prefix_snoc";
Addsimps [prefix_snoc];
-
Goal "zs:list(A) ==> ALL xs:list(A). ALL ys:list(A). \
\ (<xs, ys@zs>:prefix(A)) <-> \
\ (<xs,ys>:prefix(A) | (EX us. xs = ys@us & <us,zs>:prefix(A)))";
@@ -606,9 +603,34 @@
by (rtac (gen_prefix_mono RS subsetD) 1);
by Auto_tac;
qed "prefix_imp_pfixGe";
+(* Added by Sidi: prefix and take *)
-
+Goalw [prefix_def]
+"<xs, ys>:prefix(A) ==> xs=take(length(xs), ys)";
+by (etac gen_prefix.induct 1);
+by (subgoal_tac "length(xs):nat" 3);
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
+ simpset() addsimps [length_type]));
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (forward_tac [gen_prefix_length_le] 1);
+by (auto_tac (claset(), simpset() addsimps [take_append]));
+by (subgoal_tac "length(xs) #- length(ys)=0" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_is_0_iff])));
+qed "prefix_imp_take";
-
+Goalw [prefix_def]
+"xs:list(A) ==> ALL n:nat. <take(n, xs), xs>:prefix(A)";
+by (etac list.induct 1);
+by Auto_tac;
+by (etac natE 1);
+by Auto_tac;
+qed_spec_mp "take_prefix";
-
+Goal "<xs, ys>:prefix(A) <-> (xs=take(length(xs), ys) & xs:list(A) & ys:list(A))";
+by (rtac iffI 1);
+by (forward_tac [prefix_type RS subsetD] 1);
+by (blast_tac (claset() addIs [prefix_imp_take]) 1);
+by (Clarify_tac 1);
+by (etac ssubst 1);
+by (blast_tac (claset() addIs [take_prefix, length_type]) 1);
+qed "prefix_take_iff";
--- a/src/ZF/UNITY/GenPrefix.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy Tue May 27 11:39:03 2003 +0200
@@ -11,7 +11,7 @@
Based on Lex/Prefix
*)
-GenPrefix = ListPlus +
+GenPrefix = Main +
consts
gen_prefix :: "[i, i] => i"
@@ -38,14 +38,6 @@
strict_prefix :: i=>i
"strict_prefix(A) == prefix(A) - id(list(A))"
- (* Probably to be moved elsewhere *)
-
- Le :: i
- "Le == {<x,y>:nat*nat. x le y}"
-
- Ge :: i
- "Ge == {<x,y>:nat*nat. y le x}"
-
syntax
(* less or equal and greater or equal over prefixes *)
pfixLe :: [i, i] => o (infixl "pfixLe" 50)
--- a/src/ZF/UNITY/ListPlus.ML Mon May 26 18:36:15 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,349 +0,0 @@
-(* Title: ZF/UNITY/ListPlus.ML
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-More about lists
-
-*)
-
-(*** more theorems about lists ***)
-
-(** td and tl **)
-
-(** length **)
-
-Goal "xs:list(A) ==> length(xs)=0 <-> xs=Nil";
-by (etac list.induct 1);
-by Auto_tac;
-qed "length_is_0_iff";
-Addsimps [length_is_0_iff];
-
-Goal "xs:list(A) ==> 0 = length(xs) <-> xs=Nil";
-by (etac list.induct 1);
-by Auto_tac;
-qed "length_is_0_iff2";
-Addsimps [length_is_0_iff2];
-
-Goal "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1";
-by (etac list.induct 1);
-by Auto_tac;
-qed "length_tl";
-Addsimps [length_tl];
-
-Goal "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil";
-by (etac list.induct 1);
-by Auto_tac;
-qed "length_greater_0_iff";
-
-Goal "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "length_succ_iff";
-
-(** more theorems about append **)
-Goal "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "append_is_Nil_iff";
-Addsimps [append_is_Nil_iff];
-
-Goal "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "append_is_Nil_iff2";
-Addsimps [append_is_Nil_iff2];
-
-Goal "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "append_left_is_self_iff";
-Addsimps [append_left_is_self_iff];
-
-Goal "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "append_left_is_self_iff2";
-Addsimps [append_left_is_self_iff2];
-
-Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
-\ length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))";
-by (etac list.induct 1);
-by (auto_tac (claset(), simpset() addsimps [length_app, length_type]));
-qed_spec_mp "append_left_is_Nil_iff";
-Addsimps [append_left_is_Nil_iff];
-
-Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
-\ length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))";
-by (etac list.induct 1);
-by (auto_tac (claset(), simpset() addsimps [length_app, length_type]));
-qed_spec_mp "append_left_is_Nil_iff2";
-Addsimps [append_left_is_Nil_iff2];
-
-Goal "xs:list(A) ==> ALL ys:list(A). \
-\ length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)";
-by (etac list.induct 1);
-by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (eres_inst_tac [("a", "ys")] list.elim 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "append_eq_append_iff";
-
-
-Goal "xs:list(A) ==> \
-\ ALL ys:list(A). ALL us:list(A). ALL vs:list(A). \
-\ length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)";
-by (induct_tac "xs" 1);
-by (ALLGOALS(Clarify_tac));
-by (asm_full_simp_tac (simpset() addsimps [length_type, length_app]) 1);
-by (eres_inst_tac [("a", "ys")] list.elim 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "Cons(a, l) @ us =vs" 1);
-by (dtac (rotate_prems 4 (append_left_is_Nil_iff RS iffD1)) 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [length_type])));
-by Auto_tac;
-qed_spec_mp "append_eq_append";
-
-Goal "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] \
-\ ==> xs@us = ys@vs <-> (xs=ys & us=vs)";
-by (rtac iffI 1);
-by (rtac append_eq_append 1);
-by Auto_tac;
-qed "append_eq_append_iff2";
-Addsimps [append_eq_append_iff, append_eq_append_iff2];
-
-Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs";
-by (Asm_simp_tac 1);
-qed "append_self_iff";
-Addsimps [append_self_iff];
-
-Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs";
-by (Asm_simp_tac 1);
-qed "append_self_iff2";
-Addsimps [append_self_iff2];
-
-(* Can also be proved from append_eq_append_iff2
- if we add two more hypotheses x:A and y:A *)
-Goal "xs:list(A) ==> ALL ys:list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)";
-by (etac list.induct 1);
-by (ALLGOALS(Clarify_tac));
-by (ALLGOALS(eres_inst_tac [("a", "ys")] list.elim));
-by Auto_tac;
-qed_spec_mp "append1_eq_iff";
-Addsimps [append1_eq_iff];
-
-Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)";
-by (Asm_simp_tac 1);
-qed "append_right_is_self_iff";
-Addsimps [append_right_is_self_iff];
-
-Goal "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)";
-by (rtac iffI 1);
-by (dtac sym 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed "append_right_is_self_iff2";
-Addsimps [append_right_is_self_iff2];
-
-Goal "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "hd_append";
-Addsimps [hd_append];
-
-Goal "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "tl_append";
-Addsimps [tl_append];
-
-(** rev **)
-Goal "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "rev_is_Nil_iff";
-Addsimps [rev_is_Nil_iff];
-
-Goal "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)";
-by (etac list.induct 1);
-by Auto_tac;
-qed "Nil_is_rev_iff";
-Addsimps [Nil_is_rev_iff];
-
-Goal "xs:list(A) ==> ALL ys:list(A). rev(xs)=rev(ys) <-> xs=ys";
-by (etac list.induct 1);
-by (Force_tac 1);
-by (Clarify_tac 1);
-by (eres_inst_tac [("a", "ys")] list.elim 1);
-by Auto_tac;
-qed_spec_mp "rev_is_rev_iff";
-Addsimps [rev_is_rev_iff];
-
-Goal "xs:list(A) ==> \
-\ (xs=Nil --> P) --> (ALL ys:list(A). ALL y:A. xs =ys@[y] -->P)-->P";
-by (etac list_append_induct 1);
-by Auto_tac;
-qed_spec_mp "rev_list_elim_aux";
-
-bind_thm("rev_list_elim", impI RS ballI RS ballI RSN(3, rev_list_elim_aux));
-
-(** more theorems about drop **)
-Goal "n:nat ==> ALL xs:list(A). length(drop(n, xs)) = length(xs) #- n";
-by (etac nat_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (etac list.elim 2);
-by Auto_tac;
-qed_spec_mp "length_drop";
-Addsimps [length_drop];
-
-Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> drop(n, xs)=Nil";
-by (etac nat_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (etac list.elim 2);
-by Auto_tac;
-qed_spec_mp "drop_all";
-Addsimps [drop_all];
-
-(** take **)
-
-Goalw [take_def]
- "xs:list(A) ==> take(0, xs) = Nil";
-by (etac list.induct 1);
-by Auto_tac;
-qed "take_0";
-Addsimps [take_0];
-
-Goalw [take_def]
-"n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))";
-by (Asm_simp_tac 1);
-qed "take_succ_Cons";
-Addsimps [take_succ_Cons];
-
-(* Needed for proving take_all *)
-Goalw [take_def]
- "n:nat ==> take(n, Nil) = Nil";
-by Auto_tac;
-qed "take_Nil";
-Addsimps [take_Nil];
-
-Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> take(n, xs) = xs";
-by (etac nat_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (etac list.elim 2);
-by Auto_tac;
-qed_spec_mp "take_all";
-Addsimps [take_all];
-
-Goal "xs:list(A) ==> ALL n:nat. take(n, xs):list(A)";
-by (etac list.induct 1);
-by (Clarify_tac 2);
-by (etac natE 2);
-by Auto_tac;
-qed_spec_mp "take_type";
-
-Goal "xs:list(A) ==> \
-\ ALL ys:list(A). ALL n:nat. take(n, xs @ ys) = \
-\ take(n, xs) @ take(n #- length(xs), ys)";
-by (etac list.induct 1);
-by (Clarify_tac 2);
-by (etac natE 2);
-by Auto_tac;
-qed_spec_mp "take_append";
-Addsimps [take_append];
-
-(** nth **)
-
-Goalw [nth_def] "nth(0, Cons(a, l))= a";
-by Auto_tac;
-qed "nth_0";
-AddIffs [nth_0];
-
-Goalw [nth_def]
- "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)";
-by (Asm_simp_tac 1);
-qed "nth_Cons";
-Addsimps [nth_Cons];
-
-Goal "xs:list(A) ==> ALL n:nat. n < length(xs) --> nth(n, xs):A";
-by (etac list.induct 1);
-by (ALLGOALS(Clarify_tac));
-by (etac natE 2);
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "nth_type";
-
-Goal
-"xs:list(A) ==> ALL n:nat. \
-\ nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) \
-\ else nth(n #- length(xs),ys))";
-by (induct_tac "xs" 1);
-by (Clarify_tac 2);
-by (etac natE 2);
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "nth_append";
-
-(* Other theorems about lists *)
-
-Goal "xs:list(A) ==> (xs~=Nil) <-> (EX y:A. EX ys:list(A). xs=Cons(y,ys))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "neq_Nil_iff";
-
-Goalw [Ball_def]
- "k:nat ==> \
-\ ALL xs:list(A). (ALL ys:list(A). k le length(xs) --> k le length(ys) --> \
-\ (ALL i:nat. i < k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))";
-by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps
- [lt_succ_eq_0_disj, all_conj_distrib])));
-by (Clarify_tac 1);
-(*Both lists must be non-empty*)
-by (case_tac "xa=Nil" 1);
-by (case_tac "xb=Nil" 2);
-by (Clarify_tac 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
-by (Clarify_tac 1);
-(*prenexing's needed, not miniscoping*)
-by (Asm_simp_tac 1);
-by (rtac conjI 1);
-by (Force_tac 1);
-by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [iff_sym])
- delsimps (all_simps))));
-by (dres_inst_tac [("x", "ys"), ("x1", "ysa")] (spec RS spec) 1);
-by Auto_tac;
-qed_spec_mp "nth_take_lemma";
-
-Goal "[| xs:list(A); ys:list(A); length(xs) = length(ys); \
-\ ALL i:nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |] \
-\ ==> xs = ys";
-by (subgoal_tac "length(xs) le length(ys)" 1);
-by (forw_inst_tac [("ys", "ys")] (rotate_prems 1 nth_take_lemma) 1);
-by (ALLGOALS(Asm_simp_tac));
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all])));
-qed_spec_mp "nth_equalityI";
-
-(*The famous take-lemma*)
-
-Goal "[| xs:list(A); ys:list(A); (ALL i:nat. take(i, xs) = take(i,ys)) |] ==> xs = ys";
-by (case_tac "length(xs) le length(ys)" 1);
-by (dres_inst_tac [("x", "length(ys)")] bspec 1);
-by (dtac not_lt_imp_le 3);
-by (subgoal_tac "length(ys) le length(xs)" 5);
-by (res_inst_tac [("j", "succ(length(ys))")] le_trans 6);
-by (rtac leI 6);
-by (dres_inst_tac [("x", "length(xs)")] bspec 5);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [length_type,take_all])));
-qed_spec_mp "take_equalityI";
-
-(** More on lists **)
-
-Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
-\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
-by (induct_tac "n" 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (etac list.elim 1);
-by Auto_tac;
-qed_spec_mp "nth_drop";
-
-
-
-
--- a/src/ZF/UNITY/ListPlus.thy Mon May 26 18:36:15 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title: ZF/UNITY/ListPlus.thy
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-More about lists
-
-*)
-
-ListPlus = NatPlus +
-
-constdefs
-(* Function `take' returns the first n elements of a list *)
- take :: [i,i]=>i
- "take(n, as) == list_rec(lam n:nat. [],
- %a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
-
-(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
-
- nth :: [i, i]=>i
- "nth(n, as) == list_rec(lam n:nat. 0,
- %a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n"
-
-end
\ No newline at end of file
--- a/src/ZF/UNITY/Mutex.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Mutex.ML Tue May 27 11:39:03 2003 +0200
@@ -13,41 +13,44 @@
(** Variables' types **)
-AddIffs [p_type, u_type, v_type, m_type, n_type];
+Addsimps [p_type, u_type, v_type, m_type, n_type];
-Goal "!!s. s:state ==> s`u:bool";
-by (dres_inst_tac [("a", "u"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==>s`u:bool";
+by (dres_inst_tac [("a", "u")] apply_type 1);
by Auto_tac;
-qed "u_apply_type";
+qed "u_value_type";
-Goal "!!s. s:state ==> s`v:bool";
-by (dres_inst_tac [("a", "v"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==> s`v:bool";
+by (dres_inst_tac [("a", "v")] apply_type 1);
by Auto_tac;
-qed "v_apply_type";
+qed "v_value_type";
-Goal "!!s. s:state ==> s`p:bool";
-by (dres_inst_tac [("a", "p"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==> s`p:bool";
+by (dres_inst_tac [("a", "p")] apply_type 1);
by Auto_tac;
-qed "p_apply_type";
+qed "p_value_type";
-Goal "!!s. s:state ==> s`m:int";
-by (dres_inst_tac [("a", "m"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==> s`m:int";
+by (dres_inst_tac [("a", "m")] apply_type 1);
by Auto_tac;
-qed "m_apply_type";
+qed "m_value_type";
-Goal "!!s. s:state ==> s`n:int";
-by (dres_inst_tac [("a", "n"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==>s`n:int";
+by (dres_inst_tac [("a", "n")] apply_type 1);
by Auto_tac;
-qed "n_apply_type";
-Addsimps [p_apply_type, u_apply_type, v_apply_type,
- m_apply_type, n_apply_type];
+qed "n_value_type";
+Addsimps [p_value_type, u_value_type, v_value_type,
+ m_value_type, n_value_type];
+AddTCs [p_value_type, u_value_type, v_value_type,
+ m_value_type, n_value_type];
(** Mutex is a program **)
Goalw [Mutex_def] "Mutex:program";
by Auto_tac;
qed "Mutex_in_program";
-AddIffs [Mutex_in_program];
+Addsimps [Mutex_in_program];
+AddTCs [Mutex_in_program];
Addsimps [Mutex_def RS def_prg_Init];
program_defs_ref := [Mutex_def];
@@ -61,11 +64,6 @@
Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
-(** In case one wants to be sure that the initial state is not empty **)
-Goal "some(u:=0,v:=0, m:= #0,n:= #0):Init(Mutex)";
-by (auto_tac (claset() addSIs [update_type2], simpset()));
-qed "Mutex_Init_not_empty";
-
Goal "Mutex : Always(IU)";
by (always_tac 1);
by Auto_tac;
@@ -75,7 +73,6 @@
by (always_tac 1);
qed "IV";
-
(*The safety property: mutual exclusion*)
Goal "Mutex : Always({s:state. ~(s`m = #3 & s`n = #3)})";
by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
@@ -93,7 +90,7 @@
Goal "Mutex : Always(bad_IU)";
by (always_tac 1);
by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless]));
-by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset(), simpset() addsimps [bool_def]));
by (subgoal_tac "#1 $<= #3" 1);
by (dres_inst_tac [("x", "#1"), ("y", "#3")] zle_trans 1);
by Auto_tac;
@@ -134,7 +131,7 @@
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
by Auto_tac;
-by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
val U_lemma2 = result();
Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`p =1}";
@@ -156,7 +153,7 @@
Goal "Mutex : {s:state. #1 $<= s`m & s`m $<= #3} LeadsTo {s:state. s`p=1}";
-by (simp_tac (simpset() addsimps [m_apply_type RS eq_123, Collect_disj_eq,
+by (simp_tac (simpset() addsimps [m_value_type RS eq_123, Collect_disj_eq,
LeadsTo_Un_distrib,
U_lemma1, U_lemma2, U_F3] ) 1);
val U_lemma123 = result();
@@ -178,7 +175,6 @@
Goal "Mutex : {s:state. s`n=#1} LeadsTo {s:state. s`p = not(s`u) & s`n = #2}";
by (ensures_tac "V1" 1);
-by (auto_tac (claset() addIs [not_type], simpset()));
qed "V_F1";
Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}";
@@ -192,13 +188,12 @@
by (ensures_tac "V3" 1);
qed "V_F3";
-
Goal "Mutex : {s:state. s`n = #2} LeadsTo {s:state. s`p=0}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
by Auto_tac;
-by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
val V_lemma2 = result();
Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`p = 0}";
@@ -208,11 +203,10 @@
Goal "Mutex : {s:state. #1 $<= s`n & s`n $<= #3} LeadsTo {s:state. s`p = 0}";
by (simp_tac (simpset() addsimps
- [n_apply_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
+ [n_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
V_lemma1, V_lemma2, V_F3] ) 1);
val V_lemma123 = result();
-
(*Misra's F4*)
Goal "Mutex : {s:state. s`v = 1} LeadsTo {s:state. s`p = 0}";
by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
@@ -231,7 +225,7 @@
by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
by Auto_tac;
-by (auto_tac (claset() addSDs [v_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [v_value_type], simpset() addsimps [bool_def]));
qed "m1_Leadsto_3";
@@ -245,5 +239,5 @@
by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
by Auto_tac;
-by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [u_value_type], simpset() addsimps [bool_def]));
qed "n1_Leadsto_3";
--- a/src/ZF/UNITY/Mutex.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Mutex.thy Tue May 27 11:39:03 2003 +0200
@@ -14,18 +14,18 @@
p, m, n, u, v :: i
translations
- "p" == "Var([])"
- "m" == "Var([0])"
- "n" == "Var([1])"
- "u" == "Var([1,0])"
- "v" == "Var([1,1])"
+ "p" == "Var([0])"
+ "m" == "Var([1])"
+ "n" == "Var([0,0])"
+ "u" == "Var([0,1])"
+ "v" == "Var([1,0])"
rules (** Type declarations **)
- p_type "type_of(p)=bool"
- m_type "type_of(m)=int"
- n_type "type_of(n)=int"
- u_type "type_of(u)=bool"
- v_type "type_of(v)=bool"
+ p_type "type_of(p)=bool & default_val(p)=0"
+ m_type "type_of(m)=int & default_val(m)=#0"
+ n_type "type_of(n)=int & default_val(n)=#0"
+ u_type "type_of(u)=bool & default_val(u)=0"
+ v_type "type_of(v)=bool & default_val(v)=0"
constdefs
(** The program for process U **)
@@ -64,7 +64,7 @@
Mutex :: i
"Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
- {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))"
+ {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))"
(** The correct invariants **)
--- a/src/ZF/UNITY/NatPlus.ML Mon May 26 18:36:15 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(* Title: ZF/UNITY/NatPlus.ML
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-More theorems on naturals
-
-*)
-
-Goal "[| m:nat; n:nat |] \
-\ ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "lt_succ_eq_0_disj";
-
-(***** HAVE BEEN MOVED TO ZF BY LCP
-Goal "[| m:nat; n:nat |] ==> m #- n = 0 <-> m le n";
-by (auto_tac (claset(), simpset() addsimps [le_iff, diff_self_eq_0]));
-by (force_tac (claset(), simpset() addsimps [less_iff_succ_add ]) 2);
-by (res_inst_tac [("Pa", "False")] swap 1);
-by (ALLGOALS(asm_full_simp_tac (simpset()
- addsimps [not_lt_iff_le, le_iff])));
-by (auto_tac (claset(), simpset() addsimps [zero_less_diff RS iff_sym]));
-qed "diff_is_0_iff2";
-
-
-Goal "m #- n = 0 <-> natify(m) le natify(n)";
-by (asm_simp_tac (simpset() addsimps [diff_is_0_iff2 RS iff_sym]) 1);
-qed "diff_is_0_iff";
-
-Goal "n:nat ==> natify(n)=0 <-> n=0";
-by (Asm_simp_tac 1);
-qed "natify_of_nat_is_0_iff";
-Addsimps [natify_of_nat_is_0_iff];
-
-Goal "n:nat ==> 0 = natify(n) <-> n=0";
-by Auto_tac;
-qed "natify_of_nat_is_0_iff2";
-Addsimps [natify_of_nat_is_0_iff2];
-
-Goal "[| a:nat; b:nat |] ==> \
-\ (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))";
-by (case_tac "a le b" 1);
-by (asm_full_simp_tac (simpset()
- addsimps [diff_is_0_iff2 RS iff_sym]) 1);
-by Safe_tac;
-by (ALLGOALS(asm_full_simp_tac (simpset()
- addsimps [le_iff, not_lt_iff_le])));
-by Safe_tac;
-by (ALLGOALS(rotate_tac ~1));
-by (ALLGOALS(Asm_full_simp_tac));
-by (dtac lt_not_sym 2);
-by (Asm_full_simp_tac 2);
-by (ALLGOALS(dres_inst_tac [("x", "a #- b")] bspec));
-by (ALLGOALS(Asm_simp_tac));
-by (ALLGOALS(dtac (leI RS add_diff_inverse)));
-by (ALLGOALS(rotate_tac ~1));
-by (ALLGOALS(Asm_full_simp_tac));
-qed "nat_diff_split";
-****)
-
-
-
--- a/src/ZF/UNITY/NatPlus.thy Mon May 26 18:36:15 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(* Title: ZF/UNITY/NatPlus.thy
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-More theorems on naturals
-
-*)
-
-NatPlus = Main +
-
-end
\ No newline at end of file
--- a/src/ZF/UNITY/ROOT.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/ROOT.ML Tue May 27 11:39:03 2003 +0200
@@ -6,6 +6,8 @@
Root file for ZF/UNITY proofs.
*)
+add_path "../Induct"; (*for Multisets*)
+
(*Basic meta-theory*)
time_use_thy "Guar";
--- a/src/ZF/UNITY/State.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/State.ML Tue May 27 11:39:03 2003 +0200
@@ -5,10 +5,11 @@
Formalizes UNITY-program states.
*)
-AddIffs [some_assume];
-
-AddIs var.intrs;
-Addsimps var.intrs;
+Goalw [state_def, st0_def] "st0:state";
+by Auto_tac;
+qed "st0_in_state";
+Addsimps [st0_in_state];
+AddTCs [st0_in_state];
Goalw [st_set_def] "st_set({x:state. P(x)})";
by Auto_tac;
@@ -87,4 +88,27 @@
qed "st_set_subset";
+Goalw [state_def]
+"[| s:state; x:var; y:type_of(x) |] ==> s(x:=y):state";
+by (blast_tac (claset() addIs [update_type]) 1);
+qed "state_update_type";
+Goalw [st_compl_def] "st_set(st_compl(A))";
+by Auto_tac;
+qed "st_set_compl";
+Addsimps [st_set_compl];
+
+Goalw [st_compl_def] "x:st_compl(A) <-> x:state & x ~:A";
+by Auto_tac;
+qed "st_compl_iff";
+Addsimps [st_compl_iff];
+
+Goalw [st_compl_def] "st_compl({s:state. P(s)}) = {s:state. ~P(s)}";
+by Auto_tac;
+qed "st_compl_Collect";
+Addsimps [st_compl_Collect];
+
+
+
+
+
--- a/src/ZF/UNITY/State.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/State.thy Tue May 27 11:39:03 2003 +0200
@@ -14,36 +14,22 @@
consts var::i
datatype var = Var("i:list(nat)")
type_intrs "[list_nat_into_univ]"
-
consts
type_of :: i=>i
- some :: i
- state :: i
- st_set :: i =>o
-translations
- "state" == "Pi(var, type_of)"
-
-defs
- (* To prevent typing conditions (like `A<=state') from
- being used in combination with the rules `constrains_weaken', etc. *)
- st_set_def "st_set(A) == A<=state"
-
-rules
- some_assume "some:state"
+ default_val :: i=>i
-(***
-REMARKS:
- 1. The reason of indexing variables by lists instead of integers is that,
-at the time I was writing this theory, translations like `foo == Var(#1)'
-mysteriously provoke a syntactical error. Such translations are used
-for introducing variable names when specifying programs.
+constdefs
+ state :: i
+ "state == PROD x:var. cons(default_val(x), type_of(x))"
+ st0 :: i
+ "st0 == lam x:var. default_val(x)"
+
+ st_set :: i =>o
+(* To prevent typing conditions like `A<=state' from
+ being used in combination with the rules `constrains_weaken', etc. *)
+ "st_set(A) == A<=state"
- 2. State space `state' is required to be not empty. This requirement
-can be achieved by definition: the space "PROD x:var. type_of(x) Un {0}"
-includes the state `lam x:state. 0'. However, such definition leads to
-complications later during program type-chinking. For example, to prove
-that the assignment `foo:=#1' is well typed, for `foo' an integer
-variable, we would have to show two things: (a) that #1 is an integer
-but also (b) that #1 is different from 0. Hence axiom `some_assume'.
-***)
+ st_compl :: i=>i
+ "st_compl(A) == state-A"
+
end
\ No newline at end of file
--- a/src/ZF/UNITY/SubstAx.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/SubstAx.ML Tue May 27 11:39:03 2003 +0200
@@ -314,14 +314,13 @@
qed "LeadsTo_wf_induct";
-Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``lessThan(m,nat)) Un B); \
+Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B); \
\ A<=f-``nat; F:program |] ==> F : A LeadsTo B";
-by (res_inst_tac [("A1", "nat"), ("I", "nat")] (wf_less_than RS LeadsTo_wf_induct) 1);
+by (res_inst_tac [("A1", "nat"),("f1", "%x. x")]
+ (wf_measure RS LeadsTo_wf_induct) 1);
by (ALLGOALS(asm_full_simp_tac
- (simpset() addsimps [nat_less_than_field])));
-by (Clarify_tac 1);
-by (ALLGOALS(asm_full_simp_tac
- (simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than])));
+ (simpset() addsimps [nat_measure_field])));
+by (asm_simp_tac (simpset() addsimps [ltI, Image_inverse_lessThan, symmetric vimage_def]) 1);
qed "LessThan_induct";
@@ -407,7 +406,7 @@
Clarify_tac 3, dtac swap 3, Force_tac 4,
rtac ReplaceI 3, Force_tac 3, Force_tac 4,
Asm_full_simp_tac 3, rtac conjI 3, Simp_tac 4,
- REPEAT (rtac update_type2 3),
+ REPEAT (rtac state_update_type 3),
constrains_tac 1,
ALLGOALS Clarify_tac,
ALLGOALS (asm_full_simp_tac
--- a/src/ZF/UNITY/UNITY.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/UNITY.ML Tue May 27 11:39:03 2003 +0200
@@ -116,6 +116,8 @@
addsimps [RawInit_type, Init_def]) 1);
qed "Init_type";
+bind_thm("InitD", Init_type RS subsetD);
+
Goalw [st_set_def] "st_set(Init(F))";
by (rtac Init_type 1);
qed "st_set_Init";
@@ -133,6 +135,15 @@
addsimps [RawAllowedActs_type, AllowedActs_def]) 1);
qed "AllowedActs_type";
+(* Needed in Behaviors *)
+Goal "[| act:Acts(F); <s,s'>:act |] ==> s:state & s':state";
+by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
+qed "ActsD";
+
+Goal "[| act:AllowedActs(F); <s,s'>:act |] ==> s:state & s':state";
+by (blast_tac (claset() addDs [AllowedActs_type RS subsetD]) 1);
+qed "AllowedActsD";
+
(** More simplification rules involving state
and Init, Acts, and AllowedActs **)
@@ -575,6 +586,12 @@
qed "stable_state";
AddIffs [stable_state];
+Goalw [unless_def, stable_def]
+ "stable(A)= A unless 0";
+by Auto_tac;
+qed "stable_unless";
+
+
(** Union **)
Goalw [stable_def]
@@ -607,9 +624,8 @@
Goalw [stable_def, constrains_def, st_set_def]
"[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
by Auto_tac;
-by (Blast.depth_tac (claset()) 10 1);
+by (blast_tac (claset() addSDs [bspec]) 1);
qed "stable_constrains_Un";
Goalw [stable_def, constrains_def, st_set_def]
@@ -685,76 +701,6 @@
by Auto_tac;
qed "strongest_rhs_is_strongest";
-(*** increasing ***)
-Goalw [increasing_def] "increasing(A, r, f) <= program";
-by (case_tac "A=0" 1);
-by (etac not_emptyE 2);
-by (Clarify_tac 2);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Inter_iff, Inter_0])));
-by (blast_tac (claset() addDs [stable_type RS subsetD]) 1);
-qed "increasing_type";
-
-Goalw [increasing_def]
- "[| F:increasing(A, r, f); a:A |] ==> F:stable({s:state. <a, f`s>:r})";
-by (Blast_tac 1);
-qed "increasingD";
-
-Goalw [increasing_def]
-"F:increasing(A, r, f) ==> F:program & (EX a. a:A)";
-by (auto_tac (claset() addDs [stable_type RS subsetD],
- simpset() addsimps [INT_iff]));
-qed "increasingD2";
-
-Goalw [increasing_def, stable_def]
- "F:increasing(A, r, lam s:state. c) <-> F:program & (EX a. a:A)";
-by (auto_tac (claset() addDs [constrains_type RS subsetD],
- simpset() addsimps [INT_iff]));
-qed "increasing_constant";
-AddIffs [increasing_constant];
-
-Goalw [increasing_def, stable_def, constrains_def, st_set_def, part_order_def]
-"[| g:mono_map(A,r,A,r); part_order(A, r); f:state->A |] \
-\ ==> increasing(A, r,f) <= increasing(A, r,g O f)";
-by (case_tac "A=0" 1);
-by (Asm_full_simp_tac 1);
-by (etac not_emptyE 1);
-by (Clarify_tac 1);
-by (cut_inst_tac [("F", "xa")] Acts_type 1);
-by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
-by Auto_tac;
-by (rename_tac "xa xc xd act xe xf" 1);
-by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1);
-by (dres_inst_tac [("x", "f`xf")] bspec 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "Acts(?u) <= ?v")] asm_rl 1);
-by (dres_inst_tac [("psi", "?u <= state")] asm_rl 1);
-by (dres_inst_tac [("c", "xe")] subsetD 1);
-by (rtac imageI 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [refl_def, apply_type]) 1);
-by (dres_inst_tac [("x1", "f`xf"), ("x", "f`xe")] (bspec RS bspec) 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type])));
-by (res_inst_tac [("b", "g ` (f ` xf)")] trans_onD 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type])));
-qed "mono_increasing_comp";
-
-(*Holds by the theorem (succ(m) le n) = (m < n) *)
-Goalw [increasing_def]
- "[| F:increasing(nat, {<m,n>:nat*nat. m le n}, f); f:state->nat; k:nat |] \
-\ ==> F: stable({s:state. k < f`s})";
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "succ(k)")] bspec 1);
-by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
-by (subgoal_tac "{x: state . f`x : nat} = state" 1);
-by Auto_tac;
-qed "strict_increasingD";
-
-
(* Used in WFair.thy *)
Goal "A:Pow(Pow(B)) ==> Union(A):Pow(B)";
by Auto_tac;
--- a/src/ZF/UNITY/UNITY.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/UNITY.thy Tue May 27 11:39:03 2003 +0200
@@ -68,19 +68,13 @@
invariant :: i => i
"invariant(A) == initially(A) Int stable(A)"
- (* The `increasing' relation of Charpentier. Increasing's parameters are:
- a state function f, a domain A and an order relation r over the domain A. *)
-
- increasing :: [i,i, i] => i
- "increasing(A, r, f) == INT a:A. stable({s:state. <a, f`s>:r})"
+ (* meta-function composition *)
+ comp :: "[i=>i, i=>i] => (i=>i)" (infixl 65)
+ "f comp g == %x. f(g(x))"
- (* The definition of a partial order in ZF (predicate part_ord in theory Order)
- describes a strict order: irreflexive and transitive.
- However, the order used in association with Charpentier's increasing
- relation is not, hence the definition below: *)
- part_order :: [i, i] => o
- "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
-
+ pg_compl :: "i=>i"
+ "pg_compl(X)== program - X"
+
defs
(* Condition `st_set(A)' makes the definition slightly stronger than the HOL one *)
constrains_def "A co B == {F:program. (ALL act:Acts(F). act``A<=B) & st_set(A)}"
--- a/src/ZF/UNITY/UNITYMisc.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.ML Tue May 27 11:39:03 2003 +0200
@@ -7,53 +7,11 @@
*)
-Goalw [measure_def, less_than_def]
- "less_than(A) = {<x,y>:A*A. x<y}";
-by Auto_tac;
-qed "less_than_equals";
-
-Goalw [less_than_def] "wf(less_than(A))";
-by (rtac wf_measure 1);
-qed "wf_less_than";
-
-Goalw [less_than_def, measure_def]
- "less_than(A)<= A*A";
-by Auto_tac;
-qed "less_than_subset";
-
-Goalw [less_than_def, measure_def]
-"<x,y>:less_than(A) <-> (x:A & y:A & x<y)";
-by Auto_tac;
-qed "less_than_iff";
-
-Goalw [lessThan_def]
-"i:lessThan(k,A) <-> i:A & i<k";
-by Auto_tac;
-qed "lessThan_iff";
-
Goalw [greaterThan_def]
"i:greaterThan(k,A) <-> i:A & k<i";
by Auto_tac;
qed "greaterThan_iff";
-
-(** Needed for WF reasoning in WFair.ML **)
-
-Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)";
-by (rtac equalityI 1);
-by (auto_tac (claset(), simpset() addsimps
- [less_than_iff,greaterThan_iff]));
-qed "Image_less_than";
-
-Goal "k:A ==> less_than(A)-`` {k} = lessThan(k, A)";
-by (rtac equalityI 1);
-by (auto_tac (claset(), simpset() addsimps
- [less_than_iff,lessThan_iff]));
-qed "Image_inverse_less_than";
-
-Addsimps [Image_less_than, Image_inverse_less_than];
-
-
(** Ad-hoc set-theory rules **)
Goal "Union(B) Int A = (UN b:B. b Int A)";
@@ -81,12 +39,6 @@
(** To be moved to Update theory **)
-Goalw [update_def]
- "[| f:Pi(A,B); x:A; y:B(x) |] ==> f(x:=y):Pi(A, B)";
-by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb,
- apply_funtype, lam_type]) 1);
-qed "update_type2";
-
(** Simplication rules for Collect; To be moved elsewhere **)
Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
by Auto_tac;
@@ -107,5 +59,14 @@
by Auto_tac;
qed "Collect_conj_eq";
+Goal "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+Goal "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)";
+by Auto_tac;
+qed "Int_cons_right";
+Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)";
+by Auto_tac;
+qed "Int_succ_right";
--- a/src/ZF/UNITY/UNITYMisc.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.thy Tue May 27 11:39:03 2003 +0200
@@ -10,16 +10,6 @@
UNITYMisc = Main +
constdefs
- less_than :: i=>i
- "less_than(A) == measure(A, %x. x)"
-
- lessThan :: [i, i] => i
- "lessThan(u,A) == {x:A. x<u}"
-
greaterThan :: [i,i]=> i
"greaterThan(u,A) == {x:A. u<x}"
-
- (* Identity relation over a domain A *)
- Identity :: i=>i
- "Identity(A) == {p:A*A. EX x. p=<x,x>}"
end
\ No newline at end of file
--- a/src/ZF/UNITY/Union.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Union.ML Tue May 27 11:39:03 2003 +0200
@@ -103,8 +103,10 @@
qed "Join_commute";
Goal "A Join (B Join C) = B Join (A Join C)";
-by (asm_simp_tac (simpset() addsimps
- Un_ac@Int_ac@[Join_def,Int_Un_distrib2, cons_absorb]) 1);
+by (simp_tac (simpset() addsimps
+ [Join_def,Int_Un_distrib2, cons_absorb]) 1);
+by (simp_tac (simpset() addsimps
+ Un_ac@Int_ac@[Int_Un_distrib2, cons_absorb]) 1);
qed "Join_left_commute";
Goal "(F Join G) Join H = F Join (G Join H)";
@@ -584,7 +586,7 @@
by Auto_tac;
qed "Allowed_eq";
-Goal "[| F == mk_program (init, acts, UN F:X. Acts(F)); X:property; safety_prop(X) |] \
+Goal "[| F == mk_program (init, acts, UN F:X. Acts(F)); safety_prop(X) |] \
\ ==> Allowed(F) = X";
by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1);
qed "def_prg_Allowed";
--- a/src/ZF/UNITY/WFair.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/WFair.ML Tue May 27 11:39:03 2003 +0200
@@ -52,7 +52,7 @@
by (ALLGOALS(Clarify_tac));
by (cut_inst_tac [("F", "x")] Acts_type 1);
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1);
-by Auto_tac;
+by (auto_tac (claset() addIs [st0_in_state], simpset()));
qed "transient_state";
Goalw [transient_def,st_set_def] "state<=B ==> transient(B) = 0";
@@ -61,7 +61,7 @@
by (cut_inst_tac [("F", "x")] Acts_type 1);
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1);
by (subgoal_tac "B=state" 1);
-by Auto_tac;
+by (auto_tac (claset() addIs [st0_in_state], simpset()));
qed "transient_state2";
Goalw [transient_def] "transient(0) = program";
@@ -526,35 +526,44 @@
by Auto_tac;
qed "leadsTo_wf_induct";
-Goalw [field_def] "field(less_than(nat)) = nat";
-by (simp_tac (simpset() addsimps [less_than_equals]) 1);
+Goalw [field_def] "field(measure(nat, %x. x)) = nat";
+by (asm_full_simp_tac (simpset() addsimps [measure_def]) 1) ;
by (rtac equalityI 1);
by (force_tac (claset(), simpset()) 1);
by (Clarify_tac 1);
by (thin_tac "x~:range(?y)" 1);
by (etac nat_induct 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [domain_def])));
-by (res_inst_tac [("x", "<succ(xa),succ(succ(xa))>")] ReplaceI 2);
-by (res_inst_tac [("x", "<0,1>")] ReplaceI 1);
-by (REPEAT(force_tac (claset() addIs [splitI], simpset()) 1));
-qed "nat_less_than_field";
+by (res_inst_tac [("b", "succ(succ(xa))")] domainI 2);
+by (res_inst_tac [("b","succ(0)")] domainI 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "nat_measure_field";
+
+
+Goal "k<A ==> measure(A, %x. x) -`` {k} = k";
+by (rtac equalityI 1);
+by (auto_tac (claset(), simpset() addsimps [measure_def]));
+by (blast_tac (claset() addIs [ltD]) 1);
+by (rtac vimageI 1);
+by (blast_tac (claset() addIs []) 2);
+by (asm_full_simp_tac (simpset() addsimps [lt_Ord, lt_Ord2, Ord_mem_iff_lt]) 1);
+by (blast_tac (claset() addIs [lt_trans]) 1);
+qed "Image_inverse_lessThan";
(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
Goal
"[| A<=f-``nat;\
\ F:program; st_set(A); st_set(B); \
-\ ALL m:nat. F:(A Int f-``{m}) leadsTo ((A Int f-``lessThan(m,nat)) Un B) |] \
+\ ALL m:nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |] \
\ ==> F : A leadsTo B";
-by (res_inst_tac [("A1", "nat")]
- (wf_less_than RS leadsTo_wf_induct) 1);
+by (res_inst_tac [("A1", "nat"),("f1", "%x. x")]
+ (wf_measure RS leadsTo_wf_induct) 1);
by (Clarify_tac 6);
by (ALLGOALS(asm_full_simp_tac
- (simpset() addsimps [nat_less_than_field])));
-by (Clarify_tac 1);
-by (ALLGOALS(asm_full_simp_tac
- (simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than])));
+ (simpset() addsimps [nat_measure_field])));
+by (asm_simp_tac (simpset() addsimps [ltI, Image_inverse_lessThan, symmetric vimage_def]) 1);
qed "lessThan_induct";
+
(*** wlt ****)
(*Misra's property W3*)
--- a/src/ZF/equalities.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/equalities.thy Tue May 27 11:39:03 2003 +0200
@@ -206,6 +206,12 @@
(*Intersection is an AC-operator*)
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute
+lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
+ by blast
+
+lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
+ by blast
+
lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)"
by blast
@@ -258,6 +264,12 @@
(*Union is an AC-operator*)
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
+lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
+ by blast
+
+lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
+ by blast
+
lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)"
by blast
@@ -1217,8 +1229,11 @@
val Int_ac = thms "Int_ac";
val Un_ac = thms "Un_ac";
-
+val Int_absorb1 = thm "Int_absorb1";
+val Int_absorb2 = thm "Int_absorb2";
+val Un_absorb1 = thm "Un_absorb1";
+val Un_absorb2 = thm "Un_absorb2";
*}
-
+
end
--- a/src/ZF/ex/Limit.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/ex/Limit.thy Tue May 27 11:39:03 2003 +0200
@@ -1284,7 +1284,7 @@
lemma e_less_eq:
"m \<in> nat ==> e_less(DD,ee,m,m) = id(set(DD`m))"
-by (simp add: e_less_def diff_self_eq_0)
+by (simp add: e_less_def)
lemma lemma_succ_sub: "succ(m#+n)#-m = succ(natify(n))"
by simp
@@ -1378,9 +1378,7 @@
lemma e_gr_eq:
"m \<in> nat ==> e_gr(DD,ee,m,m) = id(set(DD`m))"
-apply (simp add: e_gr_def)
-apply (simp add: diff_self_eq_0)
-done
+by (simp add: e_gr_def)
lemma e_gr_add:
"[|n \<in> nat; k \<in> nat|]
--- a/src/ZF/func.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/func.thy Tue May 27 11:39:03 2003 +0200
@@ -480,7 +480,7 @@
lemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))"
by (unfold update_def, simp)
-lemma update_type: "[| f: A -> B; x : A; y: B |] ==> f(x:=y) : A -> B"
+lemma update_type: "[| f:Pi(A,B); x : A; y: B(x) |] ==> f(x:=y) : Pi(A, B)"
apply (unfold update_def)
apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
done