src/ZF/UNITY/Follows.thy
author wenzelm
Sun, 07 Oct 2007 21:19:31 +0200
changeset 24893 b8ef7afe3a6b
parent 24892 c663e675e177
child 32960 69916a850301
permissions -rw-r--r--
modernized specifications; removed legacy ML bindings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/Follows
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
     2
    ID:         $Id \<in> Follows.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     3
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     4
    Copyright   2002  University of Cambridge
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     5
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     6
Theory ported from HOL.
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     7
*)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     8
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
     9
header{*The "Follows" relation of Charpentier and Sivilotte*}
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    10
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14095
diff changeset
    11
theory Follows imports SubstAx Increasing begin
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    12
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    13
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    14
  Follows :: "[i, i, i=>i, i=>i] => i"  where
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    15
  "Follows(A, r, f, g) ==
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    16
            Increasing(A, r, g) Int
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    17
            Increasing(A, r,f) Int
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    18
            Always({s \<in> state. <f(s), g(s)>:r}) Int
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    19
           (\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} LeadsTo {s \<in> state. <k,f(s)>:r})"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    20
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    21
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    22
  Incr :: "[i=>i]=>i" where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    23
  "Incr(f) == Increasing(list(nat), prefix(nat), f)"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    24
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    25
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    26
  n_Incr :: "[i=>i]=>i" where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    27
  "n_Incr(f) == Increasing(nat, Le, f)"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    28
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    29
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    30
  s_Incr :: "[i=>i]=>i" where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    31
  "s_Incr(f) == Increasing(Pow(nat), SetLe(nat), f)"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    32
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    33
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    34
  m_Incr :: "[i=>i]=>i" where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    35
  "m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    36
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    37
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    38
  n_Fols :: "[i=>i, i=>i]=>i"   (infixl "n'_Fols" 65)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    39
  "f n_Fols g == Follows(nat, Le, f, g)"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    40
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    41
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    42
  Follows' :: "[i=>i, i=>i, i, i] => i"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    43
        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    44
  "f Fols g Wrt r/A == Follows(A,r,f,g)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    45
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    46
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    47
(*Does this hold for "invariant"?*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    48
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    49
lemma Follows_cong:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    50
     "[|A=A'; r=r'; !!x. x \<in> state ==> f(x)=f'(x); !!x. x \<in> state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    51
by (simp add: Increasing_def Follows_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    52
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    53
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    54
lemma subset_Always_comp:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    55
"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    56
   Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    57
apply (unfold mono1_def metacomp_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    58
apply (auto simp add: Always_eq_includes_reachable)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    59
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    60
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    61
lemma imp_Always_comp:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    62
"[| F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    63
    mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    64
    F \<in> Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    65
by (blast intro: subset_Always_comp [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    66
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    67
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    68
lemma imp_Always_comp2:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    69
"[| F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    70
    F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    71
    mono2(A, r, B, s, C, t, h);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    72
    \<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    73
  ==> F \<in> Always({x \<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \<in> t})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    74
apply (auto simp add: Always_eq_includes_reachable mono2_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    75
apply (auto dest!: subsetD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    76
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    77
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    78
(* comp LeadsTo *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    79
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    80
lemma subset_LeadsTo_comp:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    81
"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    82
        \<forall>x \<in> state. f(x):A & g(x):A |] ==>
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    83
  (\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}) <=
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    84
 (\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    85
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    86
apply (unfold mono1_def metacomp_def, clarify)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    87
apply (simp_all (no_asm_use) add: INT_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    88
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    89
apply (rule single_LeadsTo_I)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    90
prefer 2 apply (blast dest: LeadsTo_type [THEN subsetD], auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    91
apply (rotate_tac 5)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    92
apply (drule_tac x = "g (sa) " in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    93
apply (erule_tac [2] LeadsTo_weaken)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    94
apply (auto simp add: part_order_def refl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    95
apply (rule_tac b = "h (g (sa))" in trans_onD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    96
apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    97
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    98
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    99
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   100
lemma imp_LeadsTo_comp:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   101
"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   102
    mono1(A, r, B, s, h); refl(A,r); trans[B](s);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   103
    \<forall>x \<in> state. f(x):A & g(x):A |] ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   104
   F:(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   105
apply (rule subset_LeadsTo_comp [THEN subsetD], auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   106
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   107
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   108
lemma imp_LeadsTo_comp_right:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   109
"[| F \<in> Increasing(B, s, g);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   110
  \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   111
  mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   112
  \<forall>x \<in> state. f1(x):A & f(x):A & g(x):B; k \<in> C |] ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   113
  F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   114
apply (unfold mono2_def Increasing_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   115
apply (rule single_LeadsTo_I, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   116
apply (drule_tac x = "g (sa) " and A = B in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   117
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   118
apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   119
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   120
apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   121
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   122
apply (force simp add: part_order_def refl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   123
apply (force simp add: part_order_def refl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   124
apply (drule_tac x = "f1 (x) " and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. ?P (x,y,u) " in bspec [THEN bspec])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   125
apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) --> ?d (x,y) \<in> t" in bspec [THEN bspec])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   126
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   127
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   128
apply (auto simp add: part_order_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   129
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   130
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   131
lemma imp_LeadsTo_comp_left:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   132
"[| F \<in> Increasing(A, r, f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   133
  \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   134
  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   135
  \<forall>x \<in> state. f(x):A & g1(x):B & g(x):B; k \<in> C |] ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   136
  F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   137
apply (unfold mono2_def Increasing_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   138
apply (rule single_LeadsTo_I, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   139
apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   140
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   141
apply (drule_tac x = "g (sa) " in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   142
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   143
apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   144
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   145
apply (force simp add: part_order_def refl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   146
apply (force simp add: part_order_def refl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   147
apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   148
apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) --> ?d (x,y) \<in> t" in bspec [THEN bspec])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   149
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   150
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   151
apply (auto simp add: part_order_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   152
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   153
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   154
(**  This general result is used to prove Follows Un, munion, etc. **)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   155
lemma imp_LeadsTo_comp2:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   156
"[| F \<in> Increasing(A, r, f1) Int  Increasing(B, s, g);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   157
  \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   158
  \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   159
  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   160
  \<forall>x \<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \<in> C |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   161
  ==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   162
apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   163
apply (blast intro: imp_LeadsTo_comp_right)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   164
apply (blast intro: imp_LeadsTo_comp_left)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   165
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   166
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   167
(* Follows type *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   168
lemma Follows_type: "Follows(A, r, f, g)<=program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   169
apply (unfold Follows_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   170
apply (blast dest: Increasing_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   171
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   172
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   173
lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   174
by (blast dest: Follows_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   175
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   176
lemma FollowsD:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   177
"F \<in> Follows(A, r, f, g)==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   178
  F \<in> program & (\<exists>a. a \<in> A) & (\<forall>x \<in> state. f(x):A & g(x):A)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   179
apply (unfold Follows_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   180
apply (blast dest: IncreasingD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   181
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   182
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   183
lemma Follows_constantI:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   184
 "[| F \<in> program; c \<in> A; refl(A, r) |] ==> F \<in> Follows(A, r, %x. c, %x. c)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   185
apply (unfold Follows_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   186
apply (auto simp add: refl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   187
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   188
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   189
lemma subset_Follows_comp:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   190
"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   191
   ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   192
apply (unfold Follows_def, clarify)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   193
apply (frule_tac f = g in IncreasingD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   194
apply (frule_tac f = f in IncreasingD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   195
apply (rule IntI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   196
apply (rule_tac [2] h = h in imp_LeadsTo_comp)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   197
prefer 5 apply assumption
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   198
apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   199
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   200
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   201
lemma imp_Follows_comp:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   202
"[| F \<in> Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   203
  ==>  F \<in> Follows(B, s,  h comp f, h comp g)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   204
apply (blast intro: subset_Follows_comp [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   205
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   206
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   207
(* 2-place monotone operation \<in> this general result is used to prove Follows_Un, Follows_munion *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   208
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   209
(* 2-place monotone operation \<in> this general result is
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   210
   used to prove Follows_Un, Follows_munion *)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   211
lemma imp_Follows_comp2:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   212
"[| F \<in> Follows(A, r, f1, f);  F \<in> Follows(B, s, g1, g);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   213
   mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   214
   ==> F \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   215
apply (unfold Follows_def, clarify)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   216
apply (frule_tac f = g in IncreasingD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   217
apply (frule_tac f = f in IncreasingD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   218
apply (rule IntI, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   219
apply (rule_tac [3] h = h in imp_Always_comp2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   220
prefer 5 apply assumption
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   221
apply (rule_tac [2] h = h in imp_Increasing_comp2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   222
prefer 4 apply assumption
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   223
apply (rule_tac h = h in imp_Increasing_comp2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   224
prefer 3 apply assumption
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   225
apply simp_all
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   226
apply (blast dest!: IncreasingD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   227
apply (rule_tac h = h in imp_LeadsTo_comp2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   228
prefer 4 apply assumption
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   229
apply auto
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   230
  prefer 3 apply (simp add: mono2_def)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   231
apply (blast dest: IncreasingD)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   232
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   233
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   234
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   235
lemma Follows_trans:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   236
     "[| F \<in> Follows(A, r, f, g);  F \<in> Follows(A,r, g, h);
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   237
         trans[A](r) |] ==> F \<in> Follows(A, r, f, h)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   238
apply (frule_tac f = f in FollowsD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   239
apply (frule_tac f = g in FollowsD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   240
apply (simp add: Follows_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   241
apply (simp add: Always_eq_includes_reachable INT_iff, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   242
apply (rule_tac [2] B = "{s \<in> state. <k, g (s) > \<in> r}" in LeadsTo_Trans)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   243
apply (rule_tac b = "g (x) " in trans_onD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   244
apply blast+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   245
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   246
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   247
(** Destruction rules for Follows **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   248
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   249
lemma Follows_imp_Increasing_left:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   250
     "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   251
by (unfold Follows_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   252
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   253
lemma Follows_imp_Increasing_right:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   254
     "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   255
by (unfold Follows_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   256
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   257
lemma Follows_imp_Always:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   258
 "F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   259
by (unfold Follows_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   260
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   261
lemma Follows_imp_LeadsTo:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   262
 "[| F \<in> Follows(A, r, f, g); k \<in> A |]  ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   263
  F: {s \<in> state. <k,g(s)> \<in> r } LeadsTo {s \<in> state. <k,f(s)> \<in> r}"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   264
by (unfold Follows_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   265
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   266
lemma Follows_LeadsTo_pfixLe:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   267
     "[| F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   268
   ==> F \<in> {s \<in> state. k pfixLe g(s)} LeadsTo {s \<in> state. k pfixLe f(s)}"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   269
by (blast intro: Follows_imp_LeadsTo)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   270
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   271
lemma Follows_LeadsTo_pfixGe:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   272
     "[| F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   273
   ==> F \<in> {s \<in> state. k pfixGe g(s)} LeadsTo {s \<in> state. k pfixGe f(s)}"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   274
by (blast intro: Follows_imp_LeadsTo)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   275
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   276
lemma Always_Follows1:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   277
"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   278
    \<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   279
apply (unfold Follows_def Increasing_def Stable_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   280
apply (simp add: INT_iff, auto)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   281
apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   282
	and A = "{s \<in> state. <k, h (s)> \<in> r}"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   283
	and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   284
apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   285
           and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   286
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   287
apply (drule Always_Int_I, assumption)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   288
apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   289
       in Always_weaken)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   290
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   291
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   292
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   293
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   294
lemma Always_Follows2:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   295
"[| F \<in> Always({s \<in> state. g(s) = h(s)});
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   296
  F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A |] ==> F \<in> Follows(A, r, f, h)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   297
apply (unfold Follows_def Increasing_def Stable_def)
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   298
apply (simp add: INT_iff, auto)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   299
apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   300
            and A = "{s \<in> state. <k, g (s) > \<in> r}"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   301
            and A' = "{s \<in> state. <k, f (s) > \<in> r}" in Always_LeadsTo_weaken)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   302
apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   303
         and A' = "{s \<in> state. <k, g(s)> \<in> r}" in Always_Constrains_weaken)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   304
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   305
apply (drule Always_Int_I, assumption)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   306
apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   307
       in Always_weaken)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   308
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   309
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   310
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   311
(** Union properties (with the subset ordering) **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   312
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   313
lemma refl_SetLe [simp]: "refl(Pow(A), SetLe(A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   314
by (unfold refl_def SetLe_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   315
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   316
lemma trans_on_SetLe [simp]: "trans[Pow(A)](SetLe(A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   317
by (unfold trans_on_def SetLe_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   318
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   319
lemma antisym_SetLe [simp]: "antisym(SetLe(A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   320
by (unfold antisym_def SetLe_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   321
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   322
lemma part_order_SetLe [simp]: "part_order(Pow(A), SetLe(A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   323
by (unfold part_order_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   324
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   325
lemma increasing_Un:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   326
     "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   327
         F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   328
     ==> F \<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   329
by (rule_tac h = "op Un" in imp_increasing_comp2, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   330
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   331
lemma Increasing_Un:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   332
     "[| F \<in> Increasing(Pow(A), SetLe(A), f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   333
         F \<in> Increasing(Pow(A), SetLe(A), g) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   334
     ==> F \<in> Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   335
by (rule_tac h = "op Un" in imp_Increasing_comp2, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   336
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   337
lemma Always_Un:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   338
     "[| F \<in> Always({s \<in> state. f1(s) <= f(s)});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   339
     F \<in> Always({s \<in> state. g1(s) <= g(s)}) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   340
      ==> F \<in> Always({s \<in> state. f1(s) Un g1(s) <= f(s) Un g(s)})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   341
by (simp add: Always_eq_includes_reachable, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   342
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   343
lemma Follows_Un:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   344
"[| F \<in> Follows(Pow(A), SetLe(A), f1, f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   345
     F \<in> Follows(Pow(A), SetLe(A), g1, g) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   346
     ==> F \<in> Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   347
by (rule_tac h = "op Un" in imp_Follows_comp2, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   348
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   349
(** Multiset union properties (with the MultLe ordering) **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   350
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   351
lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   352
by (unfold MultLe_def refl_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   353
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   354
lemma MultLe_refl1 [simp]:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   355
 "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \<in> MultLe(A, r)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   356
apply (unfold MultLe_def id_def lam_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   357
apply (auto simp add: Mult_iff_multiset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   358
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   359
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   360
lemma MultLe_refl2 [simp]: "M \<in> Mult(A) ==> <M, M> \<in> MultLe(A, r)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   361
by (unfold MultLe_def id_def lam_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   362
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   363
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   364
lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   365
apply (unfold MultLe_def trans_on_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   366
apply (auto intro: trancl_trans simp add: multirel_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   367
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   368
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   369
lemma MultLe_type: "MultLe(A, r)<= (Mult(A) * Mult(A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   370
apply (unfold MultLe_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   371
apply (drule multirel_type [THEN subsetD], auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   372
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   373
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   374
lemma MultLe_trans:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   375
     "[| <M,K> \<in> MultLe(A,r); <K,N> \<in> MultLe(A,r) |] ==> <M,N> \<in> MultLe(A,r)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   376
apply (cut_tac A=A in trans_on_MultLe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   377
apply (drule trans_onD, assumption)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   378
apply (auto dest: MultLe_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   379
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   380
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   381
lemma part_order_imp_part_ord:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   382
     "part_order(A, r) ==> part_ord(A, r-id(A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   383
apply (unfold part_order_def part_ord_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   384
apply (simp add: refl_def id_def lam_def irrefl_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   385
apply (simp (no_asm) add: trans_on_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   386
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   387
apply (blast dest: trans_onD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   388
apply (simp (no_asm_use) add: antisym_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   389
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   390
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   391
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   392
lemma antisym_MultLe [simp]:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   393
  "part_order(A, r) ==> antisym(MultLe(A,r))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   394
apply (unfold MultLe_def antisym_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   395
apply (drule part_order_imp_part_ord, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   396
apply (drule irrefl_on_multirel)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   397
apply (frule multirel_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   398
apply (drule multirel_trans)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   399
apply (auto simp add: irrefl_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   400
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   401
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   402
lemma part_order_MultLe [simp]:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   403
     "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   404
apply (frule antisym_MultLe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   405
apply (auto simp add: part_order_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   406
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   407
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   408
lemma empty_le_MultLe [simp]:
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   409
"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \<in> MultLe(A, r)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   410
apply (unfold MultLe_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   411
apply (case_tac "M=0")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   412
apply (auto simp add: FiniteFun.intros)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   413
apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r - id (A))")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   414
apply (rule_tac [2] one_step_implies_multirel)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   415
apply (auto simp add: Mult_iff_multiset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   416
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   417
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   418
lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   419
by (simp add: Mult_iff_multiset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   420
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   421
lemma munion_mono:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   422
"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   423
  <M +# K, N +# L> \<in> MultLe(A, r)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   424
apply (unfold MultLe_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   425
apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   426
       munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   427
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   428
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   429
lemma increasing_munion:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   430
     "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   431
         F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   432
     ==> F \<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   433
by (rule_tac h = munion in imp_increasing_comp2, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   434
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   435
lemma Increasing_munion:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   436
     "[| F \<in> Increasing(Mult(A), MultLe(A,r), f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   437
         F \<in> Increasing(Mult(A), MultLe(A,r), g)|]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   438
     ==> F \<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   439
by (rule_tac h = munion in imp_Increasing_comp2, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   440
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   441
lemma Always_munion:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   442
"[| F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   443
          F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)});
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   444
  \<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   445
      ==> F \<in> Always({s \<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \<in> MultLe(A,r)})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   446
apply (rule_tac h = munion in imp_Always_comp2, simp_all)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   447
apply (blast intro: munion_mono, simp_all)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   448
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   449
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   450
lemma Follows_munion:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   451
"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   452
    F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   453
  ==> F \<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   454
by (rule_tac h = munion in imp_Follows_comp2, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   455
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   456
(** Used in ClientImp **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   457
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   458
lemma Follows_msetsum_UN:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   459
"!!f. [| \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i));
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   460
  \<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A &
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   461
                        multiset(f(i, s)) & mset_of(f(i, s))<=A ;
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   462
   Finite(I); F \<in> program |]
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   463
        ==> F \<in> Follows(Mult(A),
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   464
                        MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A),
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   465
                                      %x. msetsum(%i. f(i,  x), I, A))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   466
apply (erule rev_mp)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   467
apply (drule Finite_into_Fin)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   468
apply (erule Fin_induct)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   469
apply (simp (no_asm_simp))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   470
apply (rule Follows_constantI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   471
apply (simp_all (no_asm_simp) add: FiniteFun.intros)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   472
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   473
apply (rule Follows_munion, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   474
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   475
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
   476
end