--- a/src/HOL/IsaMakefile Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/IsaMakefile Fri Jan 31 20:12:44 2003 +0100
@@ -383,8 +383,7 @@
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
- UNITY/Extend.thy UNITY/FP.thy \
- UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
+ UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \
UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \
UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
@@ -394,7 +393,7 @@
UNITY/Simple/Network.thy\
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
- UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \
+ UNITY/Comp/AllocBase.thy \
UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
--- a/src/HOL/UNITY/Comp.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy Fri Jan 31 20:12:44 2003 +0100
@@ -13,6 +13,8 @@
*)
+header{*Composition: Basic Primitives*}
+
theory Comp = Union:
instance program :: (type) ord ..
@@ -42,7 +44,7 @@
"funPair f g == %x. (f x, g x)"
-(*** component <= ***)
+subsection{*The component relation*}
lemma componentI:
"H <= F | H <= G ==> H <= (F Join G)"
apply (unfold component_def, auto)
@@ -76,8 +78,7 @@
lemma component_Join2: "G <= (F Join G)"
apply (unfold component_def)
-apply (simp (no_asm) add: Join_commute)
-apply blast
+apply (simp add: Join_commute, blast)
done
lemma Join_absorb1: "F<=G ==> F Join G = G"
@@ -87,9 +88,7 @@
by (auto simp add: Join_ac component_def)
lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
-apply (simp (no_asm) add: component_eq_subset)
-apply blast
-done
+by (simp add: component_eq_subset, blast)
lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
apply (unfold component_def)
@@ -107,9 +106,7 @@
done
lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
-apply (simp (no_asm) add: component_eq_subset)
-apply blast
-done
+by (simp add: component_eq_subset, blast)
lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
by (auto simp add: constrains_def component_eq_subset)
@@ -118,7 +115,7 @@
lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
-(*** preserves ***)
+subsection{*The preserves property*}
lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
by (unfold preserves_def, blast)
@@ -135,8 +132,7 @@
lemma JN_preserves [iff]:
"(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
-apply (simp (no_asm) add: JN_stable preserves_def)
-apply blast
+apply (simp add: JN_stable preserves_def, blast)
done
lemma SKIP_preserves [iff]: "SKIP : preserves v"
@@ -153,16 +149,13 @@
lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
-apply (simp (no_asm) add: funPair_def o_def)
-done
+by (simp add: funPair_def o_def)
lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
-apply (simp (no_asm) add: funPair_def o_def)
-done
+by (simp add: funPair_def o_def)
lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
-apply (simp (no_asm) add: funPair_def o_def)
-done
+by (simp add: funPair_def o_def)
lemma subset_preserves_o: "preserves v <= preserves (w o v)"
by (force simp add: preserves_def stable_def constrains_def)
@@ -244,18 +237,13 @@
(** localize **)
lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
-apply (unfold localize_def)
-apply (simp (no_asm))
-done
+by (simp add: localize_def)
lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
-apply (unfold localize_def)
-apply (simp (no_asm))
-done
+by (simp add: localize_def)
lemma localize_AllowedActs_eq [simp]:
"AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
-apply (unfold localize_def, auto)
-done
+by (unfold localize_def, auto)
end
--- a/src/HOL/UNITY/Comp/AllocBase.ML Thu Jan 30 18:08:09 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-(* Title: HOL/UNITY/AllocBase.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Basis declarations for Chandy and Charpentier's Allocator
-*)
-
-Goal "!!f :: nat=>nat. \
-\ (ALL i. i<n --> f i <= g i) --> \
-\ setsum f (lessThan n) <= setsum g (lessThan n)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
-by (dres_inst_tac [("x","n")] spec 1);
-by (arith_tac 1);
-qed_spec_mp "setsum_fun_mono";
-
-Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
-by (induct_tac "ys" 1);
-by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
-qed_spec_mp "tokens_mono_prefix";
-
-Goalw [mono_def] "mono tokens";
-by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
-qed "mono_tokens";
-
-
-(** bag_of **)
-
-Goal "bag_of (l@l') = bag_of l + bag_of l'";
-by (induct_tac "l" 1);
- by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
-by (Simp_tac 1);
-qed "bag_of_append";
-Addsimps [bag_of_append];
-
-Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
-by (rtac monoI 1);
-by (rewtac prefix_def);
-by (etac genPrefix.induct 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1);
-by (etac order_trans 1);
-by (rtac (thm "union_upper1") 1);
-qed "mono_bag_of";
-
-(** setsum **)
-
-Addcongs [setsum_cong];
-
-Goal "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = \
-\ (\\<Sum>i: A Int lessThan k. {#f i#})";
-by (rtac setsum_cong 1);
-by Auto_tac;
-qed "bag_of_sublist_lemma";
-
-Goal "bag_of (sublist l A) = \
-\ (\\<Sum>i: A Int lessThan (length l). {# l!i #})";
-by (res_inst_tac [("xs","l")] rev_induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc,
- nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
-qed "bag_of_sublist";
-
-
-Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
-\ bag_of (sublist l A) + bag_of (sublist l B)";
-by (subgoal_tac "A Int B Int {..length l(} = \
-\ (A Int {..length l(}) Int (B Int {..length l(})" 1);
-by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2,
- setsum_Un_Int]) 1);
-by (Blast_tac 1);
-qed "bag_of_sublist_Un_Int";
-
-Goal "A Int B = {} \
-\ ==> bag_of (sublist l (A Un B)) = \
-\ bag_of (sublist l A) + bag_of (sublist l B)";
-by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
-qed "bag_of_sublist_Un_disjoint";
-
-Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
-\ ==> bag_of (sublist l (UNION I A)) = \
-\ (\\<Sum>i:I. bag_of (sublist l (A i)))";
-by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
- addsimps [bag_of_sublist]) 1);
-by (stac setsum_UN_disjoint 1);
-by Auto_tac;
-qed_spec_mp "bag_of_sublist_UN_disjoint";
--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Jan 31 20:12:44 2003 +0100
@@ -3,29 +3,124 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Common declarations for Chandy and Charpentier's Allocator
*)
-AllocBase = UNITY_Main +
+header{*Common Declarations for Chandy and Charpentier's Allocator*}
+
+theory AllocBase = UNITY_Main:
consts
NbT :: nat (*Number of tokens in system*)
Nclients :: nat (*Number of clients*)
-rules
- NbT_pos "0 < NbT"
+axioms
+ NbT_pos: "0 < NbT"
(*This function merely sums the elements of a list*)
-consts tokens :: nat list => nat
+consts tokens :: "nat list => nat"
primrec
"tokens [] = 0"
"tokens (x#xs) = x + tokens xs"
consts
- bag_of :: 'a list => 'a multiset
+ bag_of :: "'a list => 'a multiset"
primrec
"bag_of [] = {#}"
"bag_of (x#xs) = {#x#} + bag_of xs"
+lemma setsum_fun_mono [rule_format]:
+ "!!f :: nat=>nat.
+ (ALL i. i<n --> f i <= g i) -->
+ setsum f (lessThan n) <= setsum g (lessThan n)"
+apply (induct_tac "n")
+apply (auto simp add: lessThan_Suc)
+apply (drule_tac x = n in spec, arith)
+done
+
+lemma tokens_mono_prefix [rule_format]:
+ "ALL xs. xs <= ys --> tokens xs <= tokens ys"
+apply (induct_tac "ys")
+apply (auto simp add: prefix_Cons)
+done
+
+lemma mono_tokens: "mono tokens"
+apply (unfold mono_def)
+apply (blast intro: tokens_mono_prefix)
+done
+
+
+(** bag_of **)
+
+lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
+apply (induct_tac "l", simp)
+ apply (simp add: plus_ac0)
+done
+
+lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
+apply (rule monoI)
+apply (unfold prefix_def)
+apply (erule genPrefix.induct, auto)
+apply (simp add: union_le_mono)
+apply (erule order_trans)
+apply (rule union_upper1)
+done
+
+(** setsum **)
+
+declare setsum_cong [cong]
+
+lemma bag_of_sublist_lemma:
+ "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =
+ (\<Sum>i: A Int lessThan k. {#f i#})"
+apply (rule setsum_cong, auto)
+done
+
+lemma bag_of_sublist:
+ "bag_of (sublist l A) =
+ (\<Sum>i: A Int lessThan (length l). {# l!i #})"
+apply (rule_tac xs = l in rev_induct, simp)
+apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append
+ bag_of_sublist_lemma plus_ac0)
+done
+
+
+lemma bag_of_sublist_Un_Int:
+ "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =
+ bag_of (sublist l A) + bag_of (sublist l B)"
+apply (subgoal_tac "A Int B Int {..length l (} = (A Int {..length l (}) Int (B Int {..length l (}) ")
+apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
+done
+
+lemma bag_of_sublist_Un_disjoint:
+ "A Int B = {}
+ ==> bag_of (sublist l (A Un B)) =
+ bag_of (sublist l A) + bag_of (sublist l B)"
+apply (simp add: bag_of_sublist_Un_Int [symmetric])
+done
+
+lemma bag_of_sublist_UN_disjoint [rule_format]:
+ "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]
+ ==> bag_of (sublist l (UNION I A)) =
+ (\<Sum>i:I. bag_of (sublist l (A i)))"
+apply (simp del: UN_simps
+ add: UN_simps [symmetric] add: bag_of_sublist)
+apply (subst setsum_UN_disjoint, auto)
+done
+
+ML
+{*
+val NbT_pos = thm "NbT_pos";
+val setsum_fun_mono = thm "setsum_fun_mono";
+val tokens_mono_prefix = thm "tokens_mono_prefix";
+val mono_tokens = thm "mono_tokens";
+val bag_of_append = thm "bag_of_append";
+val mono_bag_of = thm "mono_bag_of";
+val bag_of_sublist_lemma = thm "bag_of_sublist_lemma";
+val bag_of_sublist = thm "bag_of_sublist";
+val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int";
+val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint";
+val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint";
+*}
+
end
--- a/src/HOL/UNITY/Constrains.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Constrains.thy Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,8 @@
Weak safety relations: restricted to the set of reachable states.
*)
+header{*Weak Safety*}
+
theory Constrains = UNITY:
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
@@ -50,7 +52,7 @@
"Increasing f == INT z. Stable {s. z <= f s}"
-(*** traces and reachable ***)
+subsection{*traces and reachable*}
lemma reachable_equiv_traces:
"reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
@@ -82,7 +84,7 @@
done
-(*** Co ***)
+subsection{*Co*}
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
lemmas constrains_reachable_Int =
@@ -184,7 +186,7 @@
by (simp add: Constrains_eq_constrains constrains_def, blast)
-(*** Stable ***)
+subsection{*Stable*}
(*Useful because there's no Stable_weaken. [Tanja Vos]*)
lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
@@ -238,7 +240,7 @@
-(*** Increasing ***)
+subsection{*Increasing*}
lemma IncreasingD:
"F : Increasing f ==> F : Stable {s. x <= f s}"
@@ -265,14 +267,14 @@
increasing_constant [THEN increasing_imp_Increasing, standard, iff]
-(*** The Elimination Theorem. The "free" m has become universally quantified!
- Should the premise be !!m instead of ALL m ? Would make it harder to use
- in forward proof. ***)
+subsection{*The Elimination Theorem*}
+
+(*The "free" m has become universally quantified! Should the premise be !!m
+instead of ALL m ? Would make it harder to use in forward proof.*)
lemma Elimination:
"[| ALL m. F : {s. s x = m} Co (B m) |]
==> F : {s. s x : M} Co (UN m:M. B m)"
-
by (unfold Constrains_def constrains_def, blast)
(*As above, but for the trivial case of a one-variable state, in which the
@@ -282,7 +284,7 @@
by (unfold Constrains_def constrains_def, blast)
-(*** Specialized laws for handling Always ***)
+subsection{*Specialized laws for handling Always*}
(** Natural deduction rules for "Always A" **)
@@ -340,7 +342,7 @@
by (auto simp add: Always_eq_includes_reachable)
-(*** "Co" rules involving Always ***)
+subsection{*"Co" rules involving Always*}
lemma Always_Constrains_pre:
"F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
--- a/src/HOL/UNITY/Detects.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,8 @@
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)
+header{*The Detects Relation*}
+
theory Detects = FP + SubstAx:
consts
--- a/src/HOL/UNITY/ELT.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/ELT.thy Fri Jan 31 20:12:44 2003 +0100
@@ -22,6 +22,8 @@
monos Pow_mono
*)
+header{*Progress Under Allowable Sets*}
+
theory ELT = Project:
consts
@@ -91,8 +93,7 @@
(*preserving v preserves properties given by v*)
lemma preserves_givenBy_imp_stable:
"[| F : preserves v; D : givenBy v |] ==> F : stable D"
-apply (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
-done
+by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v"
apply (simp (no_asm) add: givenBy_eq_Collect)
@@ -212,7 +213,7 @@
apply (blast intro: subset_imp_leadsETo leadsETo_Trans)
done
-lemma leadsETo_weaken_L [rule_format (no_asm)]:
+lemma leadsETo_weaken_L [rule_format]:
"[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
apply (blast intro: leadsETo_Trans subset_imp_leadsETo)
done
@@ -458,13 +459,13 @@
lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
-lemma LeadsETo_weaken_R [rule_format (no_asm)]:
+lemma LeadsETo_weaken_R [rule_format]:
"[| F : A LeadsTo[CC] A'; A' <= B' |] ==> F : A LeadsTo[CC] B'"
apply (simp (no_asm_use) add: LeadsETo_def)
apply (blast intro: leadsETo_weaken_R)
done
-lemma LeadsETo_weaken_L [rule_format (no_asm)]:
+lemma LeadsETo_weaken_L [rule_format]:
"[| F : A LeadsTo[CC] A'; B <= A |] ==> F : B LeadsTo[CC] A'"
apply (simp (no_asm_use) add: LeadsETo_def)
apply (blast intro: leadsETo_weaken_L)
--- a/src/HOL/UNITY/Extend.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy Fri Jan 31 20:12:44 2003 +0100
@@ -3,11 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Extending of state sets
+Extending of state setsExtending of state sets
function f (forget) maps the extended state to the original state
function g (forgotten) maps the extended state to the "extending part"
*)
+header{*Extending State Sets*}
+
theory Extend = Guar:
constdefs
@@ -60,7 +62,8 @@
(** These we prove OUTSIDE the locale. **)
-(*** Restrict [MOVE to Relation.thy?] ***)
+subsection{*Restrict*}
+(*MOVE to Relation.thy?*)
lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)"
by (unfold Restrict_def, blast)
@@ -130,7 +133,7 @@
done
-(*** Trivial properties of f, g, h ***)
+subsection{*Trivial properties of f, g, h*}
lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x"
by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
@@ -163,7 +166,7 @@
-(*** extend_set: basic properties ***)
+subsection{*@{term extend_set}: basic properties*}
lemma project_set_iff [iff]:
"(x : project_set h C) = (EX y. h(x,y) : C)"
@@ -210,7 +213,7 @@
apply (auto simp add: split_extended_all)
done
-(*** project_set: basic properties ***)
+subsection{*@{term project_set}: basic properties*}
(*project_set is simply image!*)
lemma (in Extend) project_set_eq: "project_set h C = f ` C"
@@ -221,7 +224,7 @@
by (auto simp add: split_extended_all)
-(*** More laws ***)
+subsection{*More laws*}
(*Because A and B could differ on the "other" part of the state,
cannot generalize to
@@ -265,7 +268,7 @@
by (unfold extend_set_def, auto)
-(*** extend_act ***)
+subsection{*@{term extend_act}*}
(*Can't strengthen it to
((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
@@ -335,9 +338,9 @@
-(**** extend ****)
+subsection{*extend ****)
-(*** Basic properties ***)
+(*** Basic properties*}
lemma Init_extend [simp]:
"Init (extend h F) = extend_set h (Init F)"
@@ -451,7 +454,7 @@
by (simp add: component_eq_subset, blast)
-(*** Safety: co, stable ***)
+subsection{*Safety: co, stable*}
lemma (in Extend) extend_constrains:
"(extend h F : (extend_set h A) co (extend_set h B)) =
@@ -477,7 +480,7 @@
by (simp add: stable_def extend_constrains_project_set)
-(*** Weak safety primitives: Co, Stable ***)
+subsection{*Weak safety primitives: Co, Stable*}
lemma (in Extend) reachable_extend_f:
"p : reachable (extend h F) ==> f p : reachable F"
@@ -570,7 +573,7 @@
by (simp add: stable_def project_constrains_project_set)
-(*** Progress: transient, ensures ***)
+subsection{*Progress: transient, ensures*}
lemma (in Extend) extend_transient:
"(extend h F : transient (extend_set h A)) = (F : transient A)"
@@ -591,7 +594,7 @@
apply (simp add: leadsTo_UN extend_set_Union)
done
-(*** Proving the converse takes some doing! ***)
+subsection{*Proving the converse takes some doing!*}
lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)"
by (simp (no_asm) add: slice_def)
@@ -631,7 +634,7 @@
apply (blast intro: leadsTo_UN)
done
-lemma (in Extend) extend_leadsTo_slice [rule_format (no_asm)]:
+lemma (in Extend) extend_leadsTo_slice [rule_format]:
"extend h F : AU leadsTo BU
==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"
apply (erule leadsTo_induct)
@@ -656,7 +659,7 @@
extend_set_Int_distrib [symmetric])
-(*** preserves ***)
+subsection{*preserves*}
lemma (in Extend) project_preserves_I:
"G : preserves (v o f) ==> project h C G : preserves v"
@@ -677,7 +680,7 @@
constrains_def g_def)
-(*** Guarantees ***)
+subsection{*Guarantees*}
lemma (in Extend) project_extend_Join:
"project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)"
--- a/src/HOL/UNITY/FP.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/FP.thy Fri Jan 31 20:12:44 2003 +0100
@@ -3,11 +3,11 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Fixed Point of a Program
-
From Misra, "A Logic for Concurrent Programming", 1994
*)
+header{*Fixed Point of a Program*}
+
theory FP = UNITY:
constdefs
--- a/src/HOL/UNITY/Follows.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Follows.thy Fri Jan 31 20:12:44 2003 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
+*)
-The "Follows" relation of Charpentier and Sivilotte
-*)
+header{*The Follows Relation of Charpentier and Sivilotte*}
theory Follows = SubstAx + ListOrder + Multiset:
@@ -35,9 +35,8 @@
apply (blast intro: monoD order_trans)+
done
-lemma Follows_constant: "F : (%s. c) Fols (%s. c)"
+lemma Follows_constant [iff]: "F : (%s. c) Fols (%s. c)"
by (unfold Follows_def, auto)
-declare Follows_constant [iff]
lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)"
apply (unfold Follows_def, clarify)
@@ -60,28 +59,23 @@
done
-(** Destructiom rules **)
+subsection{*Destruction rules*}
-lemma Follows_Increasing1:
- "F : f Fols g ==> F : Increasing f"
-
+lemma Follows_Increasing1: "F : f Fols g ==> F : Increasing f"
apply (unfold Follows_def, blast)
done
-lemma Follows_Increasing2:
- "F : f Fols g ==> F : Increasing g"
+lemma Follows_Increasing2: "F : f Fols g ==> F : Increasing g"
apply (unfold Follows_def, blast)
done
-lemma Follows_Bounded:
- "F : f Fols g ==> F : Always {s. f s <= g s}"
+lemma Follows_Bounded: "F : f Fols g ==> F : Always {s. f s <= g s}"
apply (unfold Follows_def, blast)
done
lemma Follows_LeadsTo:
"F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"
-apply (unfold Follows_def, blast)
-done
+by (unfold Follows_def, blast)
lemma Follows_LeadsTo_pfixLe:
"F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
@@ -107,7 +101,8 @@
apply (unfold Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" in Always_Constrains_weaken, auto)
+apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}"
+ in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
done
@@ -116,13 +111,14 @@
"[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"
apply (unfold Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" in Always_Constrains_weaken, auto)
+apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}"
+ in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
done
-(** Union properties (with the subset ordering) **)
+subsection{*Union properties (with the subset ordering)*}
(*Can replace "Un" by any sup. But existing max only works for linorders.*)
lemma increasing_Un:
@@ -137,7 +133,8 @@
lemma Increasing_Un:
"[| F : Increasing f; F: Increasing g |]
==> F : Increasing (%s. (f s) Un (g s))"
-apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto)
+apply (auto simp add: Increasing_def Stable_def Constrains_def
+ stable_def constrains_def)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
apply (blast dest!: bspec)
@@ -147,8 +144,7 @@
lemma Always_Un:
"[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]
==> F : Always {s. f' s Un g' s <= f s Un g s}"
-apply (simp add: Always_eq_includes_reachable, blast)
-done
+by (simp add: Always_eq_includes_reachable, blast)
(*Lemma to re-use the argument that one variable increases (progress)
while the other variable doesn't decrease (safety)*)
@@ -164,8 +160,7 @@
apply (rule PSP_Stable)
apply (erule_tac x = "f s" in spec)
apply (erule Stable_Int, assumption)
-apply blast
-apply blast
+apply blast+
done
lemma Follows_Un:
@@ -180,12 +175,11 @@
done
-(** Multiset union properties (with the multiset ordering) **)
+subsection{*Multiset union properties (with the multiset ordering)*}
lemma increasing_union:
"[| F : increasing f; F: increasing g |]
==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))"
-
apply (unfold increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
@@ -196,7 +190,8 @@
lemma Increasing_union:
"[| F : Increasing f; F: Increasing g |]
==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
-apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto)
+apply (auto simp add: Increasing_def Stable_def Constrains_def
+ stable_def constrains_def)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
apply (drule bspec, assumption)
--- a/src/HOL/UNITY/GenPrefix.ML Thu Jan 30 18:08:09 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,424 +0,0 @@
-(* Title: HOL/UNITY/GenPrefix.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Charpentier's Generalized Prefix Relation
- (xs,ys) : genPrefix r
- if ys = xs' @ zs where length xs = length xs'
- and corresponding elements of xs, xs' are pairwise related by r
-
-Based on Lex/Prefix
-*)
-
-(*** preliminary lemmas ***)
-
-Goal "([], xs) : genPrefix r";
-by (cut_facts_tac [genPrefix.Nil RS genPrefix.append] 1);
-by Auto_tac;
-qed "Nil_genPrefix";
-AddIffs[Nil_genPrefix];
-
-Goal "(xs,ys) : genPrefix r ==> length xs <= length ys";
-by (etac genPrefix.induct 1);
-by Auto_tac;
-qed "genPrefix_length_le";
-
-Goal "[| (xs', ys'): genPrefix r |] \
-\ ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))";
-by (etac genPrefix.induct 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (force_tac (claset() addIs [genPrefix.append],
- simpset()) 1);
-val lemma = result();
-
-(*As usual converting it to an elimination rule is tiresome*)
-val major::prems =
-Goal "[| (x#xs, zs): genPrefix r; \
-\ !!y ys. [| zs = y#ys; (x,y) : r; (xs, ys) : genPrefix r |] ==> P \
-\ |] ==> P";
-by (cut_facts_tac [major RS lemma] 1);
-by (Full_simp_tac 1);
-by (REPEAT (eresolve_tac [exE, conjE] 1));
-by (REPEAT (ares_tac prems 1));
-qed "cons_genPrefixE";
-
-AddSEs [cons_genPrefixE];
-
-Goal "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)";
-by (blast_tac (claset() addIs [genPrefix.prepend]) 1);
-qed"Cons_genPrefix_Cons";
-AddIffs [Cons_genPrefix_Cons];
-
-
-(*** genPrefix is a partial order ***)
-
-Goalw [refl_def] "reflexive r ==> reflexive (genPrefix r)";
-by Auto_tac;
-by (induct_tac "x" 1);
-by (blast_tac (claset() addIs [genPrefix.prepend]) 2);
-by (blast_tac (claset() addIs [genPrefix.Nil]) 1);
-qed "refl_genPrefix";
-
-Goal "reflexive r ==> (l,l) : genPrefix r";
-by (etac ([refl_genPrefix,UNIV_I] MRS reflD) 1);
-qed "genPrefix_refl";
-
-Addsimps [genPrefix_refl];
-
-Goal "r<=s ==> genPrefix r <= genPrefix s";
-by (Clarify_tac 1);
-by (etac genPrefix.induct 1);
-by (auto_tac (claset() addIs [genPrefix.append], simpset()));
-qed "genPrefix_mono";
-
-
-(** Transitivity **)
-
-(*A lemma for proving genPrefix_trans_O*)
-Goal "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "append_genPrefix";
-
-(*Lemma proving transitivity and more*)
-Goalw [prefix_def]
- "(x, y) : genPrefix r \
-\ ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)";
-by (etac genPrefix.induct 1);
- by (blast_tac (claset() addDs [append_genPrefix]) 3);
- by (blast_tac (claset() addIs [genPrefix.prepend]) 2);
-by (Blast_tac 1);
-qed_spec_mp "genPrefix_trans_O";
-
-Goal "[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |] \
-\ ==> (x,z) : genPrefix r";
-by (rtac (impOfSubs (trans_O_subset RS genPrefix_mono)) 1);
- by (assume_tac 2);
-by (blast_tac (claset() addIs [genPrefix_trans_O]) 1);
-qed_spec_mp "genPrefix_trans";
-
-Goalw [prefix_def]
- "[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r";
-by (stac (R_O_Id RS sym) 1 THEN etac genPrefix_trans_O 1);
-by (assume_tac 1);
-qed_spec_mp "prefix_genPrefix_trans";
-
-Goalw [prefix_def]
- "[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r";
-by (stac (Id_O_R RS sym) 1 THEN etac genPrefix_trans_O 1);
-by (assume_tac 1);
-qed_spec_mp "genPrefix_prefix_trans";
-
-Goal "trans r ==> trans (genPrefix r)";
-by (blast_tac (claset() addIs [transI, genPrefix_trans]) 1);
-qed "trans_genPrefix";
-
-
-(** Antisymmetry **)
-
-Goal "[| (xs,ys) : genPrefix r; antisym r |] \
-\ ==> (ys,xs) : genPrefix r --> xs = ys";
-by (etac genPrefix.induct 1);
-by (full_simp_tac (simpset() addsimps [antisym_def]) 2);
-by (Blast_tac 2);
-by (Blast_tac 1);
-(*append case is hardest*)
-by (Clarify_tac 1);
-by (subgoal_tac "length zs = 0" 1);
-by (Force_tac 1);
-by (REPEAT (dtac genPrefix_length_le 1));
-by (full_simp_tac (simpset() delsimps [length_0_conv]) 1);
-qed_spec_mp "genPrefix_antisym";
-
-Goal "antisym r ==> antisym (genPrefix r)";
-by (blast_tac (claset() addIs [antisymI, genPrefix_antisym]) 1);
-qed "antisym_genPrefix";
-
-
-(*** recursion equations ***)
-
-Goal "((xs, []) : genPrefix r) = (xs = [])";
-by (induct_tac "xs" 1);
-by (Blast_tac 2);
-by (Simp_tac 1);
-qed "genPrefix_Nil";
-Addsimps [genPrefix_Nil];
-
-Goalw [refl_def]
- "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "same_genPrefix_genPrefix";
-Addsimps [same_genPrefix_genPrefix];
-
-Goal "((xs, y#ys) : genPrefix r) = \
-\ (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))";
-by (case_tac "xs" 1);
-by Auto_tac;
-qed "genPrefix_Cons";
-
-Goal "[| reflexive r; (xs,ys) : genPrefix r |] \
-\ ==> (xs@zs, take (length xs) ys @ zs) : genPrefix r";
-by (etac genPrefix.induct 1);
-by (ftac genPrefix_length_le 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2])));
-qed "genPrefix_take_append";
-
-Goal "[| reflexive r; (xs,ys) : genPrefix r; length xs = length ys |] \
-\ ==> (xs@zs, ys @ zs) : genPrefix r";
-by (dtac genPrefix_take_append 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [take_all]) 1);
-qed "genPrefix_append_both";
-
-
-(*NOT suitable for rewriting since [y] has the form y#ys*)
-Goal "xs @ y # ys = (xs @ [y]) @ ys";
-by Auto_tac;
-qed "append_cons_eq";
-
-Goal "[| (xs,ys) : genPrefix r; reflexive r |] \
-\ ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r";
-by (etac genPrefix.induct 1);
-by (Blast_tac 1);
-by (Asm_simp_tac 1);
-(*Append case is hardest*)
-by (Asm_simp_tac 1);
-by (forward_tac [genPrefix_length_le RS le_imp_less_or_eq] 1);
-by (etac disjE 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [neq_Nil_conv, nth_append])));
-by (blast_tac (claset() addIs [genPrefix.append]) 1);
-by Auto_tac;
-by (stac append_cons_eq 1);
-by (blast_tac (claset() addIs [genPrefix_append_both, genPrefix.append]) 1);
-val lemma = result() RS mp;
-
-Goal "[| (xs,ys) : genPrefix r; length xs < length ys; reflexive r |] \
-\ ==> (xs @ [ys ! length xs], ys) : genPrefix r";
-by (blast_tac (claset() addIs [lemma]) 1);
-qed "append_one_genPrefix";
-
-
-
-
-(** Proving the equivalence with Charpentier's definition **)
-
-Goal "ALL i ys. i < length xs \
-\ --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r";
-by (induct_tac "xs" 1);
-by Auto_tac;
-by (case_tac "i" 1);
-by Auto_tac;
-qed_spec_mp "genPrefix_imp_nth";
-
-Goal "ALL ys. length xs <= length ys \
-\ --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r) \
-\ --> (xs, ys) : genPrefix r";
-by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj,
- all_conj_distrib])));
-by (Clarify_tac 1);
-by (case_tac "ys" 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "nth_imp_genPrefix";
-
-Goal "((xs,ys) : genPrefix r) = \
-\ (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))";
-by (blast_tac (claset() addIs [genPrefix_length_le, genPrefix_imp_nth,
- nth_imp_genPrefix]) 1);
-qed "genPrefix_iff_nth";
-
-
-(** <= is a partial order: **)
-
-AddIffs [reflexive_Id, antisym_Id, trans_Id];
-
-Goalw [prefix_def] "xs <= (xs::'a list)";
-by (Simp_tac 1);
-qed "prefix_refl";
-AddIffs[prefix_refl];
-
-Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
-by (blast_tac (claset() addIs [genPrefix_trans]) 1);
-qed "prefix_trans";
-
-Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
-by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
-qed "prefix_antisym";
-
-Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)";
-by Auto_tac;
-qed "prefix_less_le";
-
-(*Monotonicity of "set" operator WRT prefix*)
-Goalw [prefix_def] "xs <= ys ==> set xs <= set ys";
-by (etac genPrefix.induct 1);
-by Auto_tac;
-qed "set_mono";
-
-
-(** recursion equations **)
-
-Goalw [prefix_def] "[] <= xs";
-by (simp_tac (simpset() addsimps [Nil_genPrefix]) 1);
-qed "Nil_prefix";
-AddIffs[Nil_prefix];
-
-Goalw [prefix_def] "(xs <= []) = (xs = [])";
-by (simp_tac (simpset() addsimps [genPrefix_Nil]) 1);
-qed "prefix_Nil";
-Addsimps [prefix_Nil];
-
-Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
-by (Simp_tac 1);
-qed"Cons_prefix_Cons";
-Addsimps [Cons_prefix_Cons];
-
-Goalw [prefix_def] "(xs@ys <= xs@zs) = (ys <= zs)";
-by (Simp_tac 1);
-qed "same_prefix_prefix";
-Addsimps [same_prefix_prefix];
-
-AddIffs (* (xs@ys <= xs) = (ys <= []) *)
- [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
-
-Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
-by (etac genPrefix.append 1);
-qed "prefix_appendI";
-Addsimps [prefix_appendI];
-
-Goalw [prefix_def]
- "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (simp_tac (simpset() addsimps [genPrefix_Cons]) 1);
-by Auto_tac;
-qed "prefix_Cons";
-
-Goalw [prefix_def]
- "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
-by (asm_simp_tac (simpset() addsimps [append_one_genPrefix]) 1);
-qed "append_one_prefix";
-
-Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
-by (etac genPrefix_length_le 1);
-qed "prefix_length_le";
-
-Goalw [prefix_def] "xs<=ys ==> xs~=ys --> length xs < length ys";
-by (etac genPrefix.induct 1);
-by Auto_tac;
-val lemma = result();
-
-Goalw [strict_prefix_def] "xs < ys ==> length xs < length ys";
-by (blast_tac (claset() addIs [lemma RS mp]) 1);
-qed "strict_prefix_length_less";
-
-Goal "mono length";
-by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
-qed "mono_length";
-
-(*Equivalence to the definition used in Lex/Prefix.thy*)
-Goalw [prefix_def] "(xs <= zs) = (EX ys. zs = xs@ys)";
-by (auto_tac (claset(),
- simpset() addsimps [genPrefix_iff_nth, nth_append]));
-by (res_inst_tac [("x", "drop (length xs) zs")] exI 1);
-by (rtac nth_equalityI 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [nth_append])));
-qed "prefix_iff";
-
-Goal "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
-by (simp_tac (simpset() addsimps [prefix_iff]) 1);
-by (rtac iffI 1);
- by (etac exE 1);
- by (rename_tac "zs" 1);
- by (res_inst_tac [("xs","zs")] rev_exhaust 1);
- by (Asm_full_simp_tac 1);
- by (hyp_subst_tac 1);
- by (asm_full_simp_tac (simpset() delsimps [append_assoc]
- addsimps [append_assoc RS sym])1);
-by (Force_tac 1);
-qed "prefix_snoc";
-Addsimps [prefix_snoc];
-
-Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
- by (Force_tac 1);
-by (asm_full_simp_tac (simpset() delsimps [append_assoc]
- addsimps [append_assoc RS sym])1);
-by (Force_tac 1);
-qed "prefix_append_iff";
-
-(*Although the prefix ordering is not linear, the prefixes of a list
- are linearly ordered.*)
-Goal "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
-by Auto_tac;
-qed_spec_mp "common_prefix_linear";
-
-
-(*** pfixLe, pfixGe: properties inherited from the translations ***)
-
-(** pfixLe **)
-
-Goalw [refl_def, Le_def] "reflexive Le";
-by Auto_tac;
-qed "reflexive_Le";
-
-Goalw [antisym_def, Le_def] "antisym Le";
-by Auto_tac;
-qed "antisym_Le";
-
-Goalw [trans_def, Le_def] "trans Le";
-by Auto_tac;
-qed "trans_Le";
-
-AddIffs [reflexive_Le, antisym_Le, trans_Le];
-
-Goal "x pfixLe x";
-by (Simp_tac 1);
-qed "pfixLe_refl";
-AddIffs[pfixLe_refl];
-
-Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
-by (blast_tac (claset() addIs [genPrefix_trans]) 1);
-qed "pfixLe_trans";
-
-Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
-by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
-qed "pfixLe_antisym";
-
-Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
-by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
-qed "prefix_imp_pfixLe";
-
-Goalw [refl_def, Ge_def] "reflexive Ge";
-by Auto_tac;
-qed "reflexive_Ge";
-
-Goalw [antisym_def, Ge_def] "antisym Ge";
-by Auto_tac;
-qed "antisym_Ge";
-
-Goalw [trans_def, Ge_def] "trans Ge";
-by Auto_tac;
-qed "trans_Ge";
-
-AddIffs [reflexive_Ge, antisym_Ge, trans_Ge];
-
-Goal "x pfixGe x";
-by (Simp_tac 1);
-qed "pfixGe_refl";
-AddIffs[pfixGe_refl];
-
-Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
-by (blast_tac (claset() addIs [genPrefix_trans]) 1);
-qed "pfixGe_trans";
-
-Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
-by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
-qed "pfixGe_antisym";
-
-Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
-by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
-qed "prefix_imp_pfixGe";
-
--- a/src/HOL/UNITY/GenPrefix.thy Thu Jan 30 18:08:09 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(* Title: HOL/UNITY/GenPrefix.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Charpentier's Generalized Prefix Relation
- (xs,ys) : genPrefix(r)
- if ys = xs' @ zs where length xs = length xs'
- and corresponding elements of xs, xs' are pairwise related by r
-
-Also overloads <= and < for lists!
-
-Based on Lex/Prefix
-*)
-
-GenPrefix = Main +
-
-consts
- genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
-
-inductive "genPrefix(r)"
- intrs
- Nil "([],[]) : genPrefix(r)"
-
- prepend "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==>
- (x#xs, y#ys) : genPrefix(r)"
-
- append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
-
-instance list :: (type)ord
-
-defs
- prefix_def "xs <= zs == (xs,zs) : genPrefix Id"
-
- strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)"
-
-
-(*Constants for the <= and >= relations, used below in translations*)
-constdefs
- Le :: "(nat*nat) set"
- "Le == {(x,y). x <= y}"
-
- Ge :: "(nat*nat) set"
- "Ge == {(x,y). y <= x}"
-
-syntax
- pfixLe :: [nat list, nat list] => bool (infixl "pfixLe" 50)
- pfixGe :: [nat list, nat list] => bool (infixl "pfixGe" 50)
-
-translations
- "xs pfixLe ys" == "(xs,ys) : genPrefix Le"
-
- "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"
-
-end
--- a/src/HOL/UNITY/Guar.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy Fri Jan 31 20:12:44 2003 +0100
@@ -3,8 +3,6 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
-Guarantees, etc.
-
From Chandy and Sanders, "Reasoning About Program Composition",
Technical Report 2000-003, University of Florida, 2000.
@@ -18,6 +16,8 @@
*)
+header{*Guarantees Specifications*}
+
theory Guar = Comp:
instance program :: (type) order
@@ -80,7 +80,7 @@
(*** existential properties ***)
-lemma ex1 [rule_format (no_asm)]:
+lemma ex1 [rule_format]:
"[| ex_prop X; finite GG |] ==>
GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
apply (unfold ex_prop_def)
--- a/src/HOL/UNITY/Lift_prog.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,8 @@
lift_prog, etc: replication of components and arrays of processes.
*)
+header{*Replication of Components*}
+
theory Lift_prog = Rename:
constdefs
@@ -38,9 +40,7 @@
declare insert_map_def [simp] delete_map_def [simp]
lemma insert_map_inverse: "delete_map i (insert_map i x f) = f"
-apply (rule ext)
-apply (simp (no_asm))
-done
+by (rule ext, simp)
lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
apply (rule ext)
@@ -50,13 +50,11 @@
(*** Injectiveness proof ***)
lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
-apply (drule_tac x = i in fun_cong)
-apply (simp (no_asm_use))
-done
+by (drule_tac x = i in fun_cong, simp)
lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g"
apply (drule_tac f = "delete_map i" in arg_cong)
-apply (simp (no_asm_use) add: insert_map_inverse)
+apply (simp add: insert_map_inverse)
done
lemma insert_map_inject':
@@ -69,8 +67,7 @@
lemma lift_map_eq_iff [iff]:
"(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu')))
= (uu = uu' & insert_map i s f = insert_map i' s' f')"
-apply (unfold lift_map_def, auto)
-done
+by (unfold lift_map_def, auto)
(*The !!s allows the automatic splitting of the bound variable*)
lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s"
@@ -91,9 +88,7 @@
done
lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'"
-apply (drule_tac f = "lift_map i" in arg_cong)
-apply (simp (no_asm_use))
-done
+by (drule_tac f = "lift_map i" in arg_cong, simp)
lemma surj_lift_map: "surj (lift_map i)"
apply (rule surjI)
@@ -101,8 +96,7 @@
done
lemma bij_lift_map [iff]: "bij (lift_map i)"
-apply (simp (no_asm) add: bij_def inj_lift_map surj_lift_map)
-done
+by (simp add: bij_def inj_lift_map surj_lift_map)
lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i"
by (rule inv_equality, auto)
@@ -115,8 +109,7 @@
(*sub's main property!*)
lemma sub_apply [simp]: "sub i f = f i"
-apply (simp (no_asm) add: sub_def)
-done
+by (simp add: sub_def)
(*** lift_set ***)
@@ -131,7 +124,7 @@
(*Do we really need both this one and its predecessor?*)
lemma lift_set_iff2 [iff]:
"((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
-by (simp (no_asm_simp) add: lift_set_def mem_rename_set_iff drop_map_def)
+by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
@@ -141,7 +134,7 @@
lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
apply (unfold lift_set_def)
-apply (simp (no_asm_simp) add: image_Un)
+apply (simp add: image_Un)
done
lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
@@ -153,91 +146,71 @@
(*** the lattice operations ***)
lemma bij_lift [iff]: "bij (lift i)"
-apply (simp (no_asm) add: lift_def)
-done
+by (simp add: lift_def)
lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
-apply (unfold lift_def)
-apply (simp (no_asm_simp))
-done
+by (simp add: lift_def)
lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
-apply (unfold lift_def)
-apply (simp (no_asm_simp))
-done
+by (simp add: lift_def)
lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
-apply (unfold lift_def)
-apply (simp (no_asm_simp))
-done
+by (simp add: lift_def)
(*** Safety: co, stable, invariant ***)
lemma lift_constrains:
"(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
-apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_constrains)
-done
+by (simp add: lift_def lift_set_def rename_constrains)
lemma lift_stable:
"(lift i F : stable (lift_set i A)) = (F : stable A)"
-apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_stable)
-done
+by (simp add: lift_def lift_set_def rename_stable)
lemma lift_invariant:
"(lift i F : invariant (lift_set i A)) = (F : invariant A)"
apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_invariant)
+apply (simp add: rename_invariant)
done
lemma lift_Constrains:
"(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_Constrains)
+apply (simp add: rename_Constrains)
done
lemma lift_Stable:
"(lift i F : Stable (lift_set i A)) = (F : Stable A)"
apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_Stable)
+apply (simp add: rename_Stable)
done
lemma lift_Always:
"(lift i F : Always (lift_set i A)) = (F : Always A)"
apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_Always)
+apply (simp add: rename_Always)
done
(*** Progress: transient, ensures ***)
lemma lift_transient:
"(lift i F : transient (lift_set i A)) = (F : transient A)"
-
-apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_transient)
-done
+by (simp add: lift_def lift_set_def rename_transient)
lemma lift_ensures:
"(lift i F : (lift_set i A) ensures (lift_set i B)) =
(F : A ensures B)"
-apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_ensures)
-done
+by (simp add: lift_def lift_set_def rename_ensures)
lemma lift_leadsTo:
"(lift i F : (lift_set i A) leadsTo (lift_set i B)) =
(F : A leadsTo B)"
-apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_leadsTo)
-done
+by (simp add: lift_def lift_set_def rename_leadsTo)
lemma lift_LeadsTo:
"(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =
(F : A LeadsTo B)"
-apply (unfold lift_def lift_set_def)
-apply (simp (no_asm_simp) add: rename_LeadsTo)
-done
+by (simp add: lift_def lift_set_def rename_LeadsTo)
(** guarantees **)
@@ -245,10 +218,9 @@
lemma lift_lift_guarantees_eq:
"(lift i F : (lift i ` X) guarantees (lift i ` Y)) =
(F : X guarantees Y)"
-
apply (unfold lift_def)
apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
-apply (simp (no_asm_simp) add: o_def)
+apply (simp add: o_def)
done
lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =
@@ -266,14 +238,14 @@
change function components other than i*)
lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
-apply (simp (no_asm_simp) add: lift_def rename_preserves)
-apply (simp (no_asm_use) add: lift_map_def o_def split_def)
+apply (simp add: lift_def rename_preserves)
+apply (simp add: lift_map_def o_def split_def)
done
lemma delete_map_eqE':
"(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
apply (drule_tac f = "insert_map i (g i) " in arg_cong)
-apply (simp (no_asm_use) add: insert_map_delete_map_eq)
+apply (simp add: insert_map_delete_map_eq)
apply (erule exI)
done
@@ -302,7 +274,8 @@
lemma preserves_snd_lift_stable:
"[| F : preserves snd; i~=j |]
==> lift j F : stable (lift_set i (A <*> UNIV))"
-apply (auto simp add: lift_def lift_set_def stable_def constrains_def rename_def extend_def mem_rename_set_iff)
+apply (auto simp add: lift_def lift_set_def stable_def constrains_def
+ rename_def extend_def mem_rename_set_iff)
apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
apply (drule_tac x = i in fun_cong, auto)
done
@@ -315,7 +288,8 @@
==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
apply (case_tac "i=j")
apply (simp add: lift_def lift_set_def rename_constrains)
-apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], assumption)
+apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
+ assumption)
apply (erule constrains_imp_subset [THEN lift_set_mono])
done
@@ -329,8 +303,9 @@
(if i=j then insert_map i s f
else if i<j then insert_map j t (f(i:=s))
else insert_map j t (f(i - Suc 0 := s)))"
-apply (rule ext)
+apply (rule ext)
apply (simp split add: nat_diff_split)
+ txt{*This simplification is VERY slow*}
done
lemma insert_map_eq_diff:
@@ -354,7 +329,8 @@
(i=j & F : transient (A <*> UNIV) | A={})"
apply (case_tac "i=j")
apply (auto simp add: lift_transient)
-apply (auto simp add: lift_set_def lift_def transient_def rename_def extend_def Domain_extend_act)
+apply (auto simp add: lift_set_def lift_def transient_def rename_def
+ extend_def Domain_extend_act)
apply (drule subsetD, blast, auto)
apply (rename_tac s f uu s' f' uu')
apply (subgoal_tac "f'=f & uu'=uu")
@@ -387,7 +363,8 @@
(if i=j then F : preserves (v o fst) else True)"
apply (drule subset_preserves_o [THEN subsetD])
apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
-apply (simp cong del: if_weak_cong add: lift_map_def eq_commute split_def o_def, auto)
+apply (auto cong del: if_weak_cong
+ simp add: lift_map_def eq_commute split_def o_def)
done
@@ -443,7 +420,7 @@
ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]
==> OK I (%i. lift i (F i))"
apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
-apply (simp (no_asm) add: Extend.AllowedActs_extend project_act_extend_act)
+apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
apply (rename_tac "act")
apply (subgoal_tac
"{(x, x'). \<exists>s f u s' f' u'.
@@ -468,6 +445,6 @@
lemma lift_image_preserves:
"lift i ` preserves v = preserves (v o drop_map i)"
-by (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq)
+by (simp add: rename_image_preserves lift_def inv_lift_map_eq)
end
--- a/src/HOL/UNITY/ListOrder.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/ListOrder.thy Fri Jan 31 20:12:44 2003 +0100
@@ -3,12 +3,425 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Lists are partially ordered by the prefix relation
+Lists are partially ordered by Charpentier's Generalized Prefix Relation
+ (xs,ys) : genPrefix(r)
+ if ys = xs' @ zs where length xs = length xs'
+ and corresponding elements of xs, xs' are pairwise related by r
+
+Also overloads <= and < for lists!
+
+Based on Lex/Prefix
*)
-ListOrder = GenPrefix +
+header {*The Prefix Ordering on Lists*}
+
+theory ListOrder = Main:
+
+consts
+ genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
+
+inductive "genPrefix(r)"
+ intros
+ Nil: "([],[]) : genPrefix(r)"
+
+ prepend: "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==>
+ (x#xs, y#ys) : genPrefix(r)"
+
+ append: "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
+
+instance list :: (type)ord ..
+
+defs
+ prefix_def: "xs <= zs == (xs,zs) : genPrefix Id"
+
+ strict_prefix_def: "xs < zs == xs <= zs & xs ~= (zs::'a list)"
+
+
+(*Constants for the <= and >= relations, used below in translations*)
+constdefs
+ Le :: "(nat*nat) set"
+ "Le == {(x,y). x <= y}"
+
+ Ge :: "(nat*nat) set"
+ "Ge == {(x,y). y <= x}"
+
+syntax
+ pfixLe :: "[nat list, nat list] => bool" (infixl "pfixLe" 50)
+ pfixGe :: "[nat list, nat list] => bool" (infixl "pfixGe" 50)
+
+translations
+ "xs pfixLe ys" == "(xs,ys) : genPrefix Le"
+
+ "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"
+
+
+subsection{*preliminary lemmas*}
+
+lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
+by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
+
+lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"
+by (erule genPrefix.induct, auto)
+
+lemma cdlemma:
+ "[| (xs', ys'): genPrefix r |]
+ ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"
+apply (erule genPrefix.induct, blast, blast)
+apply (force intro: genPrefix.append)
+done
+
+(*As usual converting it to an elimination rule is tiresome*)
+lemma cons_genPrefixE [elim!]:
+ "[| (x#xs, zs): genPrefix r;
+ !!y ys. [| zs = y#ys; (x,y) : r; (xs, ys) : genPrefix r |] ==> P
+ |] ==> P"
+by (drule cdlemma, simp, blast)
+
+lemma Cons_genPrefix_Cons [iff]:
+ "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"
+by (blast intro: genPrefix.prepend)
+
+
+subsection{*genPrefix is a partial order*}
+
+lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)"
+
+apply (unfold refl_def, auto)
+apply (induct_tac "x")
+prefer 2 apply (blast intro: genPrefix.prepend)
+apply (blast intro: genPrefix.Nil)
+done
+
+lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r"
+by (erule reflD [OF refl_genPrefix UNIV_I])
+
+lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
+apply clarify
+apply (erule genPrefix.induct)
+apply (auto intro: genPrefix.append)
+done
+
+
+(** Transitivity **)
+
+(*A lemma for proving genPrefix_trans_O*)
+lemma append_genPrefix [rule_format]:
+ "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
+by (induct_tac "xs", auto)
+
+(*Lemma proving transitivity and more*)
+lemma genPrefix_trans_O [rule_format]:
+ "(x, y) : genPrefix r
+ ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
+apply (erule genPrefix.induct)
+ prefer 3 apply (blast dest: append_genPrefix)
+ prefer 2 apply (blast intro: genPrefix.prepend, blast)
+done
+
+lemma genPrefix_trans [rule_format]:
+ "[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |]
+ ==> (x,z) : genPrefix r"
+apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
+ apply assumption
+apply (blast intro: genPrefix_trans_O)
+done
+
+lemma prefix_genPrefix_trans [rule_format]:
+ "[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
+apply (unfold prefix_def)
+apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
+done
+
+lemma genPrefix_prefix_trans [rule_format]:
+ "[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r"
+apply (unfold prefix_def)
+apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
+done
+
+lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
+by (blast intro: transI genPrefix_trans)
+
+
+(** Antisymmetry **)
+
+lemma genPrefix_antisym [rule_format]:
+ "[| (xs,ys) : genPrefix r; antisym r |]
+ ==> (ys,xs) : genPrefix r --> xs = ys"
+apply (erule genPrefix.induct)
+ txt{*Base case*}
+ apply blast
+ txt{*prepend case*}
+ apply (simp add: antisym_def)
+txt{*append case is the hardest*}
+apply clarify
+apply (subgoal_tac "length zs = 0", force)
+apply (drule genPrefix_length_le)+
+apply (simp del: length_0_conv)
+done
+
+lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
+by (blast intro: antisymI genPrefix_antisym)
+
+
+subsection{*recursion equations*}
+
+lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
+apply (induct_tac "xs")
+prefer 2 apply blast
+apply simp
+done
+
+lemma same_genPrefix_genPrefix [simp]:
+ "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
+apply (unfold refl_def)
+apply (induct_tac "xs")
+apply (simp_all (no_asm_simp))
+done
+
+lemma genPrefix_Cons:
+ "((xs, y#ys) : genPrefix r) =
+ (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
+by (case_tac "xs", auto)
+
+lemma genPrefix_take_append:
+ "[| reflexive r; (xs,ys) : genPrefix r |]
+ ==> (xs@zs, take (length xs) ys @ zs) : genPrefix r"
+apply (erule genPrefix.induct)
+apply (frule_tac [3] genPrefix_length_le)
+apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
+done
+
+lemma genPrefix_append_both:
+ "[| reflexive r; (xs,ys) : genPrefix r; length xs = length ys |]
+ ==> (xs@zs, ys @ zs) : genPrefix r"
+apply (drule genPrefix_take_append, assumption)
+apply (simp add: take_all)
+done
+
+
+(*NOT suitable for rewriting since [y] has the form y#ys*)
+lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
+by auto
+
+lemma aolemma:
+ "[| (xs,ys) : genPrefix r; reflexive r |]
+ ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
+apply (erule genPrefix.induct)
+ apply blast
+ apply simp
+txt{*Append case is hardest*}
+apply simp
+apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
+apply (erule disjE)
+apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
+apply (blast intro: genPrefix.append, auto)
+apply (subst append_cons_eq)
+apply (blast intro: genPrefix_append_both genPrefix.append)
+done
+
+lemma append_one_genPrefix:
+ "[| (xs,ys) : genPrefix r; length xs < length ys; reflexive r |]
+ ==> (xs @ [ys ! length xs], ys) : genPrefix r"
+by (blast intro: aolemma [THEN mp])
+
+
+(** Proving the equivalence with Charpentier's definition **)
+
+lemma genPrefix_imp_nth [rule_format]:
+ "ALL i ys. i < length xs
+ --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
+apply (induct_tac "xs", auto)
+apply (case_tac "i", auto)
+done
+
+lemma nth_imp_genPrefix [rule_format]:
+ "ALL ys. length xs <= length ys
+ --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)
+ --> (xs, ys) : genPrefix r"
+apply (induct_tac "xs")
+apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
+apply clarify
+apply (case_tac "ys")
+apply (force+)
+done
+
+lemma genPrefix_iff_nth:
+ "((xs,ys) : genPrefix r) =
+ (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
+apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
+done
+
+
+subsection{*The type of lists is partially ordered*}
+
+declare reflexive_Id [iff]
+ antisym_Id [iff]
+ trans_Id [iff]
+
+lemma prefix_refl [iff]: "xs <= (xs::'a list)"
+by (simp add: prefix_def)
+
+lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
+apply (unfold prefix_def)
+apply (blast intro: genPrefix_trans)
+done
+
+lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
+apply (unfold prefix_def)
+apply (blast intro: genPrefix_antisym)
+done
+
+lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"
+by (unfold strict_prefix_def, auto)
instance list :: (type) order
- (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)
+ by (intro_classes,
+ (assumption | rule prefix_refl prefix_trans prefix_antisym
+ prefix_less_le)+)
+
+(*Monotonicity of "set" operator WRT prefix*)
+lemma set_mono: "xs <= ys ==> set xs <= set ys"
+apply (unfold prefix_def)
+apply (erule genPrefix.induct, auto)
+done
+
+
+(** recursion equations **)
+
+lemma Nil_prefix [iff]: "[] <= xs"
+apply (unfold prefix_def)
+apply (simp add: Nil_genPrefix)
+done
+
+lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
+apply (unfold prefix_def)
+apply (simp add: genPrefix_Nil)
+done
+
+lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
+by (simp add: prefix_def)
+
+lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
+by (simp add: prefix_def)
+
+lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
+by (insert same_prefix_prefix [of xs ys "[]"], simp)
+
+lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
+apply (unfold prefix_def)
+apply (erule genPrefix.append)
+done
+
+lemma prefix_Cons:
+ "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
+by (simp add: prefix_def genPrefix_Cons)
+
+lemma append_one_prefix:
+ "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
+apply (unfold prefix_def)
+apply (simp add: append_one_genPrefix)
+done
+
+lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
+apply (unfold prefix_def)
+apply (erule genPrefix_length_le)
+done
+
+lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
+apply (unfold prefix_def)
+apply (erule genPrefix.induct, auto)
+done
+
+lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
+apply (unfold strict_prefix_def)
+apply (blast intro: splemma [THEN mp])
+done
+
+lemma mono_length: "mono length"
+by (blast intro: monoI prefix_length_le)
+
+(*Equivalence to the definition used in Lex/Prefix.thy*)
+lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
+apply (unfold prefix_def)
+apply (auto simp add: genPrefix_iff_nth nth_append)
+apply (rule_tac x = "drop (length xs) zs" in exI)
+apply (rule nth_equalityI)
+apply (simp_all (no_asm_simp) add: nth_append)
+done
+
+lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
+apply (simp add: prefix_iff)
+apply (rule iffI)
+ apply (erule exE)
+ apply (rename_tac "zs")
+ apply (rule_tac xs = zs in rev_exhaust)
+ apply simp
+ apply clarify
+ apply (simp del: append_assoc add: append_assoc [symmetric], force)
+done
+
+lemma prefix_append_iff:
+ "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
+apply (rule_tac xs = zs in rev_induct)
+ apply force
+apply (simp del: append_assoc add: append_assoc [symmetric], force)
+done
+
+(*Although the prefix ordering is not linear, the prefixes of a list
+ are linearly ordered.*)
+lemma common_prefix_linear [rule_format]:
+ "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
+by (rule_tac xs = zs in rev_induct, auto)
+
+
+subsection{*pfixLe, pfixGe: properties inherited from the translations*}
+
+(** pfixLe **)
+
+lemma reflexive_Le [iff]: "reflexive Le"
+by (unfold refl_def Le_def, auto)
+
+lemma antisym_Le [iff]: "antisym Le"
+by (unfold antisym_def Le_def, auto)
+
+lemma trans_Le [iff]: "trans Le"
+by (unfold trans_def Le_def, auto)
+
+lemma pfixLe_refl [iff]: "x pfixLe x"
+by simp
+
+lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
+by (blast intro: genPrefix_trans)
+
+lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
+by (blast intro: genPrefix_antisym)
+
+lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
+apply (unfold prefix_def Le_def)
+apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
+done
+
+lemma reflexive_Ge [iff]: "reflexive Ge"
+by (unfold refl_def Ge_def, auto)
+
+lemma antisym_Ge [iff]: "antisym Ge"
+by (unfold antisym_def Ge_def, auto)
+
+lemma trans_Ge [iff]: "trans Ge"
+by (unfold trans_def Ge_def, auto)
+
+lemma pfixGe_refl [iff]: "x pfixGe x"
+by simp
+
+lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
+by (blast intro: genPrefix_trans)
+
+lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
+by (blast intro: genPrefix_antisym)
+
+lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
+apply (unfold prefix_def Ge_def)
+apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
+done
end
--- a/src/HOL/UNITY/PPROD.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/PPROD.thy Fri Jan 31 20:12:44 2003 +0100
@@ -59,7 +59,8 @@
(** Safety & Progress: but are they used anywhere? **)
-lemma PLam_constrains: "[| i : I; ALL j. F j : preserves snd |] ==>
+lemma PLam_constrains:
+ "[| i : I; ALL j. F j : preserves snd |] ==>
(PLam I F : (lift_set i (A <*> UNIV)) co
(lift_set i (B <*> UNIV))) =
(F i : (A <*> UNIV) co (B <*> UNIV))"
@@ -69,25 +70,29 @@
apply (blast intro: constrains_imp_lift_constrains)
done
-lemma PLam_stable: "[| i : I; ALL j. F j : preserves snd |]
+lemma PLam_stable:
+ "[| i : I; ALL j. F j : preserves snd |]
==> (PLam I F : stable (lift_set i (A <*> UNIV))) =
(F i : stable (A <*> UNIV))"
apply (simp (no_asm_simp) add: stable_def PLam_constrains)
done
-lemma PLam_transient: "i : I ==>
+lemma PLam_transient:
+ "i : I ==>
PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
apply (simp (no_asm_simp) add: JN_transient PLam_def)
done
(*This holds because the F j cannot change (lift_set i)*)
-lemma PLam_ensures: "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV);
+lemma PLam_ensures:
+ "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV);
ALL j. F j : preserves snd |] ==>
PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
done
-lemma PLam_leadsTo_Basis: "[| i : I;
+lemma PLam_leadsTo_Basis:
+ "[| i : I;
F i : ((A <*> UNIV) - (B <*> UNIV)) co
((A <*> UNIV) Un (B <*> UNIV));
F i : transient ((A <*> UNIV) - (B <*> UNIV));
@@ -99,7 +104,8 @@
(** invariant **)
-lemma invariant_imp_PLam_invariant: "[| F i : invariant (A <*> UNIV); i : I;
+lemma invariant_imp_PLam_invariant:
+ "[| F i : invariant (A <*> UNIV); i : I;
ALL j. F j : preserves snd |]
==> PLam I F : invariant (lift_set i (A <*> UNIV))"
by (auto simp add: PLam_stable invariant_def)
@@ -143,21 +149,24 @@
(**UNUSED
(*The f0 premise ensures that the product is well-defined.*)
- lemma PLam_invariant_imp_invariant: "[| PLam I F : invariant (lift_set i A); i : I;
+ lemma PLam_invariant_imp_invariant:
+ "[| PLam I F : invariant (lift_set i A); i : I;
f0: Init (PLam I F) |] ==> F i : invariant A"
apply (auto simp add: invariant_def)
apply (drule_tac c = "f0 (i:=x) " in subsetD)
apply auto
done
- lemma PLam_invariant: "[| i : I; f0: Init (PLam I F) |]
+ lemma PLam_invariant:
+ "[| i : I; f0: Init (PLam I F) |]
==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
done
(*The f0 premise isn't needed if F is a constant program because then
we get an initial state by replicating that of F*)
- lemma reachable_PLam: "i : I
+ lemma reachable_PLam:
+ "i : I
==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
apply (auto simp add: invariant_def)
done
@@ -173,16 +182,17 @@
done
(*Result to justify a re-organization of this file*)
- lemma ??unknown??: "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
- apply auto
- result()
+ lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
+ by auto
- lemma reachable_PLam_subset1: "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
+ lemma reachable_PLam_subset1:
+ "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
apply (force dest!: reachable_PLam)
done
(*simplify using reachable_lift??*)
- lemma reachable_lift_Join_PLam [rule_format (no_asm)]: "[| i ~: I; A : reachable (F i) |]
+ lemma reachable_lift_Join_PLam [rule_format]:
+ "[| i ~: I; A : reachable (F i) |]
==> ALL f. f : reachable (PLam I F)
--> f(i:=A) : reachable (lift i (F i) Join PLam I F)"
apply (erule reachable.induct)
@@ -212,14 +222,16 @@
(*The index set must be finite: otherwise infinitely many copies of F can
perform actions, and PLam can never catch up in finite time.*)
- lemma reachable_PLam_subset2: "finite I
+ lemma reachable_PLam_subset2:
+ "finite I
==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
apply (erule finite_induct)
apply (simp (no_asm))
apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
done
- lemma reachable_PLam_eq: "finite I ==>
+ lemma reachable_PLam_eq:
+ "finite I ==>
reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
done
@@ -227,7 +239,8 @@
(** Co **)
- lemma Constrains_imp_PLam_Constrains: "[| F i : A Co B; i: I; finite I |]
+ lemma Constrains_imp_PLam_Constrains:
+ "[| F i : A Co B; i: I; finite I |]
==> PLam I F : (lift_set i A) Co (lift_set i B)"
apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
apply (auto simp add: constrains_def PLam_def)
@@ -236,13 +249,15 @@
- lemma PLam_Constrains: "[| i: I; finite I; f0: Init (PLam I F) |]
+ lemma PLam_Constrains:
+ "[| i: I; finite I; f0: Init (PLam I F) |]
==> (PLam I F : (lift_set i A) Co (lift_set i B)) =
(F i : A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
done
- lemma PLam_Stable: "[| i: I; finite I; f0: Init (PLam I F) |]
+ lemma PLam_Stable:
+ "[| i: I; finite I; f0: Init (PLam I F) |]
==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
done
@@ -250,13 +265,15 @@
(** const_PLam (no dependence on i) doesn't require the f0 premise **)
- lemma const_PLam_Constrains: "[| i: I; finite I |]
+ lemma const_PLam_Constrains:
+ "[| i: I; finite I |]
==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =
(F : A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
done
- lemma const_PLam_Stable: "[| i: I; finite I |]
+ lemma const_PLam_Stable:
+ "[| i: I; finite I |]
==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
done
--- a/src/HOL/UNITY/Project.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Project.thy Fri Jan 31 20:12:44 2003 +0100
@@ -8,6 +8,8 @@
Inheritance of GUARANTEES properties under extension
*)
+header{*Projections of State Sets*}
+
theory Project = Extend:
constdefs
@@ -32,10 +34,10 @@
done
-(** Safety **)
+subsection{*Safety*}
(*used below to prove Join_project_ensures*)
-lemma (in Extend) project_unless [rule_format (no_asm)]:
+lemma (in Extend) project_unless [rule_format]:
"[| G : stable C; project h C G : A unless B |]
==> G : (C Int extend_set h A) unless (extend_set h B)"
apply (simp add: unless_def project_constrains)
@@ -98,7 +100,7 @@
by (simp add: project_constrains extend_constrains)
-(*** "projecting" and union/intersection (no converses) ***)
+subsection{*"projecting" and union/intersection (no converses)*}
lemma projecting_Int:
"[| projecting C h F XA' XA; projecting C h F XB' XB |]
@@ -198,7 +200,7 @@
by (force simp only: extending_def Join_project_increasing)
-(** Reachability and project **)
+subsection{*Reachability and project*}
(*In practice, C = reachable(...): the inclusion is equality*)
lemma (in Extend) reachable_imp_reachable_project:
@@ -247,7 +249,7 @@
done
-(** Converse results for weak safety: benefits of the argument C *)
+subsection{*Converse results for weak safety: benefits of the argument C *}
(*In practice, C = reachable(...): the inclusion is equality*)
lemma (in Extend) reachable_project_imp_reachable:
@@ -329,8 +331,8 @@
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
done
-(** A lot of redundant theorems: all are proved to facilitate reasoning
- about guarantees. **)
+subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
+ about guarantees.*}
lemma (in Extend) projecting_Constrains:
"projecting (%G. reachable (extend h F Join G)) h F
@@ -390,9 +392,9 @@
done
-(*** leadsETo in the precondition (??) ***)
+subsection{*leadsETo in the precondition (??)*}
-(** transient **)
+subsubsection{*transient*}
lemma (in Extend) transient_extend_set_imp_project_transient:
"[| G : transient (C Int extend_set h A); G : stable C |]
@@ -422,7 +424,7 @@
done
-(** ensures -- a primitive combining progress with safety **)
+subsubsection{*ensures -- a primitive combining progress with safety*}
(*Used to prove project_leadsETo_I*)
lemma (in Extend) ensures_extend_set_imp_project_ensures:
@@ -456,7 +458,7 @@
done
(*Used to prove project_leadsETo_D*)
-lemma (in Extend) Join_project_ensures [rule_format (no_asm)]:
+lemma (in Extend) Join_project_ensures [rule_format]:
"[| project h C G ~: transient (A-B) | A<=B;
extend h F Join G : stable C;
F Join project h C G : A ensures B |]
@@ -470,8 +472,8 @@
simp add: ensures_def Join_transient)
done
-(** Lemma useful for both STRONG and WEAK progress, but the transient
- condition's very strong **)
+text{*Lemma useful for both STRONG and WEAK progress, but the transient
+ condition's very strong*}
(*The strange induction formula allows induction over the leadsTo
assumption's non-atomic precondition*)
@@ -505,7 +507,7 @@
project_set_reachable_extend_eq)
-(*** Towards project_Ensures_D ***)
+subsection{*Towards the theorem @{text project_Ensures_D}*}
lemma (in Extend) act_subset_imp_project_act_subset:
@@ -544,7 +546,7 @@
apply (force simp add: split_extended_all)
done
-lemma (in Extend) project_unless2 [rule_format (no_asm)]:
+lemma (in Extend) project_unless2 [rule_format]:
"[| G : stable C; project h C G : (project_set h C Int A) unless B |]
==> G : (C Int extend_set h A) unless (extend_set h B)"
by (auto dest: stable_constrains_Int intro: constrains_weaken
@@ -589,7 +591,7 @@
done
-(*** Guarantees ***)
+subsection{*Guarantees*}
lemma (in Extend) project_act_Restrict_subset_project_act:
"project_act h (Restrict C act) <= project_act h act"
@@ -641,9 +643,9 @@
(*It seems that neither "guarantees" law can be proved from the other.*)
-(*** guarantees corollaries ***)
+subsection{*guarantees corollaries*}
-(** Some could be deleted: the required versions are easy to prove **)
+subsubsection{*Some could be deleted: the required versions are easy to prove*}
lemma (in Extend) extend_guar_increasing:
"[| F : UNIV guarantees increasing func;
@@ -682,8 +684,8 @@
done
-(** Guarantees with a leadsTo postcondition
- THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
+subsubsection{*Guarantees with a leadsTo postcondition
+ ALL TOO WEAK because G can't affect F's variables at all**)
lemma (in Extend) project_leadsTo_D:
"[| F Join project h UNIV G : A leadsTo B;
--- a/src/HOL/UNITY/Rename.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Rename.thy Fri Jan 31 20:12:44 2003 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
+*)
-Renaming of state sets
-*)
+header{*Renaming of State Sets*}
theory Rename = Extend:
@@ -42,7 +42,7 @@
by (simp add: rename_def)
-(*** inverse properties ***)
+subsection{*inverse properties*}
lemma extend_set_inv:
"bij h
@@ -166,7 +166,7 @@
by (blast intro: bij_rename bij_rename_imp_bij)
-(*** the lattice operations ***)
+subsection{*the lattice operations*}
lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
by (simp add: rename_def Extend.extend_SKIP)
@@ -180,7 +180,7 @@
by (simp add: rename_def Extend.extend_JN)
-(*** Strong Safety: co, stable ***)
+subsection{*Strong Safety: co, stable*}
lemma rename_constrains:
"bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
@@ -205,7 +205,7 @@
done
-(*** Weak Safety: Co, Stable ***)
+subsection{*Weak Safety: Co, Stable*}
lemma reachable_rename_eq:
"bij h ==> reachable (rename h F) = h ` (reachable F)"
@@ -230,7 +230,7 @@
bij_is_surj [THEN surj_f_inv_f])
-(*** Progress: transient, ensures ***)
+subsection{*Progress: transient, ensures*}
lemma rename_transient:
"bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
@@ -290,7 +290,7 @@
by (simp add: Extend.OK_extend_iff rename_def)
-(*** "image" versions of the rules, for lifting "guarantees" properties ***)
+subsection{*"image" versions of the rules, for lifting "guarantees" properties*}
(*All the proofs are similar. Better would have been to prove one
meta-theorem, but how can we handle the polymorphism? E.g. in
--- a/src/HOL/UNITY/SubstAx.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,8 @@
Weak LeadsTo relation (restricted to the set of reachable states)
*)
+header{*Weak Progress*}
+
theory SubstAx = WFair + Constrains:
constdefs
@@ -27,7 +29,7 @@
done
-(*** Specialized laws for handling invariants ***)
+subsection{*Specialized laws for handling invariants*}
(** Conjoining an Always property **)
@@ -46,7 +48,7 @@
lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
-(*** Introduction rules: Basis, Trans, Union ***)
+subsection{*Introduction rules: Basis, Trans, Union*}
lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
apply (simp add: LeadsTo_def)
@@ -67,7 +69,7 @@
done
-(*** Derived rules ***)
+subsection{*Derived rules*}
lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
by (simp add: LeadsTo_def)
@@ -302,7 +304,7 @@
done
-(*** Induction rules ***)
+subsection{*Induction rules*}
(** Meta or object quantifier ????? **)
lemma LeadsTo_wf_induct:
@@ -368,7 +370,7 @@
done
-(*** Completion: Binary and General Finite versions ***)
+subsection{*Completion: Binary and General Finite versions*}
lemma Completion:
"[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C);
--- a/src/HOL/UNITY/UNITY.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy Fri Jan 31 20:12:44 2003 +0100
@@ -8,6 +8,8 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
+header {*The Basic UNITY Theory*}
+
theory UNITY = Main:
typedef (Program)
--- a/src/HOL/UNITY/UNITY_Main.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri Jan 31 20:12:44 2003 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
+*)
-Inclusive UNITY theory
-*)
+header{*Comprehensive UNITY Theory*}
theory UNITY_Main = Detects + PPROD + Follows
files "UNITY_tactics.ML":
--- a/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,71 @@
Specialized UNITY tactics, and ML bindings of theorems
*)
+(*ListOrder*)
+val Le_def = thm "Le_def";
+val Ge_def = thm "Ge_def";
+val prefix_def = thm "prefix_def";
+val Nil_genPrefix = thm "Nil_genPrefix";
+val genPrefix_length_le = thm "genPrefix_length_le";
+val cons_genPrefixE = thm "cons_genPrefixE";
+val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons";
+val refl_genPrefix = thm "refl_genPrefix";
+val genPrefix_refl = thm "genPrefix_refl";
+val genPrefix_mono = thm "genPrefix_mono";
+val append_genPrefix = thm "append_genPrefix";
+val genPrefix_trans_O = thm "genPrefix_trans_O";
+val genPrefix_trans = thm "genPrefix_trans";
+val prefix_genPrefix_trans = thm "prefix_genPrefix_trans";
+val genPrefix_prefix_trans = thm "genPrefix_prefix_trans";
+val trans_genPrefix = thm "trans_genPrefix";
+val genPrefix_antisym = thm "genPrefix_antisym";
+val antisym_genPrefix = thm "antisym_genPrefix";
+val genPrefix_Nil = thm "genPrefix_Nil";
+val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix";
+val genPrefix_Cons = thm "genPrefix_Cons";
+val genPrefix_take_append = thm "genPrefix_take_append";
+val genPrefix_append_both = thm "genPrefix_append_both";
+val append_cons_eq = thm "append_cons_eq";
+val append_one_genPrefix = thm "append_one_genPrefix";
+val genPrefix_imp_nth = thm "genPrefix_imp_nth";
+val nth_imp_genPrefix = thm "nth_imp_genPrefix";
+val genPrefix_iff_nth = thm "genPrefix_iff_nth";
+val prefix_refl = thm "prefix_refl";
+val prefix_trans = thm "prefix_trans";
+val prefix_antisym = thm "prefix_antisym";
+val prefix_less_le = thm "prefix_less_le";
+val set_mono = thm "set_mono";
+val Nil_prefix = thm "Nil_prefix";
+val prefix_Nil = thm "prefix_Nil";
+val Cons_prefix_Cons = thm "Cons_prefix_Cons";
+val same_prefix_prefix = thm "same_prefix_prefix";
+val append_prefix = thm "append_prefix";
+val prefix_appendI = thm "prefix_appendI";
+val prefix_Cons = thm "prefix_Cons";
+val append_one_prefix = thm "append_one_prefix";
+val prefix_length_le = thm "prefix_length_le";
+val strict_prefix_length_less = thm "strict_prefix_length_less";
+val mono_length = thm "mono_length";
+val prefix_iff = thm "prefix_iff";
+val prefix_snoc = thm "prefix_snoc";
+val prefix_append_iff = thm "prefix_append_iff";
+val common_prefix_linear = thm "common_prefix_linear";
+val reflexive_Le = thm "reflexive_Le";
+val antisym_Le = thm "antisym_Le";
+val trans_Le = thm "trans_Le";
+val pfixLe_refl = thm "pfixLe_refl";
+val pfixLe_trans = thm "pfixLe_trans";
+val pfixLe_antisym = thm "pfixLe_antisym";
+val prefix_imp_pfixLe = thm "prefix_imp_pfixLe";
+val reflexive_Ge = thm "reflexive_Ge";
+val antisym_Ge = thm "antisym_Ge";
+val trans_Ge = thm "trans_Ge";
+val pfixGe_refl = thm "pfixGe_refl";
+val pfixGe_trans = thm "pfixGe_trans";
+val pfixGe_antisym = thm "pfixGe_antisym";
+val prefix_imp_pfixGe = thm "prefix_imp_pfixGe";
+
+
(*UNITY*)
val constrains_def = thm "constrains_def";
val stable_def = thm "stable_def";
@@ -105,7 +170,6 @@
val leadsTo_refl = thm "leadsTo_refl";
val empty_leadsTo = thm "empty_leadsTo";
val leadsTo_UNIV = thm "leadsTo_UNIV";
-val leadsTo_induct_pre_lemma = thm "leadsTo_induct_pre_lemma";
val leadsTo_induct_pre = thm "leadsTo_induct_pre";
val leadsTo_weaken_R = thm "leadsTo_weaken_R";
val leadsTo_weaken_L = thm "leadsTo_weaken_L";
@@ -127,7 +191,6 @@
val psp = thm "psp";
val psp2 = thm "psp2";
val psp_unless = thm "psp_unless";
-val leadsTo_wf_induct_lemma = thm "leadsTo_wf_induct_lemma";
val leadsTo_wf_induct = thm "leadsTo_wf_induct";
val bounded_induct = thm "bounded_induct";
val lessThan_induct = thm "lessThan_induct";
@@ -137,12 +200,9 @@
val leadsTo_subset = thm "leadsTo_subset";
val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
val wlt_increasing = thm "wlt_increasing";
-val lemma1 = thm "lemma1";
val leadsTo_123 = thm "leadsTo_123";
val wlt_constrains_wlt = thm "wlt_constrains_wlt";
-val completion_lemma = thm "completion_lemma";
val completion = thm "completion";
-val finite_completion_lemma = thm "finite_completion_lemma";
val finite_completion = thm "finite_completion";
val stable_completion = thm "stable_completion";
val finite_stable_completion = thm "finite_stable_completion";
@@ -276,7 +336,6 @@
val LessThan_bounded_induct = thm "LessThan_bounded_induct";
val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct";
val Completion = thm "Completion";
-val Finite_completion_lemma = thm "Finite_completion_lemma";
val Finite_completion = thm "Finite_completion";
val Stable_completion = thm "Stable_completion";
val Finite_stable_completion = thm "Finite_stable_completion";
@@ -670,12 +729,10 @@
val increasing_Un = thm "increasing_Un";
val Increasing_Un = thm "Increasing_Un";
val Always_Un = thm "Always_Un";
-val Follows_Un_lemma = thm "Follows_Un_lemma";
val Follows_Un = thm "Follows_Un";
val increasing_union = thm "increasing_union";
val Increasing_union = thm "Increasing_union";
val Always_union = thm "Always_union";
-val Follows_union_lemma = thm "Follows_union_lemma";
val Follows_union = thm "Follows_union";
val Follows_setsum = thm "Follows_setsum";
val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe";
--- a/src/HOL/UNITY/Union.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Union.thy Fri Jan 31 20:12:44 2003 +0100
@@ -3,11 +3,11 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Unions of programs
-
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
*)
+header{*Unions of Programs*}
+
theory Union = SubstAx + FP:
constdefs
@@ -52,7 +52,7 @@
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _:_./ _)" 10)
-(** SKIP **)
+subsection{*SKIP*}
lemma Init_SKIP [simp]: "Init SKIP = UNIV"
by (simp add: SKIP_def)
@@ -66,7 +66,7 @@
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
by (force elim: reachable.induct intro: reachable.intros)
-(** SKIP and safety properties **)
+subsection{*SKIP and safety properties*}
lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
by (unfold constrains_def, auto)
@@ -80,7 +80,7 @@
declare SKIP_in_stable [THEN stable_imp_Stable, iff]
-(** Join **)
+subsection{*Join*}
lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
by (simp add: Join_def)
@@ -93,7 +93,7 @@
by (auto simp add: Join_def)
-(** JN **)
+subsection{*JN*}
lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
by (unfold JOIN_def SKIP_def, auto)
@@ -119,7 +119,7 @@
by (simp add: JOIN_def)
-(** Algebraic laws **)
+subsection{*Algebraic laws*}
lemma Join_commute: "F Join G = G Join F"
by (simp add: Join_def Un_commute Int_commute)
@@ -156,7 +156,7 @@
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
-(*** JN laws ***)
+subsection{*JN laws*}
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
@@ -183,7 +183,7 @@
done
-(*** Safety: co, stable, FP ***)
+subsection{*Safety: co, stable, FP*}
(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an
alternative precondition is A<=B, but most proofs using this rule require
@@ -245,7 +245,7 @@
by (simp add: FP_def JN_stable INTER_def)
-(*** Progress: transient, ensures ***)
+subsection{*Progress: transient, ensures*}
lemma JN_transient:
"i : I ==>
@@ -313,7 +313,7 @@
done
-(*** the ok and OK relations ***)
+subsection{*the ok and OK relations*}
lemma ok_SKIP1 [iff]: "SKIP ok F"
by (auto simp add: ok_def)
@@ -357,7 +357,7 @@
by (auto simp add: OK_iff_ok)
-(*** Allowed ***)
+subsection{*Allowed*}
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
by (auto simp add: Allowed_def)
@@ -374,7 +374,8 @@
lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
by (auto simp add: OK_iff_ok ok_iff_Allowed)
-(*** safety_prop, for reasoning about given instances of "ok" ***)
+subsection{*@{text safety_prop}, for reasoning about
+ given instances of "ok"*}
lemma safety_prop_Acts_iff:
"safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
--- a/src/HOL/UNITY/WFair.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/WFair.thy Fri Jan 31 20:12:44 2003 +0100
@@ -8,6 +8,8 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
+header{*Progress under Weak Fairness*}
+
theory WFair = UNITY:
constdefs
@@ -51,11 +53,10 @@
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
-(*** transient ***)
+subsection{*transient*}
lemma stable_transient_empty:
"[| F : stable A; F : transient A |] ==> A = {}"
-
by (unfold stable_def constrains_def transient_def, blast)
lemma transient_strengthen:
@@ -81,7 +82,7 @@
by (unfold transient_def, auto)
-(*** ensures ***)
+subsection{*ensures*}
lemma ensuresI:
"[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
@@ -117,7 +118,7 @@
by (simp (no_asm) add: ensures_def unless_def)
-(*** leadsTo ***)
+subsection{*leadsTo*}
lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
apply (unfold leadsTo_def)
@@ -235,7 +236,7 @@
lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
by (blast intro: subset_imp_leadsTo leadsTo_Trans)
-lemma leadsTo_weaken_L [rule_format (no_asm)]:
+lemma leadsTo_weaken_L [rule_format]:
"[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
by (blast intro: leadsTo_Trans subset_imp_leadsTo)
@@ -372,7 +373,7 @@
done
-(*** Proving the induction rules ***)
+subsection{*Proving the induction rules*}
(** The most general rule: r is any wf relation; f is any variant function **)
@@ -449,7 +450,7 @@
done
-(*** wlt ****)
+subsection{*wlt*}
(*Misra's property W3*)
lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
@@ -497,21 +498,33 @@
apply (auto intro: leadsTo_UN)
(*Blast_tac says PROOF FAILED*)
apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B"
- in constrains_UN [THEN constrains_weaken])
-apply (auto );
+ in constrains_UN [THEN constrains_weaken], auto)
done
(*Misra's property W5*)
lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
-apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], clarify)
-apply (subgoal_tac "Ba = wlt F B")
-prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
-apply (simp add: wlt_increasing Un_absorb2)
-done
+proof -
+ from wlt_leadsTo [of F B, THEN leadsTo_123]
+ show ?thesis
+ proof (elim exE conjE)
+(* assumes have to be in exactly the form as in the goal displayed at
+ this point. Isar doesn't give you any automation. *)
+ fix C
+ assume wlt: "wlt F B \<subseteq> C"
+ and lt: "F \<in> C leadsTo B"
+ and co: "F \<in> C - B co C \<union> B"
+ have eq: "C = wlt F B"
+ proof -
+ from lt and wlt show ?thesis
+ by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1])
+ qed
+ from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2)
+ qed
+qed
-(*** Completion: Binary and General Finite versions ***)
+subsection{*Completion: Binary and General Finite versions*}
lemma completion_lemma :
"[| W = wlt F (B' Un C);