conversion to new-style theories and tidying
authorpaulson
Fri Jan 31 20:12:44 2003 +0100 (2003-01-31)
changeset 137984c1a53627500
parent 13797 baefae13ad37
child 13799 77614fe09362
conversion to new-style theories and tidying
src/HOL/IsaMakefile
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/AllocBase.ML
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Detects.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/FP.thy
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/GenPrefix.ML
src/HOL/UNITY/GenPrefix.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/Project.thy
src/HOL/UNITY/Rename.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jan 30 18:08:09 2003 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 31 20:12:44 2003 +0100
     1.3 @@ -383,8 +383,7 @@
     1.4  $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
     1.5    UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
     1.6    UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
     1.7 -  UNITY/Extend.thy UNITY/FP.thy \
     1.8 -  UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
     1.9 +  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \
    1.10    UNITY/Guar.thy UNITY/Lift_prog.thy  UNITY/ListOrder.thy  \
    1.11    UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy \
    1.12    UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
    1.13 @@ -394,7 +393,7 @@
    1.14    UNITY/Simple/Network.thy\
    1.15    UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
    1.16    UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
    1.17 -  UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \
    1.18 +  UNITY/Comp/AllocBase.thy \
    1.19    UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
    1.20    UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
    1.21    UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
     2.1 --- a/src/HOL/UNITY/Comp.thy	Thu Jan 30 18:08:09 2003 +0100
     2.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Jan 31 20:12:44 2003 +0100
     2.3 @@ -13,6 +13,8 @@
     2.4  
     2.5  *)
     2.6  
     2.7 +header{*Composition: Basic Primitives*}
     2.8 +
     2.9  theory Comp = Union:
    2.10  
    2.11  instance program :: (type) ord ..
    2.12 @@ -42,7 +44,7 @@
    2.13    "funPair f g == %x. (f x, g x)"
    2.14  
    2.15  
    2.16 -(*** component <= ***)
    2.17 +subsection{*The component relation*}
    2.18  lemma componentI: 
    2.19       "H <= F | H <= G ==> H <= (F Join G)"
    2.20  apply (unfold component_def, auto)
    2.21 @@ -76,8 +78,7 @@
    2.22  
    2.23  lemma component_Join2: "G <= (F Join G)"
    2.24  apply (unfold component_def)
    2.25 -apply (simp (no_asm) add: Join_commute)
    2.26 -apply blast
    2.27 +apply (simp add: Join_commute, blast)
    2.28  done
    2.29  
    2.30  lemma Join_absorb1: "F<=G ==> F Join G = G"
    2.31 @@ -87,9 +88,7 @@
    2.32  by (auto simp add: Join_ac component_def)
    2.33  
    2.34  lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
    2.35 -apply (simp (no_asm) add: component_eq_subset)
    2.36 -apply blast
    2.37 -done
    2.38 +by (simp add: component_eq_subset, blast)
    2.39  
    2.40  lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
    2.41  apply (unfold component_def)
    2.42 @@ -107,9 +106,7 @@
    2.43  done
    2.44  
    2.45  lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
    2.46 -apply (simp (no_asm) add: component_eq_subset)
    2.47 -apply blast
    2.48 -done
    2.49 +by (simp add: component_eq_subset, blast)
    2.50  
    2.51  lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
    2.52  by (auto simp add: constrains_def component_eq_subset)
    2.53 @@ -118,7 +115,7 @@
    2.54  lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
    2.55  
    2.56  
    2.57 -(*** preserves ***)
    2.58 +subsection{*The preserves property*}
    2.59  
    2.60  lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
    2.61  by (unfold preserves_def, blast)
    2.62 @@ -135,8 +132,7 @@
    2.63  
    2.64  lemma JN_preserves [iff]:
    2.65       "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
    2.66 -apply (simp (no_asm) add: JN_stable preserves_def)
    2.67 -apply blast
    2.68 +apply (simp add: JN_stable preserves_def, blast)
    2.69  done
    2.70  
    2.71  lemma SKIP_preserves [iff]: "SKIP : preserves v"
    2.72 @@ -153,16 +149,13 @@
    2.73  
    2.74  
    2.75  lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
    2.76 -apply (simp (no_asm) add: funPair_def o_def)
    2.77 -done
    2.78 +by (simp add: funPair_def o_def)
    2.79  
    2.80  lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
    2.81 -apply (simp (no_asm) add: funPair_def o_def)
    2.82 -done
    2.83 +by (simp add: funPair_def o_def)
    2.84  
    2.85  lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
    2.86 -apply (simp (no_asm) add: funPair_def o_def)
    2.87 -done
    2.88 +by (simp add: funPair_def o_def)
    2.89  
    2.90  lemma subset_preserves_o: "preserves v <= preserves (w o v)"
    2.91  by (force simp add: preserves_def stable_def constrains_def)
    2.92 @@ -244,18 +237,13 @@
    2.93  
    2.94  (** localize **)
    2.95  lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
    2.96 -apply (unfold localize_def)
    2.97 -apply (simp (no_asm))
    2.98 -done
    2.99 +by (simp add: localize_def)
   2.100  
   2.101  lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
   2.102 -apply (unfold localize_def)
   2.103 -apply (simp (no_asm))
   2.104 -done
   2.105 +by (simp add: localize_def)
   2.106  
   2.107  lemma localize_AllowedActs_eq [simp]: 
   2.108   "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
   2.109 -apply (unfold localize_def, auto)
   2.110 -done
   2.111 +by (unfold localize_def, auto)
   2.112  
   2.113  end
     3.1 --- a/src/HOL/UNITY/Comp/AllocBase.ML	Thu Jan 30 18:08:09 2003 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,89 +0,0 @@
     3.4 -(*  Title:      HOL/UNITY/AllocBase.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1998  University of Cambridge
     3.8 -
     3.9 -Basis declarations for Chandy and Charpentier's Allocator
    3.10 -*)
    3.11 -
    3.12 -Goal "!!f :: nat=>nat. \
    3.13 -\     (ALL i. i<n --> f i <= g i) --> \
    3.14 -\     setsum f (lessThan n) <= setsum g (lessThan n)";
    3.15 -by (induct_tac "n" 1);
    3.16 -by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
    3.17 -by (dres_inst_tac [("x","n")] spec 1);
    3.18 -by (arith_tac 1);
    3.19 -qed_spec_mp "setsum_fun_mono";
    3.20 -
    3.21 -Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    3.22 -by (induct_tac "ys" 1);
    3.23 -by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
    3.24 -qed_spec_mp "tokens_mono_prefix";
    3.25 -
    3.26 -Goalw [mono_def] "mono tokens";
    3.27 -by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    3.28 -qed "mono_tokens";
    3.29 -
    3.30 -
    3.31 -(** bag_of **)
    3.32 -
    3.33 -Goal "bag_of (l@l') = bag_of l + bag_of l'";
    3.34 -by (induct_tac "l" 1);
    3.35 - by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
    3.36 -by (Simp_tac 1);
    3.37 -qed "bag_of_append";
    3.38 -Addsimps [bag_of_append];
    3.39 -
    3.40 -Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
    3.41 -by (rtac monoI 1); 
    3.42 -by (rewtac prefix_def);
    3.43 -by (etac genPrefix.induct 1);
    3.44 -by Auto_tac;
    3.45 -by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1); 
    3.46 -by (etac order_trans 1); 
    3.47 -by (rtac (thm "union_upper1") 1); 
    3.48 -qed "mono_bag_of";
    3.49 -
    3.50 -(** setsum **)
    3.51 -
    3.52 -Addcongs [setsum_cong];
    3.53 -
    3.54 -Goal "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = \
    3.55 -\     (\\<Sum>i: A Int lessThan k. {#f i#})";
    3.56 -by (rtac setsum_cong 1);
    3.57 -by Auto_tac;  
    3.58 -qed "bag_of_sublist_lemma";
    3.59 -
    3.60 -Goal "bag_of (sublist l A) = \
    3.61 -\     (\\<Sum>i: A Int lessThan (length l). {# l!i #})";
    3.62 -by (res_inst_tac [("xs","l")] rev_induct 1);
    3.63 -by (Simp_tac 1);
    3.64 -by (asm_simp_tac
    3.65 -    (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
    3.66 -                    nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
    3.67 -qed "bag_of_sublist";
    3.68 -
    3.69 -
    3.70 -Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
    3.71 -\     bag_of (sublist l A) + bag_of (sublist l B)";
    3.72 -by (subgoal_tac "A Int B Int {..length l(} = \
    3.73 -\                (A Int {..length l(}) Int (B Int {..length l(})" 1);
    3.74 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2, 
    3.75 -                                      setsum_Un_Int]) 1);
    3.76 -by (Blast_tac 1);
    3.77 -qed "bag_of_sublist_Un_Int";
    3.78 -
    3.79 -Goal "A Int B = {} \
    3.80 -\     ==> bag_of (sublist l (A Un B)) = \
    3.81 -\         bag_of (sublist l A) + bag_of (sublist l B)"; 
    3.82 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
    3.83 -qed "bag_of_sublist_Un_disjoint";
    3.84 -
    3.85 -Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
    3.86 -\     ==> bag_of (sublist l (UNION I A)) =  \
    3.87 -\         (\\<Sum>i:I. bag_of (sublist l (A i)))";  
    3.88 -by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
    3.89 -			    addsimps [bag_of_sublist]) 1);
    3.90 -by (stac setsum_UN_disjoint 1);
    3.91 -by Auto_tac;  
    3.92 -qed_spec_mp "bag_of_sublist_UN_disjoint";
     4.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jan 30 18:08:09 2003 +0100
     4.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jan 31 20:12:44 2003 +0100
     4.3 @@ -3,29 +3,124 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5      Copyright   1998  University of Cambridge
     4.6  
     4.7 -Common declarations for Chandy and Charpentier's Allocator
     4.8  *)
     4.9  
    4.10 -AllocBase = UNITY_Main + 
    4.11 +header{*Common Declarations for Chandy and Charpentier's Allocator*}
    4.12 +
    4.13 +theory AllocBase = UNITY_Main:
    4.14  
    4.15  consts
    4.16    NbT      :: nat       (*Number of tokens in system*)
    4.17    Nclients :: nat       (*Number of clients*)
    4.18  
    4.19 -rules
    4.20 -  NbT_pos  "0 < NbT"
    4.21 +axioms
    4.22 +  NbT_pos:  "0 < NbT"
    4.23  
    4.24  (*This function merely sums the elements of a list*)
    4.25 -consts tokens     :: nat list => nat
    4.26 +consts tokens     :: "nat list => nat"
    4.27  primrec 
    4.28    "tokens [] = 0"
    4.29    "tokens (x#xs) = x + tokens xs"
    4.30  
    4.31  consts
    4.32 -  bag_of :: 'a list => 'a multiset
    4.33 +  bag_of :: "'a list => 'a multiset"
    4.34  
    4.35  primrec
    4.36    "bag_of []     = {#}"
    4.37    "bag_of (x#xs) = {#x#} + bag_of xs"
    4.38  
    4.39 +lemma setsum_fun_mono [rule_format]:
    4.40 +     "!!f :: nat=>nat.  
    4.41 +      (ALL i. i<n --> f i <= g i) -->  
    4.42 +      setsum f (lessThan n) <= setsum g (lessThan n)"
    4.43 +apply (induct_tac "n")
    4.44 +apply (auto simp add: lessThan_Suc)
    4.45 +apply (drule_tac x = n in spec, arith)
    4.46 +done
    4.47 +
    4.48 +lemma tokens_mono_prefix [rule_format]:
    4.49 +     "ALL xs. xs <= ys --> tokens xs <= tokens ys"
    4.50 +apply (induct_tac "ys")
    4.51 +apply (auto simp add: prefix_Cons)
    4.52 +done
    4.53 +
    4.54 +lemma mono_tokens: "mono tokens"
    4.55 +apply (unfold mono_def)
    4.56 +apply (blast intro: tokens_mono_prefix)
    4.57 +done
    4.58 +
    4.59 +
    4.60 +(** bag_of **)
    4.61 +
    4.62 +lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
    4.63 +apply (induct_tac "l", simp)
    4.64 + apply (simp add: plus_ac0)
    4.65 +done
    4.66 +
    4.67 +lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    4.68 +apply (rule monoI)
    4.69 +apply (unfold prefix_def)
    4.70 +apply (erule genPrefix.induct, auto)
    4.71 +apply (simp add: union_le_mono)
    4.72 +apply (erule order_trans)
    4.73 +apply (rule union_upper1)
    4.74 +done
    4.75 +
    4.76 +(** setsum **)
    4.77 +
    4.78 +declare setsum_cong [cong]
    4.79 +
    4.80 +lemma bag_of_sublist_lemma:
    4.81 +     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
    4.82 +      (\<Sum>i: A Int lessThan k. {#f i#})"
    4.83 +apply (rule setsum_cong, auto)
    4.84 +done
    4.85 +
    4.86 +lemma bag_of_sublist:
    4.87 +     "bag_of (sublist l A) =  
    4.88 +      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
    4.89 +apply (rule_tac xs = l in rev_induct, simp)
    4.90 +apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    4.91 +                 bag_of_sublist_lemma plus_ac0)
    4.92 +done
    4.93 +
    4.94 +
    4.95 +lemma bag_of_sublist_Un_Int:
    4.96 +     "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
    4.97 +      bag_of (sublist l A) + bag_of (sublist l B)"
    4.98 +apply (subgoal_tac "A Int B Int {..length l (} = (A Int {..length l (}) Int (B Int {..length l (}) ")
    4.99 +apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
   4.100 +done
   4.101 +
   4.102 +lemma bag_of_sublist_Un_disjoint:
   4.103 +     "A Int B = {}  
   4.104 +      ==> bag_of (sublist l (A Un B)) =  
   4.105 +          bag_of (sublist l A) + bag_of (sublist l B)"
   4.106 +apply (simp add: bag_of_sublist_Un_Int [symmetric])
   4.107 +done
   4.108 +
   4.109 +lemma bag_of_sublist_UN_disjoint [rule_format]:
   4.110 +     "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
   4.111 +      ==> bag_of (sublist l (UNION I A)) =   
   4.112 +          (\<Sum>i:I. bag_of (sublist l (A i)))"
   4.113 +apply (simp del: UN_simps 
   4.114 +            add: UN_simps [symmetric] add: bag_of_sublist)
   4.115 +apply (subst setsum_UN_disjoint, auto)
   4.116 +done
   4.117 +
   4.118 +ML
   4.119 +{*
   4.120 +val NbT_pos = thm "NbT_pos";
   4.121 +val setsum_fun_mono = thm "setsum_fun_mono";
   4.122 +val tokens_mono_prefix = thm "tokens_mono_prefix";
   4.123 +val mono_tokens = thm "mono_tokens";
   4.124 +val bag_of_append = thm "bag_of_append";
   4.125 +val mono_bag_of = thm "mono_bag_of";
   4.126 +val bag_of_sublist_lemma = thm "bag_of_sublist_lemma";
   4.127 +val bag_of_sublist = thm "bag_of_sublist";
   4.128 +val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int";
   4.129 +val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint";
   4.130 +val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint";
   4.131 +*}
   4.132 +
   4.133  end
     5.1 --- a/src/HOL/UNITY/Constrains.thy	Thu Jan 30 18:08:09 2003 +0100
     5.2 +++ b/src/HOL/UNITY/Constrains.thy	Fri Jan 31 20:12:44 2003 +0100
     5.3 @@ -6,6 +6,8 @@
     5.4  Weak safety relations: restricted to the set of reachable states.
     5.5  *)
     5.6  
     5.7 +header{*Weak Safety*}
     5.8 +
     5.9  theory Constrains = UNITY:
    5.10  
    5.11  consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
    5.12 @@ -50,7 +52,7 @@
    5.13      "Increasing f == INT z. Stable {s. z <= f s}"
    5.14  
    5.15  
    5.16 -(*** traces and reachable ***)
    5.17 +subsection{*traces and reachable*}
    5.18  
    5.19  lemma reachable_equiv_traces:
    5.20       "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
    5.21 @@ -82,7 +84,7 @@
    5.22  done
    5.23  
    5.24  
    5.25 -(*** Co ***)
    5.26 +subsection{*Co*}
    5.27  
    5.28  (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
    5.29  lemmas constrains_reachable_Int =  
    5.30 @@ -184,7 +186,7 @@
    5.31  by (simp add: Constrains_eq_constrains constrains_def, blast)
    5.32  
    5.33  
    5.34 -(*** Stable ***)
    5.35 +subsection{*Stable*}
    5.36  
    5.37  (*Useful because there's no Stable_weaken.  [Tanja Vos]*)
    5.38  lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
    5.39 @@ -238,7 +240,7 @@
    5.40  
    5.41  
    5.42  
    5.43 -(*** Increasing ***)
    5.44 +subsection{*Increasing*}
    5.45  
    5.46  lemma IncreasingD: 
    5.47       "F : Increasing f ==> F : Stable {s. x <= f s}"
    5.48 @@ -265,14 +267,14 @@
    5.49      increasing_constant [THEN increasing_imp_Increasing, standard, iff]
    5.50  
    5.51  
    5.52 -(*** The Elimination Theorem.  The "free" m has become universally quantified!
    5.53 -     Should the premise be !!m instead of ALL m ?  Would make it harder to use
    5.54 -     in forward proof. ***)
    5.55 +subsection{*The Elimination Theorem*}
    5.56 +
    5.57 +(*The "free" m has become universally quantified! Should the premise be !!m
    5.58 +instead of ALL m ?  Would make it harder to use in forward proof.*)
    5.59  
    5.60  lemma Elimination: 
    5.61      "[| ALL m. F : {s. s x = m} Co (B m) |]  
    5.62       ==> F : {s. s x : M} Co (UN m:M. B m)"
    5.63 -
    5.64  by (unfold Constrains_def constrains_def, blast)
    5.65  
    5.66  (*As above, but for the trivial case of a one-variable state, in which the
    5.67 @@ -282,7 +284,7 @@
    5.68  by (unfold Constrains_def constrains_def, blast)
    5.69  
    5.70  
    5.71 -(*** Specialized laws for handling Always ***)
    5.72 +subsection{*Specialized laws for handling Always*}
    5.73  
    5.74  (** Natural deduction rules for "Always A" **)
    5.75  
    5.76 @@ -340,7 +342,7 @@
    5.77  by (auto simp add: Always_eq_includes_reachable)
    5.78  
    5.79  
    5.80 -(*** "Co" rules involving Always ***)
    5.81 +subsection{*"Co" rules involving Always*}
    5.82  
    5.83  lemma Always_Constrains_pre:
    5.84       "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
     6.1 --- a/src/HOL/UNITY/Detects.thy	Thu Jan 30 18:08:09 2003 +0100
     6.2 +++ b/src/HOL/UNITY/Detects.thy	Fri Jan 31 20:12:44 2003 +0100
     6.3 @@ -6,6 +6,8 @@
     6.4  Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
     6.5  *)
     6.6  
     6.7 +header{*The Detects Relation*}
     6.8 +
     6.9  theory Detects = FP + SubstAx:
    6.10  
    6.11  consts
     7.1 --- a/src/HOL/UNITY/ELT.thy	Thu Jan 30 18:08:09 2003 +0100
     7.2 +++ b/src/HOL/UNITY/ELT.thy	Fri Jan 31 20:12:44 2003 +0100
     7.3 @@ -22,6 +22,8 @@
     7.4    monos Pow_mono
     7.5  *)
     7.6  
     7.7 +header{*Progress Under Allowable Sets*}
     7.8 +
     7.9  theory ELT = Project:
    7.10  
    7.11  consts
    7.12 @@ -91,8 +93,7 @@
    7.13  (*preserving v preserves properties given by v*)
    7.14  lemma preserves_givenBy_imp_stable:
    7.15       "[| F : preserves v;  D : givenBy v |] ==> F : stable D"
    7.16 -apply (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
    7.17 -done
    7.18 +by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
    7.19  
    7.20  lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v"
    7.21  apply (simp (no_asm) add: givenBy_eq_Collect)
    7.22 @@ -212,7 +213,7 @@
    7.23  apply (blast intro: subset_imp_leadsETo leadsETo_Trans)
    7.24  done
    7.25  
    7.26 -lemma leadsETo_weaken_L [rule_format (no_asm)]:
    7.27 +lemma leadsETo_weaken_L [rule_format]:
    7.28       "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
    7.29  apply (blast intro: leadsETo_Trans subset_imp_leadsETo)
    7.30  done
    7.31 @@ -458,13 +459,13 @@
    7.32  
    7.33  lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
    7.34  
    7.35 -lemma LeadsETo_weaken_R [rule_format (no_asm)]:
    7.36 +lemma LeadsETo_weaken_R [rule_format]:
    7.37       "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
    7.38  apply (simp (no_asm_use) add: LeadsETo_def)
    7.39  apply (blast intro: leadsETo_weaken_R)
    7.40  done
    7.41  
    7.42 -lemma LeadsETo_weaken_L [rule_format (no_asm)]:
    7.43 +lemma LeadsETo_weaken_L [rule_format]:
    7.44       "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
    7.45  apply (simp (no_asm_use) add: LeadsETo_def)
    7.46  apply (blast intro: leadsETo_weaken_L)
     8.1 --- a/src/HOL/UNITY/Extend.thy	Thu Jan 30 18:08:09 2003 +0100
     8.2 +++ b/src/HOL/UNITY/Extend.thy	Fri Jan 31 20:12:44 2003 +0100
     8.3 @@ -3,11 +3,13 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1998  University of Cambridge
     8.6  
     8.7 -Extending of state sets
     8.8 +Extending of state setsExtending of state sets
     8.9    function f (forget)    maps the extended state to the original state
    8.10    function g (forgotten) maps the extended state to the "extending part"
    8.11  *)
    8.12  
    8.13 +header{*Extending State Sets*}
    8.14 +
    8.15  theory Extend = Guar:
    8.16  
    8.17  constdefs
    8.18 @@ -60,7 +62,8 @@
    8.19  (** These we prove OUTSIDE the locale. **)
    8.20  
    8.21  
    8.22 -(*** Restrict [MOVE to Relation.thy?] ***)
    8.23 +subsection{*Restrict*}
    8.24 +(*MOVE to Relation.thy?*)
    8.25  
    8.26  lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)"
    8.27  by (unfold Restrict_def, blast)
    8.28 @@ -130,7 +133,7 @@
    8.29  done
    8.30  
    8.31  
    8.32 -(*** Trivial properties of f, g, h ***)
    8.33 +subsection{*Trivial properties of f, g, h*}
    8.34  
    8.35  lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x" 
    8.36  by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
    8.37 @@ -163,7 +166,7 @@
    8.38  
    8.39  
    8.40  
    8.41 -(*** extend_set: basic properties ***)
    8.42 +subsection{*@{term extend_set}: basic properties*}
    8.43  
    8.44  lemma project_set_iff [iff]:
    8.45       "(x : project_set h C) = (EX y. h(x,y) : C)"
    8.46 @@ -210,7 +213,7 @@
    8.47  apply (auto simp add: split_extended_all)
    8.48  done
    8.49  
    8.50 -(*** project_set: basic properties ***)
    8.51 +subsection{*@{term project_set}: basic properties*}
    8.52  
    8.53  (*project_set is simply image!*)
    8.54  lemma (in Extend) project_set_eq: "project_set h C = f ` C"
    8.55 @@ -221,7 +224,7 @@
    8.56  by (auto simp add: split_extended_all)
    8.57  
    8.58  
    8.59 -(*** More laws ***)
    8.60 +subsection{*More laws*}
    8.61  
    8.62  (*Because A and B could differ on the "other" part of the state, 
    8.63     cannot generalize to 
    8.64 @@ -265,7 +268,7 @@
    8.65  by (unfold extend_set_def, auto)
    8.66  
    8.67  
    8.68 -(*** extend_act ***)
    8.69 +subsection{*@{term extend_act}*}
    8.70  
    8.71  (*Can't strengthen it to
    8.72    ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
    8.73 @@ -335,9 +338,9 @@
    8.74  
    8.75  
    8.76  
    8.77 -(**** extend ****)
    8.78 +subsection{*extend ****)
    8.79  
    8.80 -(*** Basic properties ***)
    8.81 +(*** Basic properties*}
    8.82  
    8.83  lemma Init_extend [simp]:
    8.84       "Init (extend h F) = extend_set h (Init F)"
    8.85 @@ -451,7 +454,7 @@
    8.86  by (simp add: component_eq_subset, blast)
    8.87  
    8.88  
    8.89 -(*** Safety: co, stable ***)
    8.90 +subsection{*Safety: co, stable*}
    8.91  
    8.92  lemma (in Extend) extend_constrains:
    8.93       "(extend h F : (extend_set h A) co (extend_set h B)) =  
    8.94 @@ -477,7 +480,7 @@
    8.95  by (simp add: stable_def extend_constrains_project_set)
    8.96  
    8.97  
    8.98 -(*** Weak safety primitives: Co, Stable ***)
    8.99 +subsection{*Weak safety primitives: Co, Stable*}
   8.100  
   8.101  lemma (in Extend) reachable_extend_f:
   8.102       "p : reachable (extend h F) ==> f p : reachable F"
   8.103 @@ -570,7 +573,7 @@
   8.104  by (simp add: stable_def project_constrains_project_set)
   8.105  
   8.106  
   8.107 -(*** Progress: transient, ensures ***)
   8.108 +subsection{*Progress: transient, ensures*}
   8.109  
   8.110  lemma (in Extend) extend_transient:
   8.111       "(extend h F : transient (extend_set h A)) = (F : transient A)"
   8.112 @@ -591,7 +594,7 @@
   8.113  apply (simp add: leadsTo_UN extend_set_Union)
   8.114  done
   8.115  
   8.116 -(*** Proving the converse takes some doing! ***)
   8.117 +subsection{*Proving the converse takes some doing!*}
   8.118  
   8.119  lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)"
   8.120  by (simp (no_asm) add: slice_def)
   8.121 @@ -631,7 +634,7 @@
   8.122  apply (blast intro: leadsTo_UN)
   8.123  done
   8.124  
   8.125 -lemma (in Extend) extend_leadsTo_slice [rule_format (no_asm)]:
   8.126 +lemma (in Extend) extend_leadsTo_slice [rule_format]:
   8.127       "extend h F : AU leadsTo BU  
   8.128        ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"
   8.129  apply (erule leadsTo_induct)
   8.130 @@ -656,7 +659,7 @@
   8.131                extend_set_Int_distrib [symmetric])
   8.132  
   8.133  
   8.134 -(*** preserves ***)
   8.135 +subsection{*preserves*}
   8.136  
   8.137  lemma (in Extend) project_preserves_I:
   8.138       "G : preserves (v o f) ==> project h C G : preserves v"
   8.139 @@ -677,7 +680,7 @@
   8.140                     constrains_def g_def)
   8.141  
   8.142  
   8.143 -(*** Guarantees ***)
   8.144 +subsection{*Guarantees*}
   8.145  
   8.146  lemma (in Extend) project_extend_Join:
   8.147       "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)"
     9.1 --- a/src/HOL/UNITY/FP.thy	Thu Jan 30 18:08:09 2003 +0100
     9.2 +++ b/src/HOL/UNITY/FP.thy	Fri Jan 31 20:12:44 2003 +0100
     9.3 @@ -3,11 +3,11 @@
     9.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.5      Copyright   1998  University of Cambridge
     9.6  
     9.7 -Fixed Point of a Program
     9.8 -
     9.9  From Misra, "A Logic for Concurrent Programming", 1994
    9.10  *)
    9.11  
    9.12 +header{*Fixed Point of a Program*}
    9.13 +
    9.14  theory FP = UNITY:
    9.15  
    9.16  constdefs
    10.1 --- a/src/HOL/UNITY/Follows.thy	Thu Jan 30 18:08:09 2003 +0100
    10.2 +++ b/src/HOL/UNITY/Follows.thy	Fri Jan 31 20:12:44 2003 +0100
    10.3 @@ -2,9 +2,9 @@
    10.4      ID:         $Id$
    10.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.6      Copyright   1998  University of Cambridge
    10.7 +*)
    10.8  
    10.9 -The "Follows" relation of Charpentier and Sivilotte
   10.10 -*)
   10.11 +header{*The Follows Relation of Charpentier and Sivilotte*}
   10.12  
   10.13  theory Follows = SubstAx + ListOrder + Multiset:
   10.14  
   10.15 @@ -35,9 +35,8 @@
   10.16  apply (blast intro: monoD order_trans)+
   10.17  done
   10.18  
   10.19 -lemma Follows_constant: "F : (%s. c) Fols (%s. c)"
   10.20 +lemma Follows_constant [iff]: "F : (%s. c) Fols (%s. c)"
   10.21  by (unfold Follows_def, auto)
   10.22 -declare Follows_constant [iff]
   10.23  
   10.24  lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)"
   10.25  apply (unfold Follows_def, clarify)
   10.26 @@ -60,28 +59,23 @@
   10.27  done
   10.28  
   10.29  
   10.30 -(** Destructiom rules **)
   10.31 +subsection{*Destruction rules*}
   10.32  
   10.33 -lemma Follows_Increasing1: 
   10.34 -     "F : f Fols g ==> F : Increasing f"
   10.35 -
   10.36 +lemma Follows_Increasing1: "F : f Fols g ==> F : Increasing f"
   10.37  apply (unfold Follows_def, blast)
   10.38  done
   10.39  
   10.40 -lemma Follows_Increasing2: 
   10.41 -     "F : f Fols g ==> F : Increasing g"
   10.42 +lemma Follows_Increasing2: "F : f Fols g ==> F : Increasing g"
   10.43  apply (unfold Follows_def, blast)
   10.44  done
   10.45  
   10.46 -lemma Follows_Bounded: 
   10.47 -     "F : f Fols g ==> F : Always {s. f s <= g s}"
   10.48 +lemma Follows_Bounded: "F : f Fols g ==> F : Always {s. f s <= g s}"
   10.49  apply (unfold Follows_def, blast)
   10.50  done
   10.51  
   10.52  lemma Follows_LeadsTo: 
   10.53       "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"
   10.54 -apply (unfold Follows_def, blast)
   10.55 -done
   10.56 +by (unfold Follows_def, blast)
   10.57  
   10.58  lemma Follows_LeadsTo_pfixLe:
   10.59       "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
   10.60 @@ -107,7 +101,8 @@
   10.61  
   10.62  apply (unfold Follows_def Increasing_def Stable_def, auto)
   10.63  apply (erule_tac [3] Always_LeadsTo_weaken)
   10.64 -apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" in Always_Constrains_weaken, auto)
   10.65 +apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" 
   10.66 +       in Always_Constrains_weaken, auto)
   10.67  apply (drule Always_Int_I, assumption)
   10.68  apply (force intro: Always_weaken)
   10.69  done
   10.70 @@ -116,13 +111,14 @@
   10.71       "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"
   10.72  apply (unfold Follows_def Increasing_def Stable_def, auto)
   10.73  apply (erule_tac [3] Always_LeadsTo_weaken)
   10.74 -apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" in Always_Constrains_weaken, auto)
   10.75 +apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}"
   10.76 +       in Always_Constrains_weaken, auto)
   10.77  apply (drule Always_Int_I, assumption)
   10.78  apply (force intro: Always_weaken)
   10.79  done
   10.80  
   10.81  
   10.82 -(** Union properties (with the subset ordering) **)
   10.83 +subsection{*Union properties (with the subset ordering)*}
   10.84  
   10.85  (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
   10.86  lemma increasing_Un: 
   10.87 @@ -137,7 +133,8 @@
   10.88  lemma Increasing_Un: 
   10.89      "[| F : Increasing f;  F: Increasing g |]  
   10.90       ==> F : Increasing (%s. (f s) Un (g s))"
   10.91 -apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto)
   10.92 +apply (auto simp add: Increasing_def Stable_def Constrains_def
   10.93 +                      stable_def constrains_def)
   10.94  apply (drule_tac x = "f xa" in spec)
   10.95  apply (drule_tac x = "g xa" in spec)
   10.96  apply (blast dest!: bspec)
   10.97 @@ -147,8 +144,7 @@
   10.98  lemma Always_Un:
   10.99       "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]  
  10.100        ==> F : Always {s. f' s Un g' s <= f s Un g s}"
  10.101 -apply (simp add: Always_eq_includes_reachable, blast)
  10.102 -done
  10.103 +by (simp add: Always_eq_includes_reachable, blast)
  10.104  
  10.105  (*Lemma to re-use the argument that one variable increases (progress)
  10.106    while the other variable doesn't decrease (safety)*)
  10.107 @@ -164,8 +160,7 @@
  10.108  apply (rule PSP_Stable)
  10.109  apply (erule_tac x = "f s" in spec)
  10.110  apply (erule Stable_Int, assumption)
  10.111 -apply blast
  10.112 -apply blast
  10.113 +apply blast+
  10.114  done
  10.115  
  10.116  lemma Follows_Un: 
  10.117 @@ -180,12 +175,11 @@
  10.118  done
  10.119  
  10.120  
  10.121 -(** Multiset union properties (with the multiset ordering) **)
  10.122 +subsection{*Multiset union properties (with the multiset ordering)*}
  10.123  
  10.124  lemma increasing_union: 
  10.125      "[| F : increasing f;  F: increasing g |]  
  10.126       ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))"
  10.127 -
  10.128  apply (unfold increasing_def stable_def constrains_def, auto)
  10.129  apply (drule_tac x = "f xa" in spec)
  10.130  apply (drule_tac x = "g xa" in spec)
  10.131 @@ -196,7 +190,8 @@
  10.132  lemma Increasing_union: 
  10.133      "[| F : Increasing f;  F: Increasing g |]  
  10.134       ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
  10.135 -apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto)
  10.136 +apply (auto simp add: Increasing_def Stable_def Constrains_def
  10.137 +                      stable_def constrains_def)
  10.138  apply (drule_tac x = "f xa" in spec)
  10.139  apply (drule_tac x = "g xa" in spec)
  10.140  apply (drule bspec, assumption) 
    11.1 --- a/src/HOL/UNITY/GenPrefix.ML	Thu Jan 30 18:08:09 2003 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,424 +0,0 @@
    11.4 -(*  Title:      HOL/UNITY/GenPrefix.thy
    11.5 -    ID:         $Id$
    11.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 -    Copyright   1999  University of Cambridge
    11.8 -
    11.9 -Charpentier's Generalized Prefix Relation
   11.10 -   (xs,ys) : genPrefix r
   11.11 -     if ys = xs' @ zs where length xs = length xs'
   11.12 -     and corresponding elements of xs, xs' are pairwise related by r
   11.13 -
   11.14 -Based on Lex/Prefix
   11.15 -*)
   11.16 -
   11.17 -(*** preliminary lemmas ***)
   11.18 -
   11.19 -Goal "([], xs) : genPrefix r";
   11.20 -by (cut_facts_tac [genPrefix.Nil RS genPrefix.append] 1);
   11.21 -by Auto_tac;
   11.22 -qed "Nil_genPrefix";
   11.23 -AddIffs[Nil_genPrefix];
   11.24 -
   11.25 -Goal "(xs,ys) : genPrefix r ==> length xs <= length ys";
   11.26 -by (etac genPrefix.induct 1);
   11.27 -by Auto_tac;
   11.28 -qed "genPrefix_length_le";
   11.29 -
   11.30 -Goal "[| (xs', ys'): genPrefix r |] \
   11.31 -\     ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))";
   11.32 -by (etac genPrefix.induct 1);
   11.33 -by (Blast_tac 1);
   11.34 -by (Blast_tac 1);
   11.35 -by (force_tac (claset() addIs [genPrefix.append],
   11.36 -	       simpset()) 1);
   11.37 -val lemma = result();
   11.38 -
   11.39 -(*As usual converting it to an elimination rule is tiresome*)
   11.40 -val major::prems = 
   11.41 -Goal "[| (x#xs, zs): genPrefix r;  \
   11.42 -\        !!y ys. [| zs = y#ys;  (x,y) : r;  (xs, ys) : genPrefix r |] ==> P \
   11.43 -\     |] ==> P";
   11.44 -by (cut_facts_tac [major RS lemma] 1);
   11.45 -by (Full_simp_tac 1);
   11.46 -by (REPEAT (eresolve_tac [exE, conjE] 1));
   11.47 -by (REPEAT (ares_tac prems 1));
   11.48 -qed "cons_genPrefixE";
   11.49 -
   11.50 -AddSEs [cons_genPrefixE];
   11.51 -
   11.52 -Goal "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)";
   11.53 -by (blast_tac (claset() addIs [genPrefix.prepend]) 1);
   11.54 -qed"Cons_genPrefix_Cons";
   11.55 -AddIffs [Cons_genPrefix_Cons];
   11.56 -
   11.57 -
   11.58 -(*** genPrefix is a partial order ***)
   11.59 -
   11.60 -Goalw [refl_def] "reflexive r ==> reflexive (genPrefix r)";
   11.61 -by Auto_tac;
   11.62 -by (induct_tac "x" 1);
   11.63 -by (blast_tac (claset() addIs [genPrefix.prepend]) 2);
   11.64 -by (blast_tac (claset() addIs [genPrefix.Nil]) 1);
   11.65 -qed "refl_genPrefix";
   11.66 -
   11.67 -Goal "reflexive r ==> (l,l) : genPrefix r";
   11.68 -by (etac ([refl_genPrefix,UNIV_I] MRS reflD) 1);
   11.69 -qed "genPrefix_refl";
   11.70 -
   11.71 -Addsimps [genPrefix_refl];
   11.72 -
   11.73 -Goal "r<=s ==> genPrefix r <= genPrefix s";
   11.74 -by (Clarify_tac 1);
   11.75 -by (etac genPrefix.induct 1);
   11.76 -by (auto_tac (claset() addIs [genPrefix.append], simpset()));
   11.77 -qed "genPrefix_mono";
   11.78 -
   11.79 -
   11.80 -(** Transitivity **)
   11.81 -
   11.82 -(*A lemma for proving genPrefix_trans_O*)
   11.83 -Goal "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r";
   11.84 -by (induct_tac "xs" 1);
   11.85 -by Auto_tac;
   11.86 -qed_spec_mp "append_genPrefix";
   11.87 -
   11.88 -(*Lemma proving transitivity and more*)
   11.89 -Goalw [prefix_def]
   11.90 -     "(x, y) : genPrefix r \
   11.91 -\     ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)";
   11.92 -by (etac genPrefix.induct 1);
   11.93 -  by (blast_tac (claset() addDs [append_genPrefix]) 3);
   11.94 - by (blast_tac (claset() addIs [genPrefix.prepend]) 2);
   11.95 -by (Blast_tac 1);
   11.96 -qed_spec_mp "genPrefix_trans_O";
   11.97 -
   11.98 -Goal "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |] \
   11.99 -\     ==> (x,z) : genPrefix r"; 
  11.100 -by (rtac (impOfSubs (trans_O_subset RS genPrefix_mono)) 1);
  11.101 - by (assume_tac 2);
  11.102 -by (blast_tac (claset() addIs [genPrefix_trans_O]) 1);
  11.103 -qed_spec_mp "genPrefix_trans";
  11.104 -
  11.105 -Goalw [prefix_def]
  11.106 -     "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r";
  11.107 -by (stac (R_O_Id RS sym) 1 THEN etac genPrefix_trans_O 1);
  11.108 -by (assume_tac 1);
  11.109 -qed_spec_mp "prefix_genPrefix_trans";
  11.110 -
  11.111 -Goalw [prefix_def]
  11.112 -     "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r";
  11.113 -by (stac (Id_O_R RS sym) 1 THEN etac genPrefix_trans_O 1);
  11.114 -by (assume_tac 1);
  11.115 -qed_spec_mp "genPrefix_prefix_trans";
  11.116 -
  11.117 -Goal "trans r ==> trans (genPrefix r)";
  11.118 -by (blast_tac (claset() addIs [transI, genPrefix_trans]) 1);
  11.119 -qed "trans_genPrefix";
  11.120 -
  11.121 -
  11.122 -(** Antisymmetry **)
  11.123 -
  11.124 -Goal "[| (xs,ys) : genPrefix r;  antisym r |] \
  11.125 -\     ==> (ys,xs) : genPrefix r --> xs = ys";
  11.126 -by (etac genPrefix.induct 1);
  11.127 -by (full_simp_tac (simpset() addsimps [antisym_def]) 2);
  11.128 -by (Blast_tac 2);
  11.129 -by (Blast_tac 1);
  11.130 -(*append case is hardest*)
  11.131 -by (Clarify_tac 1);
  11.132 -by (subgoal_tac "length zs = 0" 1);
  11.133 -by (Force_tac 1);
  11.134 -by (REPEAT (dtac genPrefix_length_le 1));
  11.135 -by (full_simp_tac (simpset() delsimps [length_0_conv]) 1);
  11.136 -qed_spec_mp "genPrefix_antisym";
  11.137 -
  11.138 -Goal "antisym r ==> antisym (genPrefix r)";
  11.139 -by (blast_tac (claset() addIs [antisymI, genPrefix_antisym]) 1);
  11.140 -qed "antisym_genPrefix";
  11.141 -
  11.142 -
  11.143 -(*** recursion equations ***)
  11.144 -
  11.145 -Goal "((xs, []) : genPrefix r) = (xs = [])";
  11.146 -by (induct_tac "xs" 1);
  11.147 -by (Blast_tac 2);
  11.148 -by (Simp_tac 1);
  11.149 -qed "genPrefix_Nil";
  11.150 -Addsimps [genPrefix_Nil];
  11.151 -
  11.152 -Goalw [refl_def]
  11.153 -    "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)";
  11.154 -by (induct_tac "xs" 1);
  11.155 -by (ALLGOALS Asm_simp_tac);
  11.156 -qed "same_genPrefix_genPrefix";
  11.157 -Addsimps [same_genPrefix_genPrefix];
  11.158 -
  11.159 -Goal "((xs, y#ys) : genPrefix r) = \
  11.160 -\     (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))";
  11.161 -by (case_tac "xs" 1);
  11.162 -by Auto_tac;
  11.163 -qed "genPrefix_Cons";
  11.164 -
  11.165 -Goal "[| reflexive r;  (xs,ys) : genPrefix r |] \
  11.166 -\     ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r";
  11.167 -by (etac genPrefix.induct 1);
  11.168 -by (ftac genPrefix_length_le 3);
  11.169 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2])));
  11.170 -qed "genPrefix_take_append";
  11.171 -
  11.172 -Goal "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |] \
  11.173 -\     ==>  (xs@zs, ys @ zs) : genPrefix r";
  11.174 -by (dtac genPrefix_take_append 1);
  11.175 -by (assume_tac 1);
  11.176 -by (asm_full_simp_tac (simpset() addsimps [take_all]) 1);
  11.177 -qed "genPrefix_append_both";
  11.178 -
  11.179 -
  11.180 -(*NOT suitable for rewriting since [y] has the form y#ys*)
  11.181 -Goal "xs @ y # ys = (xs @ [y]) @ ys";
  11.182 -by Auto_tac;
  11.183 -qed "append_cons_eq";
  11.184 -
  11.185 -Goal "[| (xs,ys) : genPrefix r;  reflexive r |] \
  11.186 -\     ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r";
  11.187 -by (etac genPrefix.induct 1);
  11.188 -by (Blast_tac 1);
  11.189 -by (Asm_simp_tac 1);
  11.190 -(*Append case is hardest*)
  11.191 -by (Asm_simp_tac 1);
  11.192 -by (forward_tac [genPrefix_length_le RS le_imp_less_or_eq] 1);
  11.193 -by (etac disjE 1);
  11.194 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [neq_Nil_conv, nth_append])));
  11.195 -by (blast_tac (claset() addIs [genPrefix.append]) 1);
  11.196 -by Auto_tac;
  11.197 -by (stac append_cons_eq 1);
  11.198 -by (blast_tac (claset() addIs [genPrefix_append_both, genPrefix.append]) 1);
  11.199 -val lemma = result() RS mp;
  11.200 -
  11.201 -Goal "[| (xs,ys) : genPrefix r;  length xs < length ys;  reflexive r |] \
  11.202 -\     ==> (xs @ [ys ! length xs], ys) : genPrefix r";
  11.203 -by (blast_tac (claset() addIs [lemma]) 1);
  11.204 -qed "append_one_genPrefix";
  11.205 -
  11.206 -
  11.207 -
  11.208 -
  11.209 -(** Proving the equivalence with Charpentier's definition **)
  11.210 -
  11.211 -Goal "ALL i ys. i < length xs \
  11.212 -\               --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r";
  11.213 -by (induct_tac "xs" 1);
  11.214 -by Auto_tac;
  11.215 -by (case_tac "i" 1);
  11.216 -by Auto_tac;
  11.217 -qed_spec_mp "genPrefix_imp_nth";
  11.218 -
  11.219 -Goal "ALL ys. length xs <= length ys  \
  11.220 -\     --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)  \
  11.221 -\     --> (xs, ys) : genPrefix r";
  11.222 -by (induct_tac "xs" 1);
  11.223 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, 
  11.224 -						all_conj_distrib])));
  11.225 -by (Clarify_tac 1);
  11.226 -by (case_tac "ys" 1);
  11.227 -by (ALLGOALS Force_tac);
  11.228 -qed_spec_mp "nth_imp_genPrefix";
  11.229 -
  11.230 -Goal "((xs,ys) : genPrefix r) = \
  11.231 -\     (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))";
  11.232 -by (blast_tac (claset() addIs [genPrefix_length_le, genPrefix_imp_nth,
  11.233 -			       nth_imp_genPrefix]) 1);
  11.234 -qed "genPrefix_iff_nth";
  11.235 -
  11.236 -
  11.237 -(** <= is a partial order: **)
  11.238 -
  11.239 -AddIffs [reflexive_Id, antisym_Id, trans_Id];
  11.240 -
  11.241 -Goalw [prefix_def] "xs <= (xs::'a list)";
  11.242 -by (Simp_tac 1);
  11.243 -qed "prefix_refl";
  11.244 -AddIffs[prefix_refl];
  11.245 -
  11.246 -Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
  11.247 -by (blast_tac (claset() addIs [genPrefix_trans]) 1);
  11.248 -qed "prefix_trans";
  11.249 -
  11.250 -Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
  11.251 -by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
  11.252 -qed "prefix_antisym";
  11.253 -
  11.254 -Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)";
  11.255 -by Auto_tac;
  11.256 -qed "prefix_less_le";
  11.257 -
  11.258 -(*Monotonicity of "set" operator WRT prefix*)
  11.259 -Goalw [prefix_def] "xs <= ys ==> set xs <= set ys";
  11.260 -by (etac genPrefix.induct 1);
  11.261 -by Auto_tac;
  11.262 -qed "set_mono";
  11.263 -
  11.264 -
  11.265 -(** recursion equations **)
  11.266 -
  11.267 -Goalw [prefix_def] "[] <= xs";
  11.268 -by (simp_tac (simpset() addsimps [Nil_genPrefix]) 1);
  11.269 -qed "Nil_prefix";
  11.270 -AddIffs[Nil_prefix];
  11.271 -
  11.272 -Goalw [prefix_def] "(xs <= []) = (xs = [])";
  11.273 -by (simp_tac (simpset() addsimps [genPrefix_Nil]) 1);
  11.274 -qed "prefix_Nil";
  11.275 -Addsimps [prefix_Nil];
  11.276 -
  11.277 -Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
  11.278 -by (Simp_tac 1);
  11.279 -qed"Cons_prefix_Cons";
  11.280 -Addsimps [Cons_prefix_Cons];
  11.281 -
  11.282 -Goalw [prefix_def] "(xs@ys <= xs@zs) = (ys <= zs)";
  11.283 -by (Simp_tac 1);
  11.284 -qed "same_prefix_prefix";
  11.285 -Addsimps [same_prefix_prefix];
  11.286 -
  11.287 -AddIffs   (* (xs@ys <= xs) = (ys <= []) *)
  11.288 - [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
  11.289 -
  11.290 -Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
  11.291 -by (etac genPrefix.append 1);
  11.292 -qed "prefix_appendI";
  11.293 -Addsimps [prefix_appendI];
  11.294 -
  11.295 -Goalw [prefix_def]
  11.296 -   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
  11.297 -by (simp_tac (simpset() addsimps [genPrefix_Cons]) 1);
  11.298 -by Auto_tac;
  11.299 -qed "prefix_Cons";
  11.300 -
  11.301 -Goalw [prefix_def]
  11.302 -  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
  11.303 -by (asm_simp_tac (simpset() addsimps [append_one_genPrefix]) 1);
  11.304 -qed "append_one_prefix";
  11.305 -
  11.306 -Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
  11.307 -by (etac genPrefix_length_le 1);
  11.308 -qed "prefix_length_le";
  11.309 -
  11.310 -Goalw [prefix_def] "xs<=ys ==> xs~=ys --> length xs < length ys";
  11.311 -by (etac genPrefix.induct 1);
  11.312 -by Auto_tac;
  11.313 -val lemma = result();
  11.314 -
  11.315 -Goalw [strict_prefix_def] "xs < ys ==> length xs < length ys";
  11.316 -by (blast_tac (claset() addIs [lemma RS mp]) 1);
  11.317 -qed "strict_prefix_length_less";
  11.318 -
  11.319 -Goal "mono length";
  11.320 -by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
  11.321 -qed "mono_length";
  11.322 -
  11.323 -(*Equivalence to the definition used in Lex/Prefix.thy*)
  11.324 -Goalw [prefix_def] "(xs <= zs) = (EX ys. zs = xs@ys)";
  11.325 -by (auto_tac (claset(),
  11.326 -	      simpset() addsimps [genPrefix_iff_nth, nth_append]));
  11.327 -by (res_inst_tac [("x", "drop (length xs) zs")] exI 1);
  11.328 -by (rtac nth_equalityI 1);
  11.329 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nth_append])));
  11.330 -qed "prefix_iff";
  11.331 -
  11.332 -Goal "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
  11.333 -by (simp_tac (simpset() addsimps [prefix_iff]) 1);
  11.334 -by (rtac iffI 1);
  11.335 - by (etac exE 1);
  11.336 - by (rename_tac "zs" 1);
  11.337 - by (res_inst_tac [("xs","zs")] rev_exhaust 1);
  11.338 -  by (Asm_full_simp_tac 1);
  11.339 - by (hyp_subst_tac 1);
  11.340 - by (asm_full_simp_tac (simpset() delsimps [append_assoc]
  11.341 -                                  addsimps [append_assoc RS sym])1);
  11.342 -by (Force_tac 1);
  11.343 -qed "prefix_snoc";
  11.344 -Addsimps [prefix_snoc];
  11.345 -
  11.346 -Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
  11.347 -by (res_inst_tac [("xs","zs")] rev_induct 1);
  11.348 - by (Force_tac 1);
  11.349 -by (asm_full_simp_tac (simpset() delsimps [append_assoc]
  11.350 -                                 addsimps [append_assoc RS sym])1);
  11.351 -by (Force_tac 1);
  11.352 -qed "prefix_append_iff";
  11.353 -
  11.354 -(*Although the prefix ordering is not linear, the prefixes of a list
  11.355 -  are linearly ordered.*)
  11.356 -Goal "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs";
  11.357 -by (res_inst_tac [("xs","zs")] rev_induct 1);
  11.358 -by Auto_tac;
  11.359 -qed_spec_mp "common_prefix_linear";
  11.360 -
  11.361 -
  11.362 -(*** pfixLe, pfixGe: properties inherited from the translations ***)
  11.363 -
  11.364 -(** pfixLe **)
  11.365 -
  11.366 -Goalw [refl_def, Le_def] "reflexive Le";
  11.367 -by Auto_tac;
  11.368 -qed "reflexive_Le";
  11.369 -
  11.370 -Goalw [antisym_def, Le_def] "antisym Le";
  11.371 -by Auto_tac;
  11.372 -qed "antisym_Le";
  11.373 -
  11.374 -Goalw [trans_def, Le_def] "trans Le";
  11.375 -by Auto_tac;
  11.376 -qed "trans_Le";
  11.377 -
  11.378 -AddIffs [reflexive_Le, antisym_Le, trans_Le];
  11.379 -
  11.380 -Goal "x pfixLe x";
  11.381 -by (Simp_tac 1);
  11.382 -qed "pfixLe_refl";
  11.383 -AddIffs[pfixLe_refl];
  11.384 -
  11.385 -Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
  11.386 -by (blast_tac (claset() addIs [genPrefix_trans]) 1);
  11.387 -qed "pfixLe_trans";
  11.388 -
  11.389 -Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
  11.390 -by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
  11.391 -qed "pfixLe_antisym";
  11.392 -
  11.393 -Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
  11.394 -by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
  11.395 -qed "prefix_imp_pfixLe";
  11.396 -
  11.397 -Goalw [refl_def, Ge_def] "reflexive Ge";
  11.398 -by Auto_tac;
  11.399 -qed "reflexive_Ge";
  11.400 -
  11.401 -Goalw [antisym_def, Ge_def] "antisym Ge";
  11.402 -by Auto_tac;
  11.403 -qed "antisym_Ge";
  11.404 -
  11.405 -Goalw [trans_def, Ge_def] "trans Ge";
  11.406 -by Auto_tac;
  11.407 -qed "trans_Ge";
  11.408 -
  11.409 -AddIffs [reflexive_Ge, antisym_Ge, trans_Ge];
  11.410 -
  11.411 -Goal "x pfixGe x";
  11.412 -by (Simp_tac 1);
  11.413 -qed "pfixGe_refl";
  11.414 -AddIffs[pfixGe_refl];
  11.415 -
  11.416 -Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
  11.417 -by (blast_tac (claset() addIs [genPrefix_trans]) 1);
  11.418 -qed "pfixGe_trans";
  11.419 -
  11.420 -Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
  11.421 -by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
  11.422 -qed "pfixGe_antisym";
  11.423 -
  11.424 -Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
  11.425 -by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
  11.426 -qed "prefix_imp_pfixGe";
  11.427 -
    12.1 --- a/src/HOL/UNITY/GenPrefix.thy	Thu Jan 30 18:08:09 2003 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,55 +0,0 @@
    12.4 -(*  Title:      HOL/UNITY/GenPrefix.thy
    12.5 -    ID:         $Id$
    12.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 -    Copyright   1999  University of Cambridge
    12.8 -
    12.9 -Charpentier's Generalized Prefix Relation
   12.10 -   (xs,ys) : genPrefix(r)
   12.11 -     if ys = xs' @ zs where length xs = length xs'
   12.12 -     and corresponding elements of xs, xs' are pairwise related by r
   12.13 -
   12.14 -Also overloads <= and < for lists!
   12.15 -
   12.16 -Based on Lex/Prefix
   12.17 -*)
   12.18 -
   12.19 -GenPrefix = Main +
   12.20 -
   12.21 -consts
   12.22 -  genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
   12.23 -
   12.24 -inductive "genPrefix(r)"
   12.25 -  intrs
   12.26 -    Nil     "([],[]) : genPrefix(r)"
   12.27 -
   12.28 -    prepend "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
   12.29 -	     (x#xs, y#ys) : genPrefix(r)"
   12.30 -
   12.31 -    append  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
   12.32 -
   12.33 -instance list :: (type)ord
   12.34 -
   12.35 -defs
   12.36 -  prefix_def        "xs <= zs  ==  (xs,zs) : genPrefix Id"
   12.37 -
   12.38 -  strict_prefix_def "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
   12.39 -  
   12.40 -
   12.41 -(*Constants for the <= and >= relations, used below in translations*)
   12.42 -constdefs
   12.43 -  Le :: "(nat*nat) set"
   12.44 -    "Le == {(x,y). x <= y}"
   12.45 -
   12.46 -  Ge :: "(nat*nat) set"
   12.47 -    "Ge == {(x,y). y <= x}"
   12.48 -
   12.49 -syntax
   12.50 -  pfixLe :: [nat list, nat list] => bool               (infixl "pfixLe" 50)
   12.51 -  pfixGe :: [nat list, nat list] => bool               (infixl "pfixGe" 50)
   12.52 -
   12.53 -translations
   12.54 -  "xs pfixLe ys" == "(xs,ys) : genPrefix Le"
   12.55 -
   12.56 -  "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"
   12.57 -
   12.58 -end
    13.1 --- a/src/HOL/UNITY/Guar.thy	Thu Jan 30 18:08:09 2003 +0100
    13.2 +++ b/src/HOL/UNITY/Guar.thy	Fri Jan 31 20:12:44 2003 +0100
    13.3 @@ -3,8 +3,6 @@
    13.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.5      Copyright   1999  University of Cambridge
    13.6  
    13.7 -Guarantees, etc.
    13.8 -
    13.9  From Chandy and Sanders, "Reasoning About Program Composition",
   13.10  Technical Report 2000-003, University of Florida, 2000.
   13.11  
   13.12 @@ -18,6 +16,8 @@
   13.13  
   13.14  *)
   13.15  
   13.16 +header{*Guarantees Specifications*}
   13.17 +
   13.18  theory Guar = Comp:
   13.19  
   13.20  instance program :: (type) order
   13.21 @@ -80,7 +80,7 @@
   13.22  
   13.23  
   13.24  (*** existential properties ***)
   13.25 -lemma ex1 [rule_format (no_asm)]: 
   13.26 +lemma ex1 [rule_format]: 
   13.27   "[| ex_prop X; finite GG |] ==>  
   13.28       GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
   13.29  apply (unfold ex_prop_def)
    14.1 --- a/src/HOL/UNITY/Lift_prog.thy	Thu Jan 30 18:08:09 2003 +0100
    14.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Fri Jan 31 20:12:44 2003 +0100
    14.3 @@ -6,6 +6,8 @@
    14.4  lift_prog, etc: replication of components and arrays of processes. 
    14.5  *)
    14.6  
    14.7 +header{*Replication of Components*}
    14.8 +
    14.9  theory Lift_prog = Rename:
   14.10  
   14.11  constdefs
   14.12 @@ -38,9 +40,7 @@
   14.13  declare insert_map_def [simp] delete_map_def [simp]
   14.14  
   14.15  lemma insert_map_inverse: "delete_map i (insert_map i x f) = f"
   14.16 -apply (rule ext)
   14.17 -apply (simp (no_asm))
   14.18 -done
   14.19 +by (rule ext, simp)
   14.20  
   14.21  lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
   14.22  apply (rule ext)
   14.23 @@ -50,13 +50,11 @@
   14.24  (*** Injectiveness proof ***)
   14.25  
   14.26  lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
   14.27 -apply (drule_tac x = i in fun_cong)
   14.28 -apply (simp (no_asm_use))
   14.29 -done
   14.30 +by (drule_tac x = i in fun_cong, simp)
   14.31  
   14.32  lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g"
   14.33  apply (drule_tac f = "delete_map i" in arg_cong)
   14.34 -apply (simp (no_asm_use) add: insert_map_inverse)
   14.35 +apply (simp add: insert_map_inverse)
   14.36  done
   14.37  
   14.38  lemma insert_map_inject':
   14.39 @@ -69,8 +67,7 @@
   14.40  lemma lift_map_eq_iff [iff]: 
   14.41       "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu')))  
   14.42        = (uu = uu' & insert_map i s f = insert_map i' s' f')"
   14.43 -apply (unfold lift_map_def, auto)
   14.44 -done
   14.45 +by (unfold lift_map_def, auto)
   14.46  
   14.47  (*The !!s allows the automatic splitting of the bound variable*)
   14.48  lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s"
   14.49 @@ -91,9 +88,7 @@
   14.50  done
   14.51  
   14.52  lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'"
   14.53 -apply (drule_tac f = "lift_map i" in arg_cong)
   14.54 -apply (simp (no_asm_use))
   14.55 -done
   14.56 +by (drule_tac f = "lift_map i" in arg_cong, simp)
   14.57  
   14.58  lemma surj_lift_map: "surj (lift_map i)"
   14.59  apply (rule surjI)
   14.60 @@ -101,8 +96,7 @@
   14.61  done
   14.62  
   14.63  lemma bij_lift_map [iff]: "bij (lift_map i)"
   14.64 -apply (simp (no_asm) add: bij_def inj_lift_map surj_lift_map)
   14.65 -done
   14.66 +by (simp add: bij_def inj_lift_map surj_lift_map)
   14.67  
   14.68  lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i"
   14.69  by (rule inv_equality, auto)
   14.70 @@ -115,8 +109,7 @@
   14.71  
   14.72  (*sub's main property!*)
   14.73  lemma sub_apply [simp]: "sub i f = f i"
   14.74 -apply (simp (no_asm) add: sub_def)
   14.75 -done
   14.76 +by (simp add: sub_def)
   14.77  
   14.78  (*** lift_set ***)
   14.79  
   14.80 @@ -131,7 +124,7 @@
   14.81  (*Do we really need both this one and its predecessor?*)
   14.82  lemma lift_set_iff2 [iff]:
   14.83       "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
   14.84 -by (simp (no_asm_simp) add: lift_set_def mem_rename_set_iff drop_map_def)
   14.85 +by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
   14.86  
   14.87  
   14.88  lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
   14.89 @@ -141,7 +134,7 @@
   14.90  
   14.91  lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
   14.92  apply (unfold lift_set_def)
   14.93 -apply (simp (no_asm_simp) add: image_Un)
   14.94 +apply (simp add: image_Un)
   14.95  done
   14.96  
   14.97  lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
   14.98 @@ -153,91 +146,71 @@
   14.99  (*** the lattice operations ***)
  14.100  
  14.101  lemma bij_lift [iff]: "bij (lift i)"
  14.102 -apply (simp (no_asm) add: lift_def)
  14.103 -done
  14.104 +by (simp add: lift_def)
  14.105  
  14.106  lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
  14.107 -apply (unfold lift_def)
  14.108 -apply (simp (no_asm_simp))
  14.109 -done
  14.110 +by (simp add: lift_def)
  14.111  
  14.112  lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
  14.113 -apply (unfold lift_def)
  14.114 -apply (simp (no_asm_simp))
  14.115 -done
  14.116 +by (simp add: lift_def)
  14.117  
  14.118  lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
  14.119 -apply (unfold lift_def)
  14.120 -apply (simp (no_asm_simp))
  14.121 -done
  14.122 +by (simp add: lift_def)
  14.123  
  14.124  (*** Safety: co, stable, invariant ***)
  14.125  
  14.126  lemma lift_constrains: 
  14.127       "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
  14.128 -apply (unfold lift_def lift_set_def)
  14.129 -apply (simp (no_asm_simp) add: rename_constrains)
  14.130 -done
  14.131 +by (simp add: lift_def lift_set_def rename_constrains)
  14.132  
  14.133  lemma lift_stable: 
  14.134       "(lift i F : stable (lift_set i A)) = (F : stable A)"
  14.135 -apply (unfold lift_def lift_set_def)
  14.136 -apply (simp (no_asm_simp) add: rename_stable)
  14.137 -done
  14.138 +by (simp add: lift_def lift_set_def rename_stable)
  14.139  
  14.140  lemma lift_invariant: 
  14.141       "(lift i F : invariant (lift_set i A)) = (F : invariant A)"
  14.142  apply (unfold lift_def lift_set_def)
  14.143 -apply (simp (no_asm_simp) add: rename_invariant)
  14.144 +apply (simp add: rename_invariant)
  14.145  done
  14.146  
  14.147  lemma lift_Constrains: 
  14.148       "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
  14.149  apply (unfold lift_def lift_set_def)
  14.150 -apply (simp (no_asm_simp) add: rename_Constrains)
  14.151 +apply (simp add: rename_Constrains)
  14.152  done
  14.153  
  14.154  lemma lift_Stable: 
  14.155       "(lift i F : Stable (lift_set i A)) = (F : Stable A)"
  14.156  apply (unfold lift_def lift_set_def)
  14.157 -apply (simp (no_asm_simp) add: rename_Stable)
  14.158 +apply (simp add: rename_Stable)
  14.159  done
  14.160  
  14.161  lemma lift_Always: 
  14.162       "(lift i F : Always (lift_set i A)) = (F : Always A)"
  14.163  apply (unfold lift_def lift_set_def)
  14.164 -apply (simp (no_asm_simp) add: rename_Always)
  14.165 +apply (simp add: rename_Always)
  14.166  done
  14.167  
  14.168  (*** Progress: transient, ensures ***)
  14.169  
  14.170  lemma lift_transient: 
  14.171       "(lift i F : transient (lift_set i A)) = (F : transient A)"
  14.172 -
  14.173 -apply (unfold lift_def lift_set_def)
  14.174 -apply (simp (no_asm_simp) add: rename_transient)
  14.175 -done
  14.176 +by (simp add: lift_def lift_set_def rename_transient)
  14.177  
  14.178  lemma lift_ensures: 
  14.179       "(lift i F : (lift_set i A) ensures (lift_set i B)) =  
  14.180        (F : A ensures B)"
  14.181 -apply (unfold lift_def lift_set_def)
  14.182 -apply (simp (no_asm_simp) add: rename_ensures)
  14.183 -done
  14.184 +by (simp add: lift_def lift_set_def rename_ensures)
  14.185  
  14.186  lemma lift_leadsTo: 
  14.187       "(lift i F : (lift_set i A) leadsTo (lift_set i B)) =  
  14.188        (F : A leadsTo B)"
  14.189 -apply (unfold lift_def lift_set_def)
  14.190 -apply (simp (no_asm_simp) add: rename_leadsTo)
  14.191 -done
  14.192 +by (simp add: lift_def lift_set_def rename_leadsTo)
  14.193  
  14.194  lemma lift_LeadsTo: 
  14.195       "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =   
  14.196        (F : A LeadsTo B)"
  14.197 -apply (unfold lift_def lift_set_def)
  14.198 -apply (simp (no_asm_simp) add: rename_LeadsTo)
  14.199 -done
  14.200 +by (simp add: lift_def lift_set_def rename_LeadsTo)
  14.201  
  14.202  
  14.203  (** guarantees **)
  14.204 @@ -245,10 +218,9 @@
  14.205  lemma lift_lift_guarantees_eq: 
  14.206       "(lift i F : (lift i ` X) guarantees (lift i ` Y)) =  
  14.207        (F : X guarantees Y)"
  14.208 -
  14.209  apply (unfold lift_def)
  14.210  apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
  14.211 -apply (simp (no_asm_simp) add: o_def)
  14.212 +apply (simp add: o_def)
  14.213  done
  14.214  
  14.215  lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =  
  14.216 @@ -266,14 +238,14 @@
  14.217    change function components other than i*)
  14.218  lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
  14.219  apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
  14.220 -apply (simp (no_asm_simp) add: lift_def rename_preserves)
  14.221 -apply (simp (no_asm_use) add: lift_map_def o_def split_def)
  14.222 +apply (simp add: lift_def rename_preserves)
  14.223 +apply (simp add: lift_map_def o_def split_def)
  14.224  done
  14.225  
  14.226  lemma delete_map_eqE':
  14.227       "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
  14.228  apply (drule_tac f = "insert_map i (g i) " in arg_cong)
  14.229 -apply (simp (no_asm_use) add: insert_map_delete_map_eq)
  14.230 +apply (simp add: insert_map_delete_map_eq)
  14.231  apply (erule exI)
  14.232  done
  14.233  
  14.234 @@ -302,7 +274,8 @@
  14.235  lemma preserves_snd_lift_stable:
  14.236       "[| F : preserves snd;  i~=j |]  
  14.237        ==> lift j F : stable (lift_set i (A <*> UNIV))"
  14.238 -apply (auto simp add: lift_def lift_set_def stable_def constrains_def rename_def extend_def mem_rename_set_iff)
  14.239 +apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
  14.240 +                      rename_def extend_def mem_rename_set_iff)
  14.241  apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
  14.242  apply (drule_tac x = i in fun_cong, auto)
  14.243  done
  14.244 @@ -315,7 +288,8 @@
  14.245       ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
  14.246  apply (case_tac "i=j")
  14.247  apply (simp add: lift_def lift_set_def rename_constrains)
  14.248 -apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], assumption)
  14.249 +apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
  14.250 +       assumption)
  14.251  apply (erule constrains_imp_subset [THEN lift_set_mono])
  14.252  done
  14.253  
  14.254 @@ -329,8 +303,9 @@
  14.255        (if i=j then insert_map i s f  
  14.256         else if i<j then insert_map j t (f(i:=s))  
  14.257         else insert_map j t (f(i - Suc 0 := s)))"
  14.258 -apply (rule ext)
  14.259 +apply (rule ext) 
  14.260  apply (simp split add: nat_diff_split) 
  14.261 + txt{*This simplification is VERY slow*}
  14.262  done
  14.263  
  14.264  lemma insert_map_eq_diff:
  14.265 @@ -354,7 +329,8 @@
  14.266            (i=j & F : transient (A <*> UNIV) | A={})"
  14.267  apply (case_tac "i=j")
  14.268  apply (auto simp add: lift_transient)
  14.269 -apply (auto simp add: lift_set_def lift_def transient_def rename_def extend_def Domain_extend_act)
  14.270 +apply (auto simp add: lift_set_def lift_def transient_def rename_def 
  14.271 +                      extend_def Domain_extend_act)
  14.272  apply (drule subsetD, blast, auto)
  14.273  apply (rename_tac s f uu s' f' uu')
  14.274  apply (subgoal_tac "f'=f & uu'=uu")
  14.275 @@ -387,7 +363,8 @@
  14.276            (if i=j then F : preserves (v o fst) else True)"
  14.277  apply (drule subset_preserves_o [THEN subsetD])
  14.278  apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
  14.279 -apply (simp cong del: if_weak_cong add: lift_map_def eq_commute split_def o_def, auto)
  14.280 +apply (auto cong del: if_weak_cong 
  14.281 +            simp add: lift_map_def eq_commute split_def o_def)
  14.282  done
  14.283  
  14.284  
  14.285 @@ -443,7 +420,7 @@
  14.286           ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]  
  14.287        ==> OK I (%i. lift i (F i))"
  14.288  apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
  14.289 -apply (simp (no_asm) add: Extend.AllowedActs_extend project_act_extend_act)
  14.290 +apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
  14.291  apply (rename_tac "act")
  14.292  apply (subgoal_tac
  14.293         "{(x, x'). \<exists>s f u s' f' u'. 
  14.294 @@ -468,6 +445,6 @@
  14.295  
  14.296  lemma lift_image_preserves:
  14.297       "lift i ` preserves v = preserves (v o drop_map i)"
  14.298 -by (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq)
  14.299 +by (simp add: rename_image_preserves lift_def inv_lift_map_eq)
  14.300  
  14.301  end
    15.1 --- a/src/HOL/UNITY/ListOrder.thy	Thu Jan 30 18:08:09 2003 +0100
    15.2 +++ b/src/HOL/UNITY/ListOrder.thy	Fri Jan 31 20:12:44 2003 +0100
    15.3 @@ -3,12 +3,425 @@
    15.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.5      Copyright   1998  University of Cambridge
    15.6  
    15.7 -Lists are partially ordered by the prefix relation
    15.8 +Lists are partially ordered by Charpentier's Generalized Prefix Relation
    15.9 +   (xs,ys) : genPrefix(r)
   15.10 +     if ys = xs' @ zs where length xs = length xs'
   15.11 +     and corresponding elements of xs, xs' are pairwise related by r
   15.12 +
   15.13 +Also overloads <= and < for lists!
   15.14 +
   15.15 +Based on Lex/Prefix
   15.16  *)
   15.17  
   15.18 -ListOrder = GenPrefix +
   15.19 +header {*The Prefix Ordering on Lists*}
   15.20 +
   15.21 +theory ListOrder = Main:
   15.22 +
   15.23 +consts
   15.24 +  genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
   15.25 +
   15.26 +inductive "genPrefix(r)"
   15.27 + intros
   15.28 +   Nil:     "([],[]) : genPrefix(r)"
   15.29 +
   15.30 +   prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
   15.31 +	     (x#xs, y#ys) : genPrefix(r)"
   15.32 +
   15.33 +   append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
   15.34 +
   15.35 +instance list :: (type)ord ..
   15.36 +
   15.37 +defs
   15.38 +  prefix_def:        "xs <= zs  ==  (xs,zs) : genPrefix Id"
   15.39 +
   15.40 +  strict_prefix_def: "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
   15.41 +  
   15.42 +
   15.43 +(*Constants for the <= and >= relations, used below in translations*)
   15.44 +constdefs
   15.45 +  Le :: "(nat*nat) set"
   15.46 +    "Le == {(x,y). x <= y}"
   15.47 +
   15.48 +  Ge :: "(nat*nat) set"
   15.49 +    "Ge == {(x,y). y <= x}"
   15.50 +
   15.51 +syntax
   15.52 +  pfixLe :: "[nat list, nat list] => bool"          (infixl "pfixLe" 50)
   15.53 +  pfixGe :: "[nat list, nat list] => bool"          (infixl "pfixGe" 50)
   15.54 +
   15.55 +translations
   15.56 +  "xs pfixLe ys" == "(xs,ys) : genPrefix Le"
   15.57 +
   15.58 +  "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"
   15.59 +
   15.60 +
   15.61 +subsection{*preliminary lemmas*}
   15.62 +
   15.63 +lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
   15.64 +by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
   15.65 +
   15.66 +lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"
   15.67 +by (erule genPrefix.induct, auto)
   15.68 +
   15.69 +lemma cdlemma:
   15.70 +     "[| (xs', ys'): genPrefix r |]  
   15.71 +      ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"
   15.72 +apply (erule genPrefix.induct, blast, blast)
   15.73 +apply (force intro: genPrefix.append)
   15.74 +done
   15.75 +
   15.76 +(*As usual converting it to an elimination rule is tiresome*)
   15.77 +lemma cons_genPrefixE [elim!]: 
   15.78 +     "[| (x#xs, zs): genPrefix r;   
   15.79 +         !!y ys. [| zs = y#ys;  (x,y) : r;  (xs, ys) : genPrefix r |] ==> P  
   15.80 +      |] ==> P"
   15.81 +by (drule cdlemma, simp, blast)
   15.82 +
   15.83 +lemma Cons_genPrefix_Cons [iff]:
   15.84 +     "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"
   15.85 +by (blast intro: genPrefix.prepend)
   15.86 +
   15.87 +
   15.88 +subsection{*genPrefix is a partial order*}
   15.89 +
   15.90 +lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)"
   15.91 +
   15.92 +apply (unfold refl_def, auto)
   15.93 +apply (induct_tac "x")
   15.94 +prefer 2 apply (blast intro: genPrefix.prepend)
   15.95 +apply (blast intro: genPrefix.Nil)
   15.96 +done
   15.97 +
   15.98 +lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r"
   15.99 +by (erule reflD [OF refl_genPrefix UNIV_I])
  15.100 +
  15.101 +lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
  15.102 +apply clarify
  15.103 +apply (erule genPrefix.induct)
  15.104 +apply (auto intro: genPrefix.append)
  15.105 +done
  15.106 +
  15.107 +
  15.108 +(** Transitivity **)
  15.109 +
  15.110 +(*A lemma for proving genPrefix_trans_O*)
  15.111 +lemma append_genPrefix [rule_format]:
  15.112 +     "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
  15.113 +by (induct_tac "xs", auto)
  15.114 +
  15.115 +(*Lemma proving transitivity and more*)
  15.116 +lemma genPrefix_trans_O [rule_format]: 
  15.117 +     "(x, y) : genPrefix r  
  15.118 +      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
  15.119 +apply (erule genPrefix.induct)
  15.120 +  prefer 3 apply (blast dest: append_genPrefix)
  15.121 + prefer 2 apply (blast intro: genPrefix.prepend, blast)
  15.122 +done
  15.123 +
  15.124 +lemma genPrefix_trans [rule_format]:
  15.125 +     "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
  15.126 +      ==> (x,z) : genPrefix r"
  15.127 +apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
  15.128 + apply assumption
  15.129 +apply (blast intro: genPrefix_trans_O)
  15.130 +done
  15.131 +
  15.132 +lemma prefix_genPrefix_trans [rule_format]: 
  15.133 +     "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
  15.134 +apply (unfold prefix_def)
  15.135 +apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
  15.136 +done
  15.137 +
  15.138 +lemma genPrefix_prefix_trans [rule_format]: 
  15.139 +     "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
  15.140 +apply (unfold prefix_def)
  15.141 +apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
  15.142 +done
  15.143 +
  15.144 +lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
  15.145 +by (blast intro: transI genPrefix_trans)
  15.146 +
  15.147 +
  15.148 +(** Antisymmetry **)
  15.149 +
  15.150 +lemma genPrefix_antisym [rule_format]:
  15.151 +     "[| (xs,ys) : genPrefix r;  antisym r |]  
  15.152 +      ==> (ys,xs) : genPrefix r --> xs = ys"
  15.153 +apply (erule genPrefix.induct)
  15.154 +  txt{*Base case*}
  15.155 +  apply blast
  15.156 + txt{*prepend case*}
  15.157 + apply (simp add: antisym_def)
  15.158 +txt{*append case is the hardest*}
  15.159 +apply clarify
  15.160 +apply (subgoal_tac "length zs = 0", force)
  15.161 +apply (drule genPrefix_length_le)+
  15.162 +apply (simp del: length_0_conv)
  15.163 +done
  15.164 +
  15.165 +lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
  15.166 +by (blast intro: antisymI genPrefix_antisym)
  15.167 +
  15.168 +
  15.169 +subsection{*recursion equations*}
  15.170 +
  15.171 +lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
  15.172 +apply (induct_tac "xs")
  15.173 +prefer 2 apply blast
  15.174 +apply simp
  15.175 +done
  15.176 +
  15.177 +lemma same_genPrefix_genPrefix [simp]: 
  15.178 +    "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
  15.179 +apply (unfold refl_def)
  15.180 +apply (induct_tac "xs")
  15.181 +apply (simp_all (no_asm_simp))
  15.182 +done
  15.183 +
  15.184 +lemma genPrefix_Cons:
  15.185 +     "((xs, y#ys) : genPrefix r) =  
  15.186 +      (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
  15.187 +by (case_tac "xs", auto)
  15.188 +
  15.189 +lemma genPrefix_take_append:
  15.190 +     "[| reflexive r;  (xs,ys) : genPrefix r |]  
  15.191 +      ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
  15.192 +apply (erule genPrefix.induct)
  15.193 +apply (frule_tac [3] genPrefix_length_le)
  15.194 +apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
  15.195 +done
  15.196 +
  15.197 +lemma genPrefix_append_both:
  15.198 +     "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
  15.199 +      ==>  (xs@zs, ys @ zs) : genPrefix r"
  15.200 +apply (drule genPrefix_take_append, assumption)
  15.201 +apply (simp add: take_all)
  15.202 +done
  15.203 +
  15.204 +
  15.205 +(*NOT suitable for rewriting since [y] has the form y#ys*)
  15.206 +lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
  15.207 +by auto
  15.208 +
  15.209 +lemma aolemma:
  15.210 +     "[| (xs,ys) : genPrefix r;  reflexive r |]  
  15.211 +      ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
  15.212 +apply (erule genPrefix.induct)
  15.213 +  apply blast
  15.214 + apply simp
  15.215 +txt{*Append case is hardest*}
  15.216 +apply simp
  15.217 +apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
  15.218 +apply (erule disjE)
  15.219 +apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
  15.220 +apply (blast intro: genPrefix.append, auto)
  15.221 +apply (subst append_cons_eq)
  15.222 +apply (blast intro: genPrefix_append_both genPrefix.append)
  15.223 +done
  15.224 +
  15.225 +lemma append_one_genPrefix:
  15.226 +     "[| (xs,ys) : genPrefix r;  length xs < length ys;  reflexive r |]  
  15.227 +      ==> (xs @ [ys ! length xs], ys) : genPrefix r"
  15.228 +by (blast intro: aolemma [THEN mp])
  15.229 +
  15.230 +
  15.231 +(** Proving the equivalence with Charpentier's definition **)
  15.232 +
  15.233 +lemma genPrefix_imp_nth [rule_format]:
  15.234 +     "ALL i ys. i < length xs  
  15.235 +                --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
  15.236 +apply (induct_tac "xs", auto)
  15.237 +apply (case_tac "i", auto)
  15.238 +done
  15.239 +
  15.240 +lemma nth_imp_genPrefix [rule_format]:
  15.241 +     "ALL ys. length xs <= length ys   
  15.242 +      --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
  15.243 +      --> (xs, ys) : genPrefix r"
  15.244 +apply (induct_tac "xs")
  15.245 +apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
  15.246 +apply clarify
  15.247 +apply (case_tac "ys")
  15.248 +apply (force+)
  15.249 +done
  15.250 +
  15.251 +lemma genPrefix_iff_nth:
  15.252 +     "((xs,ys) : genPrefix r) =  
  15.253 +      (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
  15.254 +apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
  15.255 +done
  15.256 +
  15.257 +
  15.258 +subsection{*The type of lists is partially ordered*}
  15.259 +
  15.260 +declare reflexive_Id [iff] 
  15.261 +        antisym_Id [iff] 
  15.262 +        trans_Id [iff]
  15.263 +
  15.264 +lemma prefix_refl [iff]: "xs <= (xs::'a list)"
  15.265 +by (simp add: prefix_def)
  15.266 +
  15.267 +lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
  15.268 +apply (unfold prefix_def)
  15.269 +apply (blast intro: genPrefix_trans)
  15.270 +done
  15.271 +
  15.272 +lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
  15.273 +apply (unfold prefix_def)
  15.274 +apply (blast intro: genPrefix_antisym)
  15.275 +done
  15.276 +
  15.277 +lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"
  15.278 +by (unfold strict_prefix_def, auto)
  15.279  
  15.280  instance list :: (type) order
  15.281 -    (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)
  15.282 +  by (intro_classes,
  15.283 +      (assumption | rule prefix_refl prefix_trans prefix_antisym
  15.284 +                     prefix_less_le)+)
  15.285 +
  15.286 +(*Monotonicity of "set" operator WRT prefix*)
  15.287 +lemma set_mono: "xs <= ys ==> set xs <= set ys"
  15.288 +apply (unfold prefix_def)
  15.289 +apply (erule genPrefix.induct, auto)
  15.290 +done
  15.291 +
  15.292 +
  15.293 +(** recursion equations **)
  15.294 +
  15.295 +lemma Nil_prefix [iff]: "[] <= xs"
  15.296 +apply (unfold prefix_def)
  15.297 +apply (simp add: Nil_genPrefix)
  15.298 +done
  15.299 +
  15.300 +lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
  15.301 +apply (unfold prefix_def)
  15.302 +apply (simp add: genPrefix_Nil)
  15.303 +done
  15.304 +
  15.305 +lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
  15.306 +by (simp add: prefix_def)
  15.307 +
  15.308 +lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
  15.309 +by (simp add: prefix_def)
  15.310 +
  15.311 +lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
  15.312 +by (insert same_prefix_prefix [of xs ys "[]"], simp)
  15.313 +
  15.314 +lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
  15.315 +apply (unfold prefix_def)
  15.316 +apply (erule genPrefix.append)
  15.317 +done
  15.318 +
  15.319 +lemma prefix_Cons: 
  15.320 +   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
  15.321 +by (simp add: prefix_def genPrefix_Cons)
  15.322 +
  15.323 +lemma append_one_prefix: 
  15.324 +  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
  15.325 +apply (unfold prefix_def)
  15.326 +apply (simp add: append_one_genPrefix)
  15.327 +done
  15.328 +
  15.329 +lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
  15.330 +apply (unfold prefix_def)
  15.331 +apply (erule genPrefix_length_le)
  15.332 +done
  15.333 +
  15.334 +lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
  15.335 +apply (unfold prefix_def)
  15.336 +apply (erule genPrefix.induct, auto)
  15.337 +done
  15.338 +
  15.339 +lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
  15.340 +apply (unfold strict_prefix_def)
  15.341 +apply (blast intro: splemma [THEN mp])
  15.342 +done
  15.343 +
  15.344 +lemma mono_length: "mono length"
  15.345 +by (blast intro: monoI prefix_length_le)
  15.346 +
  15.347 +(*Equivalence to the definition used in Lex/Prefix.thy*)
  15.348 +lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
  15.349 +apply (unfold prefix_def)
  15.350 +apply (auto simp add: genPrefix_iff_nth nth_append)
  15.351 +apply (rule_tac x = "drop (length xs) zs" in exI)
  15.352 +apply (rule nth_equalityI)
  15.353 +apply (simp_all (no_asm_simp) add: nth_append)
  15.354 +done
  15.355 +
  15.356 +lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
  15.357 +apply (simp add: prefix_iff)
  15.358 +apply (rule iffI)
  15.359 + apply (erule exE)
  15.360 + apply (rename_tac "zs")
  15.361 + apply (rule_tac xs = zs in rev_exhaust)
  15.362 +  apply simp
  15.363 + apply clarify
  15.364 + apply (simp del: append_assoc add: append_assoc [symmetric], force)
  15.365 +done
  15.366 +
  15.367 +lemma prefix_append_iff:
  15.368 +     "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
  15.369 +apply (rule_tac xs = zs in rev_induct)
  15.370 + apply force
  15.371 +apply (simp del: append_assoc add: append_assoc [symmetric], force)
  15.372 +done
  15.373 +
  15.374 +(*Although the prefix ordering is not linear, the prefixes of a list
  15.375 +  are linearly ordered.*)
  15.376 +lemma common_prefix_linear [rule_format]:
  15.377 +     "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
  15.378 +by (rule_tac xs = zs in rev_induct, auto)
  15.379 +
  15.380 +
  15.381 +subsection{*pfixLe, pfixGe: properties inherited from the translations*}
  15.382 +
  15.383 +(** pfixLe **)
  15.384 +
  15.385 +lemma reflexive_Le [iff]: "reflexive Le"
  15.386 +by (unfold refl_def Le_def, auto)
  15.387 +
  15.388 +lemma antisym_Le [iff]: "antisym Le"
  15.389 +by (unfold antisym_def Le_def, auto)
  15.390 +
  15.391 +lemma trans_Le [iff]: "trans Le"
  15.392 +by (unfold trans_def Le_def, auto)
  15.393 +
  15.394 +lemma pfixLe_refl [iff]: "x pfixLe x"
  15.395 +by simp
  15.396 +
  15.397 +lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
  15.398 +by (blast intro: genPrefix_trans)
  15.399 +
  15.400 +lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
  15.401 +by (blast intro: genPrefix_antisym)
  15.402 +
  15.403 +lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
  15.404 +apply (unfold prefix_def Le_def)
  15.405 +apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
  15.406 +done
  15.407 +
  15.408 +lemma reflexive_Ge [iff]: "reflexive Ge"
  15.409 +by (unfold refl_def Ge_def, auto)
  15.410 +
  15.411 +lemma antisym_Ge [iff]: "antisym Ge"
  15.412 +by (unfold antisym_def Ge_def, auto)
  15.413 +
  15.414 +lemma trans_Ge [iff]: "trans Ge"
  15.415 +by (unfold trans_def Ge_def, auto)
  15.416 +
  15.417 +lemma pfixGe_refl [iff]: "x pfixGe x"
  15.418 +by simp
  15.419 +
  15.420 +lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
  15.421 +by (blast intro: genPrefix_trans)
  15.422 +
  15.423 +lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
  15.424 +by (blast intro: genPrefix_antisym)
  15.425 +
  15.426 +lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
  15.427 +apply (unfold prefix_def Ge_def)
  15.428 +apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
  15.429 +done
  15.430  
  15.431  end
    16.1 --- a/src/HOL/UNITY/PPROD.thy	Thu Jan 30 18:08:09 2003 +0100
    16.2 +++ b/src/HOL/UNITY/PPROD.thy	Fri Jan 31 20:12:44 2003 +0100
    16.3 @@ -59,7 +59,8 @@
    16.4  
    16.5  (** Safety & Progress: but are they used anywhere? **)
    16.6  
    16.7 -lemma PLam_constrains: "[| i : I;  ALL j. F j : preserves snd |] ==>   
    16.8 +lemma PLam_constrains: 
    16.9 +     "[| i : I;  ALL j. F j : preserves snd |] ==>   
   16.10        (PLam I F : (lift_set i (A <*> UNIV)) co  
   16.11                    (lift_set i (B <*> UNIV)))  =   
   16.12        (F i : (A <*> UNIV) co (B <*> UNIV))"
   16.13 @@ -69,25 +70,29 @@
   16.14  apply (blast intro: constrains_imp_lift_constrains)
   16.15  done
   16.16  
   16.17 -lemma PLam_stable: "[| i : I;  ALL j. F j : preserves snd |]   
   16.18 +lemma PLam_stable: 
   16.19 +     "[| i : I;  ALL j. F j : preserves snd |]   
   16.20        ==> (PLam I F : stable (lift_set i (A <*> UNIV))) =  
   16.21            (F i : stable (A <*> UNIV))"
   16.22  apply (simp (no_asm_simp) add: stable_def PLam_constrains)
   16.23  done
   16.24  
   16.25 -lemma PLam_transient: "i : I ==>  
   16.26 +lemma PLam_transient: 
   16.27 +     "i : I ==>  
   16.28      PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
   16.29  apply (simp (no_asm_simp) add: JN_transient PLam_def)
   16.30  done
   16.31  
   16.32  (*This holds because the F j cannot change (lift_set i)*)
   16.33 -lemma PLam_ensures: "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);   
   16.34 +lemma PLam_ensures: 
   16.35 +     "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);   
   16.36           ALL j. F j : preserves snd |] ==>   
   16.37        PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
   16.38  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])
   16.39  done
   16.40  
   16.41 -lemma PLam_leadsTo_Basis: "[| i : I;   
   16.42 +lemma PLam_leadsTo_Basis: 
   16.43 +     "[| i : I;   
   16.44           F i : ((A <*> UNIV) - (B <*> UNIV)) co  
   16.45                 ((A <*> UNIV) Un (B <*> UNIV));   
   16.46           F i : transient ((A <*> UNIV) - (B <*> UNIV));   
   16.47 @@ -99,7 +104,8 @@
   16.48  
   16.49  (** invariant **)
   16.50  
   16.51 -lemma invariant_imp_PLam_invariant: "[| F i : invariant (A <*> UNIV);  i : I;   
   16.52 +lemma invariant_imp_PLam_invariant: 
   16.53 +     "[| F i : invariant (A <*> UNIV);  i : I;   
   16.54           ALL j. F j : preserves snd |]  
   16.55        ==> PLam I F : invariant (lift_set i (A <*> UNIV))"
   16.56  by (auto simp add: PLam_stable invariant_def)
   16.57 @@ -143,21 +149,24 @@
   16.58  
   16.59  (**UNUSED
   16.60      (*The f0 premise ensures that the product is well-defined.*)
   16.61 -    lemma PLam_invariant_imp_invariant: "[| PLam I F : invariant (lift_set i A);  i : I;   
   16.62 +    lemma PLam_invariant_imp_invariant: 
   16.63 +     "[| PLam I F : invariant (lift_set i A);  i : I;   
   16.64               f0: Init (PLam I F) |] ==> F i : invariant A"
   16.65      apply (auto simp add: invariant_def)
   16.66      apply (drule_tac c = "f0 (i:=x) " in subsetD)
   16.67      apply auto
   16.68      done
   16.69  
   16.70 -    lemma PLam_invariant: "[| i : I;  f0: Init (PLam I F) |]  
   16.71 +    lemma PLam_invariant: 
   16.72 +     "[| i : I;  f0: Init (PLam I F) |]  
   16.73            ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
   16.74      apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
   16.75      done
   16.76  
   16.77      (*The f0 premise isn't needed if F is a constant program because then
   16.78        we get an initial state by replicating that of F*)
   16.79 -    lemma reachable_PLam: "i : I  
   16.80 +    lemma reachable_PLam: 
   16.81 +     "i : I  
   16.82            ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
   16.83      apply (auto simp add: invariant_def)
   16.84      done
   16.85 @@ -173,16 +182,17 @@
   16.86      done
   16.87  
   16.88      (*Result to justify a re-organization of this file*)
   16.89 -    lemma ??unknown??: "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
   16.90 -    apply auto
   16.91 -    result()
   16.92 +    lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
   16.93 +    by auto
   16.94  
   16.95 -    lemma reachable_PLam_subset1: "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
   16.96 +    lemma reachable_PLam_subset1: 
   16.97 +     "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
   16.98      apply (force dest!: reachable_PLam)
   16.99      done
  16.100  
  16.101      (*simplify using reachable_lift??*)
  16.102 -    lemma reachable_lift_Join_PLam [rule_format (no_asm)]: "[| i ~: I;  A : reachable (F i) |]      
  16.103 +    lemma reachable_lift_Join_PLam [rule_format]:
  16.104 +      "[| i ~: I;  A : reachable (F i) |]      
  16.105         ==> ALL f. f : reachable (PLam I F)       
  16.106                    --> f(i:=A) : reachable (lift i (F i) Join PLam I F)"
  16.107      apply (erule reachable.induct)
  16.108 @@ -212,14 +222,16 @@
  16.109  
  16.110      (*The index set must be finite: otherwise infinitely many copies of F can
  16.111        perform actions, and PLam can never catch up in finite time.*)
  16.112 -    lemma reachable_PLam_subset2: "finite I  
  16.113 +    lemma reachable_PLam_subset2: 
  16.114 +     "finite I  
  16.115            ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
  16.116      apply (erule finite_induct)
  16.117      apply (simp (no_asm))
  16.118      apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
  16.119      done
  16.120  
  16.121 -    lemma reachable_PLam_eq: "finite I ==>  
  16.122 +    lemma reachable_PLam_eq: 
  16.123 +     "finite I ==>  
  16.124            reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
  16.125      apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
  16.126      done
  16.127 @@ -227,7 +239,8 @@
  16.128  
  16.129      (** Co **)
  16.130  
  16.131 -    lemma Constrains_imp_PLam_Constrains: "[| F i : A Co B;  i: I;  finite I |]   
  16.132 +    lemma Constrains_imp_PLam_Constrains: 
  16.133 +     "[| F i : A Co B;  i: I;  finite I |]   
  16.134            ==> PLam I F : (lift_set i A) Co (lift_set i B)"
  16.135      apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
  16.136      apply (auto simp add: constrains_def PLam_def)
  16.137 @@ -236,13 +249,15 @@
  16.138  
  16.139  
  16.140  
  16.141 -    lemma PLam_Constrains: "[| i: I;  finite I;  f0: Init (PLam I F) |]   
  16.142 +    lemma PLam_Constrains: 
  16.143 +     "[| i: I;  finite I;  f0: Init (PLam I F) |]   
  16.144            ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =   
  16.145                (F i : A Co B)"
  16.146      apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
  16.147      done
  16.148  
  16.149 -    lemma PLam_Stable: "[| i: I;  finite I;  f0: Init (PLam I F) |]   
  16.150 +    lemma PLam_Stable: 
  16.151 +     "[| i: I;  finite I;  f0: Init (PLam I F) |]   
  16.152            ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
  16.153      apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
  16.154      done
  16.155 @@ -250,13 +265,15 @@
  16.156  
  16.157      (** const_PLam (no dependence on i) doesn't require the f0 premise **)
  16.158  
  16.159 -    lemma const_PLam_Constrains: "[| i: I;  finite I |]   
  16.160 +    lemma const_PLam_Constrains: 
  16.161 +     "[| i: I;  finite I |]   
  16.162            ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =   
  16.163                (F : A Co B)"
  16.164      apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
  16.165      done
  16.166  
  16.167 -    lemma const_PLam_Stable: "[| i: I;  finite I |]   
  16.168 +    lemma const_PLam_Stable: 
  16.169 +     "[| i: I;  finite I |]   
  16.170            ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
  16.171      apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
  16.172      done
    17.1 --- a/src/HOL/UNITY/Project.thy	Thu Jan 30 18:08:09 2003 +0100
    17.2 +++ b/src/HOL/UNITY/Project.thy	Fri Jan 31 20:12:44 2003 +0100
    17.3 @@ -8,6 +8,8 @@
    17.4  Inheritance of GUARANTEES properties under extension
    17.5  *)
    17.6  
    17.7 +header{*Projections of State Sets*}
    17.8 +
    17.9  theory Project = Extend:
   17.10  
   17.11  constdefs
   17.12 @@ -32,10 +34,10 @@
   17.13  done
   17.14  
   17.15  
   17.16 -(** Safety **)
   17.17 +subsection{*Safety*}
   17.18  
   17.19  (*used below to prove Join_project_ensures*)
   17.20 -lemma (in Extend) project_unless [rule_format (no_asm)]:
   17.21 +lemma (in Extend) project_unless [rule_format]:
   17.22       "[| G : stable C;  project h C G : A unless B |]  
   17.23        ==> G : (C Int extend_set h A) unless (extend_set h B)"
   17.24  apply (simp add: unless_def project_constrains)
   17.25 @@ -98,7 +100,7 @@
   17.26  by (simp add: project_constrains extend_constrains)
   17.27  
   17.28  
   17.29 -(*** "projecting" and union/intersection (no converses) ***)
   17.30 +subsection{*"projecting" and union/intersection (no converses)*}
   17.31  
   17.32  lemma projecting_Int: 
   17.33       "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
   17.34 @@ -198,7 +200,7 @@
   17.35  by (force simp only: extending_def Join_project_increasing)
   17.36  
   17.37  
   17.38 -(** Reachability and project **)
   17.39 +subsection{*Reachability and project*}
   17.40  
   17.41  (*In practice, C = reachable(...): the inclusion is equality*)
   17.42  lemma (in Extend) reachable_imp_reachable_project:
   17.43 @@ -247,7 +249,7 @@
   17.44  done
   17.45  
   17.46  
   17.47 -(** Converse results for weak safety: benefits of the argument C *)
   17.48 +subsection{*Converse results for weak safety: benefits of the argument C *}
   17.49  
   17.50  (*In practice, C = reachable(...): the inclusion is equality*)
   17.51  lemma (in Extend) reachable_project_imp_reachable:
   17.52 @@ -329,8 +331,8 @@
   17.53  apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
   17.54  done
   17.55  
   17.56 -(** A lot of redundant theorems: all are proved to facilitate reasoning
   17.57 -    about guarantees. **)
   17.58 +subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
   17.59 +    about guarantees.*}
   17.60  
   17.61  lemma (in Extend) projecting_Constrains: 
   17.62       "projecting (%G. reachable (extend h F Join G)) h F  
   17.63 @@ -390,9 +392,9 @@
   17.64  done
   17.65  
   17.66  
   17.67 -(*** leadsETo in the precondition (??) ***)
   17.68 +subsection{*leadsETo in the precondition (??)*}
   17.69  
   17.70 -(** transient **)
   17.71 +subsubsection{*transient*}
   17.72  
   17.73  lemma (in Extend) transient_extend_set_imp_project_transient: 
   17.74       "[| G : transient (C Int extend_set h A);  G : stable C |]   
   17.75 @@ -422,7 +424,7 @@
   17.76  done
   17.77  
   17.78  
   17.79 -(** ensures -- a primitive combining progress with safety **)
   17.80 +subsubsection{*ensures -- a primitive combining progress with safety*}
   17.81  
   17.82  (*Used to prove project_leadsETo_I*)
   17.83  lemma (in Extend) ensures_extend_set_imp_project_ensures:
   17.84 @@ -456,7 +458,7 @@
   17.85  done
   17.86  
   17.87  (*Used to prove project_leadsETo_D*)
   17.88 -lemma (in Extend) Join_project_ensures [rule_format (no_asm)]:
   17.89 +lemma (in Extend) Join_project_ensures [rule_format]:
   17.90       "[| project h C G ~: transient (A-B) | A<=B;   
   17.91           extend h F Join G : stable C;   
   17.92           F Join project h C G : A ensures B |]  
   17.93 @@ -470,8 +472,8 @@
   17.94              simp add: ensures_def Join_transient)
   17.95  done
   17.96  
   17.97 -(** Lemma useful for both STRONG and WEAK progress, but the transient
   17.98 -    condition's very strong **)
   17.99 +text{*Lemma useful for both STRONG and WEAK progress, but the transient
  17.100 +    condition's very strong*}
  17.101  
  17.102  (*The strange induction formula allows induction over the leadsTo
  17.103    assumption's non-atomic precondition*)
  17.104 @@ -505,7 +507,7 @@
  17.105                                    project_set_reachable_extend_eq)
  17.106  
  17.107  
  17.108 -(*** Towards project_Ensures_D ***)
  17.109 +subsection{*Towards the theorem @{text project_Ensures_D}*}
  17.110  
  17.111  
  17.112  lemma (in Extend) act_subset_imp_project_act_subset: 
  17.113 @@ -544,7 +546,7 @@
  17.114  apply (force simp add: split_extended_all)
  17.115  done
  17.116  
  17.117 -lemma (in Extend) project_unless2 [rule_format (no_asm)]:
  17.118 +lemma (in Extend) project_unless2 [rule_format]:
  17.119       "[| G : stable C;  project h C G : (project_set h C Int A) unless B |]  
  17.120        ==> G : (C Int extend_set h A) unless (extend_set h B)"
  17.121  by (auto dest: stable_constrains_Int intro: constrains_weaken
  17.122 @@ -589,7 +591,7 @@
  17.123  done
  17.124  
  17.125  
  17.126 -(*** Guarantees ***)
  17.127 +subsection{*Guarantees*}
  17.128  
  17.129  lemma (in Extend) project_act_Restrict_subset_project_act:
  17.130       "project_act h (Restrict C act) <= project_act h act"
  17.131 @@ -641,9 +643,9 @@
  17.132  (*It seems that neither "guarantees" law can be proved from the other.*)
  17.133  
  17.134  
  17.135 -(*** guarantees corollaries ***)
  17.136 +subsection{*guarantees corollaries*}
  17.137  
  17.138 -(** Some could be deleted: the required versions are easy to prove **)
  17.139 +subsubsection{*Some could be deleted: the required versions are easy to prove*}
  17.140  
  17.141  lemma (in Extend) extend_guar_increasing:
  17.142       "[| F : UNIV guarantees increasing func;   
  17.143 @@ -682,8 +684,8 @@
  17.144  done
  17.145  
  17.146  
  17.147 -(** Guarantees with a leadsTo postcondition 
  17.148 -    THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
  17.149 +subsubsection{*Guarantees with a leadsTo postcondition 
  17.150 +     ALL TOO WEAK because G can't affect F's variables at all**)
  17.151  
  17.152  lemma (in Extend) project_leadsTo_D:
  17.153       "[| F Join project h UNIV G : A leadsTo B;     
    18.1 --- a/src/HOL/UNITY/Rename.thy	Thu Jan 30 18:08:09 2003 +0100
    18.2 +++ b/src/HOL/UNITY/Rename.thy	Fri Jan 31 20:12:44 2003 +0100
    18.3 @@ -2,9 +2,9 @@
    18.4      ID:         $Id$
    18.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.6      Copyright   2000  University of Cambridge
    18.7 +*)
    18.8  
    18.9 -Renaming of state sets
   18.10 -*)
   18.11 +header{*Renaming of State Sets*}
   18.12  
   18.13  theory Rename = Extend:
   18.14  
   18.15 @@ -42,7 +42,7 @@
   18.16  by (simp add: rename_def)
   18.17  
   18.18  
   18.19 -(*** inverse properties ***)
   18.20 +subsection{*inverse properties*}
   18.21  
   18.22  lemma extend_set_inv: 
   18.23       "bij h  
   18.24 @@ -166,7 +166,7 @@
   18.25  by (blast intro: bij_rename bij_rename_imp_bij)
   18.26  
   18.27  
   18.28 -(*** the lattice operations ***)
   18.29 +subsection{*the lattice operations*}
   18.30  
   18.31  lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
   18.32  by (simp add: rename_def Extend.extend_SKIP)
   18.33 @@ -180,7 +180,7 @@
   18.34  by (simp add: rename_def Extend.extend_JN)
   18.35  
   18.36  
   18.37 -(*** Strong Safety: co, stable ***)
   18.38 +subsection{*Strong Safety: co, stable*}
   18.39  
   18.40  lemma rename_constrains: 
   18.41       "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
   18.42 @@ -205,7 +205,7 @@
   18.43  done
   18.44  
   18.45  
   18.46 -(*** Weak Safety: Co, Stable ***)
   18.47 +subsection{*Weak Safety: Co, Stable*}
   18.48  
   18.49  lemma reachable_rename_eq: 
   18.50       "bij h ==> reachable (rename h F) = h ` (reachable F)"
   18.51 @@ -230,7 +230,7 @@
   18.52                bij_is_surj [THEN surj_f_inv_f])
   18.53  
   18.54  
   18.55 -(*** Progress: transient, ensures ***)
   18.56 +subsection{*Progress: transient, ensures*}
   18.57  
   18.58  lemma rename_transient: 
   18.59       "bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
   18.60 @@ -290,7 +290,7 @@
   18.61  by (simp add: Extend.OK_extend_iff rename_def)
   18.62  
   18.63  
   18.64 -(*** "image" versions of the rules, for lifting "guarantees" properties ***)
   18.65 +subsection{*"image" versions of the rules, for lifting "guarantees" properties*}
   18.66  
   18.67  (*All the proofs are similar.  Better would have been to prove one 
   18.68    meta-theorem, but how can we handle the polymorphism?  E.g. in 
    19.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Jan 30 18:08:09 2003 +0100
    19.2 +++ b/src/HOL/UNITY/SubstAx.thy	Fri Jan 31 20:12:44 2003 +0100
    19.3 @@ -6,6 +6,8 @@
    19.4  Weak LeadsTo relation (restricted to the set of reachable states)
    19.5  *)
    19.6  
    19.7 +header{*Weak Progress*}
    19.8 +
    19.9  theory SubstAx = WFair + Constrains:
   19.10  
   19.11  constdefs
   19.12 @@ -27,7 +29,7 @@
   19.13  done
   19.14  
   19.15  
   19.16 -(*** Specialized laws for handling invariants ***)
   19.17 +subsection{*Specialized laws for handling invariants*}
   19.18  
   19.19  (** Conjoining an Always property **)
   19.20  
   19.21 @@ -46,7 +48,7 @@
   19.22  lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
   19.23  
   19.24  
   19.25 -(*** Introduction rules: Basis, Trans, Union ***)
   19.26 +subsection{*Introduction rules: Basis, Trans, Union*}
   19.27  
   19.28  lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
   19.29  apply (simp add: LeadsTo_def)
   19.30 @@ -67,7 +69,7 @@
   19.31  done
   19.32  
   19.33  
   19.34 -(*** Derived rules ***)
   19.35 +subsection{*Derived rules*}
   19.36  
   19.37  lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
   19.38  by (simp add: LeadsTo_def)
   19.39 @@ -302,7 +304,7 @@
   19.40  done
   19.41  
   19.42  
   19.43 -(*** Induction rules ***)
   19.44 +subsection{*Induction rules*}
   19.45  
   19.46  (** Meta or object quantifier ????? **)
   19.47  lemma LeadsTo_wf_induct:
   19.48 @@ -368,7 +370,7 @@
   19.49  done
   19.50  
   19.51  
   19.52 -(*** Completion: Binary and General Finite versions ***)
   19.53 +subsection{*Completion: Binary and General Finite versions*}
   19.54  
   19.55  lemma Completion:
   19.56       "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C);  
    20.1 --- a/src/HOL/UNITY/UNITY.thy	Thu Jan 30 18:08:09 2003 +0100
    20.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Jan 31 20:12:44 2003 +0100
    20.3 @@ -8,6 +8,8 @@
    20.4  From Misra, "A Logic for Concurrent Programming", 1994
    20.5  *)
    20.6  
    20.7 +header {*The Basic UNITY Theory*}
    20.8 +
    20.9  theory UNITY = Main:
   20.10  
   20.11  typedef (Program)
    21.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Thu Jan 30 18:08:09 2003 +0100
    21.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Jan 31 20:12:44 2003 +0100
    21.3 @@ -2,9 +2,9 @@
    21.4      ID:         $Id$
    21.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.6      Copyright   2003  University of Cambridge
    21.7 +*)
    21.8  
    21.9 -Inclusive UNITY theory
   21.10 -*)
   21.11 +header{*Comprehensive UNITY Theory*}
   21.12  
   21.13  theory UNITY_Main = Detects + PPROD + Follows
   21.14  files "UNITY_tactics.ML":
    22.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Jan 30 18:08:09 2003 +0100
    22.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Jan 31 20:12:44 2003 +0100
    22.3 @@ -6,6 +6,71 @@
    22.4  Specialized UNITY tactics, and ML bindings of theorems
    22.5  *)
    22.6  
    22.7 +(*ListOrder*)
    22.8 +val Le_def = thm "Le_def";
    22.9 +val Ge_def = thm "Ge_def";
   22.10 +val prefix_def = thm "prefix_def";
   22.11 +val Nil_genPrefix = thm "Nil_genPrefix";
   22.12 +val genPrefix_length_le = thm "genPrefix_length_le";
   22.13 +val cons_genPrefixE = thm "cons_genPrefixE";
   22.14 +val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons";
   22.15 +val refl_genPrefix = thm "refl_genPrefix";
   22.16 +val genPrefix_refl = thm "genPrefix_refl";
   22.17 +val genPrefix_mono = thm "genPrefix_mono";
   22.18 +val append_genPrefix = thm "append_genPrefix";
   22.19 +val genPrefix_trans_O = thm "genPrefix_trans_O";
   22.20 +val genPrefix_trans = thm "genPrefix_trans";
   22.21 +val prefix_genPrefix_trans = thm "prefix_genPrefix_trans";
   22.22 +val genPrefix_prefix_trans = thm "genPrefix_prefix_trans";
   22.23 +val trans_genPrefix = thm "trans_genPrefix";
   22.24 +val genPrefix_antisym = thm "genPrefix_antisym";
   22.25 +val antisym_genPrefix = thm "antisym_genPrefix";
   22.26 +val genPrefix_Nil = thm "genPrefix_Nil";
   22.27 +val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix";
   22.28 +val genPrefix_Cons = thm "genPrefix_Cons";
   22.29 +val genPrefix_take_append = thm "genPrefix_take_append";
   22.30 +val genPrefix_append_both = thm "genPrefix_append_both";
   22.31 +val append_cons_eq = thm "append_cons_eq";
   22.32 +val append_one_genPrefix = thm "append_one_genPrefix";
   22.33 +val genPrefix_imp_nth = thm "genPrefix_imp_nth";
   22.34 +val nth_imp_genPrefix = thm "nth_imp_genPrefix";
   22.35 +val genPrefix_iff_nth = thm "genPrefix_iff_nth";
   22.36 +val prefix_refl = thm "prefix_refl";
   22.37 +val prefix_trans = thm "prefix_trans";
   22.38 +val prefix_antisym = thm "prefix_antisym";
   22.39 +val prefix_less_le = thm "prefix_less_le";
   22.40 +val set_mono = thm "set_mono";
   22.41 +val Nil_prefix = thm "Nil_prefix";
   22.42 +val prefix_Nil = thm "prefix_Nil";
   22.43 +val Cons_prefix_Cons = thm "Cons_prefix_Cons";
   22.44 +val same_prefix_prefix = thm "same_prefix_prefix";
   22.45 +val append_prefix = thm "append_prefix";
   22.46 +val prefix_appendI = thm "prefix_appendI";
   22.47 +val prefix_Cons = thm "prefix_Cons";
   22.48 +val append_one_prefix = thm "append_one_prefix";
   22.49 +val prefix_length_le = thm "prefix_length_le";
   22.50 +val strict_prefix_length_less = thm "strict_prefix_length_less";
   22.51 +val mono_length = thm "mono_length";
   22.52 +val prefix_iff = thm "prefix_iff";
   22.53 +val prefix_snoc = thm "prefix_snoc";
   22.54 +val prefix_append_iff = thm "prefix_append_iff";
   22.55 +val common_prefix_linear = thm "common_prefix_linear";
   22.56 +val reflexive_Le = thm "reflexive_Le";
   22.57 +val antisym_Le = thm "antisym_Le";
   22.58 +val trans_Le = thm "trans_Le";
   22.59 +val pfixLe_refl = thm "pfixLe_refl";
   22.60 +val pfixLe_trans = thm "pfixLe_trans";
   22.61 +val pfixLe_antisym = thm "pfixLe_antisym";
   22.62 +val prefix_imp_pfixLe = thm "prefix_imp_pfixLe";
   22.63 +val reflexive_Ge = thm "reflexive_Ge";
   22.64 +val antisym_Ge = thm "antisym_Ge";
   22.65 +val trans_Ge = thm "trans_Ge";
   22.66 +val pfixGe_refl = thm "pfixGe_refl";
   22.67 +val pfixGe_trans = thm "pfixGe_trans";
   22.68 +val pfixGe_antisym = thm "pfixGe_antisym";
   22.69 +val prefix_imp_pfixGe = thm "prefix_imp_pfixGe";
   22.70 +
   22.71 +
   22.72  (*UNITY*)
   22.73  val constrains_def = thm "constrains_def";
   22.74  val stable_def = thm "stable_def";
   22.75 @@ -105,7 +170,6 @@
   22.76  val leadsTo_refl = thm "leadsTo_refl";
   22.77  val empty_leadsTo = thm "empty_leadsTo";
   22.78  val leadsTo_UNIV = thm "leadsTo_UNIV";
   22.79 -val leadsTo_induct_pre_lemma = thm "leadsTo_induct_pre_lemma";
   22.80  val leadsTo_induct_pre = thm "leadsTo_induct_pre";
   22.81  val leadsTo_weaken_R = thm "leadsTo_weaken_R";
   22.82  val leadsTo_weaken_L = thm "leadsTo_weaken_L";
   22.83 @@ -127,7 +191,6 @@
   22.84  val psp = thm "psp";
   22.85  val psp2 = thm "psp2";
   22.86  val psp_unless = thm "psp_unless";
   22.87 -val leadsTo_wf_induct_lemma = thm "leadsTo_wf_induct_lemma";
   22.88  val leadsTo_wf_induct = thm "leadsTo_wf_induct";
   22.89  val bounded_induct = thm "bounded_induct";
   22.90  val lessThan_induct = thm "lessThan_induct";
   22.91 @@ -137,12 +200,9 @@
   22.92  val leadsTo_subset = thm "leadsTo_subset";
   22.93  val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
   22.94  val wlt_increasing = thm "wlt_increasing";
   22.95 -val lemma1 = thm "lemma1";
   22.96  val leadsTo_123 = thm "leadsTo_123";
   22.97  val wlt_constrains_wlt = thm "wlt_constrains_wlt";
   22.98 -val completion_lemma = thm "completion_lemma";
   22.99  val completion = thm "completion";
  22.100 -val finite_completion_lemma = thm "finite_completion_lemma";
  22.101  val finite_completion = thm "finite_completion";
  22.102  val stable_completion = thm "stable_completion";
  22.103  val finite_stable_completion = thm "finite_stable_completion";
  22.104 @@ -276,7 +336,6 @@
  22.105  val LessThan_bounded_induct = thm "LessThan_bounded_induct";
  22.106  val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct";
  22.107  val Completion = thm "Completion";
  22.108 -val Finite_completion_lemma = thm "Finite_completion_lemma";
  22.109  val Finite_completion = thm "Finite_completion";
  22.110  val Stable_completion = thm "Stable_completion";
  22.111  val Finite_stable_completion = thm "Finite_stable_completion";
  22.112 @@ -670,12 +729,10 @@
  22.113  val increasing_Un = thm "increasing_Un";
  22.114  val Increasing_Un = thm "Increasing_Un";
  22.115  val Always_Un = thm "Always_Un";
  22.116 -val Follows_Un_lemma = thm "Follows_Un_lemma";
  22.117  val Follows_Un = thm "Follows_Un";
  22.118  val increasing_union = thm "increasing_union";
  22.119  val Increasing_union = thm "Increasing_union";
  22.120  val Always_union = thm "Always_union";
  22.121 -val Follows_union_lemma = thm "Follows_union_lemma";
  22.122  val Follows_union = thm "Follows_union";
  22.123  val Follows_setsum = thm "Follows_setsum";
  22.124  val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe";
    23.1 --- a/src/HOL/UNITY/Union.thy	Thu Jan 30 18:08:09 2003 +0100
    23.2 +++ b/src/HOL/UNITY/Union.thy	Fri Jan 31 20:12:44 2003 +0100
    23.3 @@ -3,11 +3,11 @@
    23.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.5      Copyright   1998  University of Cambridge
    23.6  
    23.7 -Unions of programs
    23.8 -
    23.9  Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
   23.10  *)
   23.11  
   23.12 +header{*Unions of Programs*}
   23.13 +
   23.14  theory Union = SubstAx + FP:
   23.15  
   23.16  constdefs
   23.17 @@ -52,7 +52,7 @@
   23.18    "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _:_./ _)" 10)
   23.19  
   23.20  
   23.21 -(** SKIP **)
   23.22 +subsection{*SKIP*}
   23.23  
   23.24  lemma Init_SKIP [simp]: "Init SKIP = UNIV"
   23.25  by (simp add: SKIP_def)
   23.26 @@ -66,7 +66,7 @@
   23.27  lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
   23.28  by (force elim: reachable.induct intro: reachable.intros)
   23.29  
   23.30 -(** SKIP and safety properties **)
   23.31 +subsection{*SKIP and safety properties*}
   23.32  
   23.33  lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
   23.34  by (unfold constrains_def, auto)
   23.35 @@ -80,7 +80,7 @@
   23.36  declare SKIP_in_stable [THEN stable_imp_Stable, iff]
   23.37  
   23.38  
   23.39 -(** Join **)
   23.40 +subsection{*Join*}
   23.41  
   23.42  lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
   23.43  by (simp add: Join_def)
   23.44 @@ -93,7 +93,7 @@
   23.45  by (auto simp add: Join_def)
   23.46  
   23.47  
   23.48 -(** JN **)
   23.49 +subsection{*JN*}
   23.50  
   23.51  lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
   23.52  by (unfold JOIN_def SKIP_def, auto)
   23.53 @@ -119,7 +119,7 @@
   23.54  by (simp add: JOIN_def)
   23.55  
   23.56  
   23.57 -(** Algebraic laws **)
   23.58 +subsection{*Algebraic laws*}
   23.59  
   23.60  lemma Join_commute: "F Join G = G Join F"
   23.61  by (simp add: Join_def Un_commute Int_commute)
   23.62 @@ -156,7 +156,7 @@
   23.63  lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
   23.64  
   23.65  
   23.66 -(*** JN laws ***)
   23.67 +subsection{*JN laws*}
   23.68  
   23.69  (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
   23.70  lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
   23.71 @@ -183,7 +183,7 @@
   23.72  done
   23.73  
   23.74  
   23.75 -(*** Safety: co, stable, FP ***)
   23.76 +subsection{*Safety: co, stable, FP*}
   23.77  
   23.78  (*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
   23.79    alternative precondition is A<=B, but most proofs using this rule require
   23.80 @@ -245,7 +245,7 @@
   23.81  by (simp add: FP_def JN_stable INTER_def)
   23.82  
   23.83  
   23.84 -(*** Progress: transient, ensures ***)
   23.85 +subsection{*Progress: transient, ensures*}
   23.86  
   23.87  lemma JN_transient:
   23.88       "i : I ==>  
   23.89 @@ -313,7 +313,7 @@
   23.90  done
   23.91  
   23.92  
   23.93 -(*** the ok and OK relations ***)
   23.94 +subsection{*the ok and OK relations*}
   23.95  
   23.96  lemma ok_SKIP1 [iff]: "SKIP ok F"
   23.97  by (auto simp add: ok_def)
   23.98 @@ -357,7 +357,7 @@
   23.99  by (auto simp add: OK_iff_ok)
  23.100  
  23.101  
  23.102 -(*** Allowed ***)
  23.103 +subsection{*Allowed*}
  23.104  
  23.105  lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
  23.106  by (auto simp add: Allowed_def)
  23.107 @@ -374,7 +374,8 @@
  23.108  lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
  23.109  by (auto simp add: OK_iff_ok ok_iff_Allowed)
  23.110  
  23.111 -(*** safety_prop, for reasoning about given instances of "ok" ***)
  23.112 +subsection{*@{text safety_prop}, for reasoning about
  23.113 + given instances of "ok"*}
  23.114  
  23.115  lemma safety_prop_Acts_iff:
  23.116       "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
    24.1 --- a/src/HOL/UNITY/WFair.thy	Thu Jan 30 18:08:09 2003 +0100
    24.2 +++ b/src/HOL/UNITY/WFair.thy	Fri Jan 31 20:12:44 2003 +0100
    24.3 @@ -8,6 +8,8 @@
    24.4  From Misra, "A Logic for Concurrent Programming", 1994
    24.5  *)
    24.6  
    24.7 +header{*Progress under Weak Fairness*}
    24.8 +
    24.9  theory WFair = UNITY:
   24.10  
   24.11  constdefs
   24.12 @@ -51,11 +53,10 @@
   24.13    "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
   24.14  
   24.15  
   24.16 -(*** transient ***)
   24.17 +subsection{*transient*}
   24.18  
   24.19  lemma stable_transient_empty: 
   24.20      "[| F : stable A; F : transient A |] ==> A = {}"
   24.21 -
   24.22  by (unfold stable_def constrains_def transient_def, blast)
   24.23  
   24.24  lemma transient_strengthen: 
   24.25 @@ -81,7 +82,7 @@
   24.26  by (unfold transient_def, auto)
   24.27  
   24.28  
   24.29 -(*** ensures ***)
   24.30 +subsection{*ensures*}
   24.31  
   24.32  lemma ensuresI: 
   24.33      "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
   24.34 @@ -117,7 +118,7 @@
   24.35  by (simp (no_asm) add: ensures_def unless_def)
   24.36  
   24.37  
   24.38 -(*** leadsTo ***)
   24.39 +subsection{*leadsTo*}
   24.40  
   24.41  lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
   24.42  apply (unfold leadsTo_def)
   24.43 @@ -235,7 +236,7 @@
   24.44  lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
   24.45  by (blast intro: subset_imp_leadsTo leadsTo_Trans)
   24.46  
   24.47 -lemma leadsTo_weaken_L [rule_format (no_asm)]:
   24.48 +lemma leadsTo_weaken_L [rule_format]:
   24.49       "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
   24.50  by (blast intro: leadsTo_Trans subset_imp_leadsTo)
   24.51  
   24.52 @@ -372,7 +373,7 @@
   24.53  done
   24.54  
   24.55  
   24.56 -(*** Proving the induction rules ***)
   24.57 +subsection{*Proving the induction rules*}
   24.58  
   24.59  (** The most general rule: r is any wf relation; f is any variant function **)
   24.60  
   24.61 @@ -449,7 +450,7 @@
   24.62  done
   24.63  
   24.64  
   24.65 -(*** wlt ****)
   24.66 +subsection{*wlt*}
   24.67  
   24.68  (*Misra's property W3*)
   24.69  lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
   24.70 @@ -497,21 +498,33 @@
   24.71  apply (auto intro: leadsTo_UN)
   24.72  (*Blast_tac says PROOF FAILED*)
   24.73  apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" 
   24.74 -       in constrains_UN [THEN constrains_weaken])
   24.75 -apply (auto ); 
   24.76 +       in constrains_UN [THEN constrains_weaken], auto) 
   24.77  done
   24.78  
   24.79  
   24.80  (*Misra's property W5*)
   24.81  lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
   24.82 -apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], clarify)
   24.83 -apply (subgoal_tac "Ba = wlt F B")
   24.84 -prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
   24.85 -apply (simp add: wlt_increasing Un_absorb2)
   24.86 -done
   24.87 +proof -
   24.88 +  from wlt_leadsTo [of F B, THEN leadsTo_123]
   24.89 +  show ?thesis
   24.90 +  proof (elim exE conjE)
   24.91 +(* assumes have to be in exactly the form as in the goal displayed at
   24.92 +   this point.  Isar doesn't give you any automation. *)
   24.93 +    fix C
   24.94 +    assume wlt: "wlt F B \<subseteq> C"
   24.95 +       and lt:  "F \<in> C leadsTo B"
   24.96 +       and co:  "F \<in> C - B co C \<union> B"
   24.97 +    have eq: "C = wlt F B"
   24.98 +    proof -
   24.99 +      from lt and wlt show ?thesis 
  24.100 +           by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1])
  24.101 +    qed
  24.102 +    from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2)
  24.103 +  qed
  24.104 +qed
  24.105  
  24.106  
  24.107 -(*** Completion: Binary and General Finite versions ***)
  24.108 +subsection{*Completion: Binary and General Finite versions*}
  24.109  
  24.110  lemma completion_lemma :
  24.111       "[| W = wlt F (B' Un C);