src/HOL/HOLCF/FOCUS/Buffer_adm.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45653 63ed1be524eb
child 49521 06cb12198b92
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40774
diff changeset
     1
(*  Title:      HOL/HOLCF/FOCUS/Buffer_adm.thy
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     2
    Author:     David von Oheimb, TU Muenchen
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     3
*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     4
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     5
header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     6
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory Buffer_adm
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
imports Buffer Stream_adm
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42151
diff changeset
    11
declare enat_0 [simp]
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    12
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    13
lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    14
by (drule BufAC_Asm_unfold [THEN iffD1], auto)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    15
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    16
lemma BufAC_Asm_d3:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    17
    "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\<bullet> & s:BufAC_Asm"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    18
by (drule BufAC_Asm_unfold [THEN iffD1], auto)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    19
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    20
lemma BufAC_Asm_F_def3:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    21
 "(s:BufAC_Asm_F A) = (s=<> | 
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    22
  (? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    23
by (unfold BufAC_Asm_F_def, auto)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    24
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    25
lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    26
by (auto simp add: down_cont_def BufAC_Asm_F_def3)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    27
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    28
lemma BufAC_Cmt_F_def3:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    29
 "((s,t):BufAC_Cmt_F C) = (!d x.
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    30
    (s = <>       --> t = <>                   ) & 
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    31
    (s = Md d\<leadsto><>  --> t = <>                   ) & 
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    32
    (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x,rt\<cdot>t):C))"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    33
apply (unfold BufAC_Cmt_F_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    34
apply (subgoal_tac "!d x. (s = Md d\<leadsto>\<bullet>\<leadsto>x --> (? y. t = d\<leadsto>y & (x,y):C)) = 
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    35
                     (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x,rt\<cdot>t):C)")
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    36
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    37
apply (auto intro: surjectiv_scons [symmetric])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    38
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    39
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    40
lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    41
by (auto simp add: down_cont_def BufAC_Cmt_F_def3)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    42
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    43
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    44
(**** adm_BufAC_Asm ***********************************************************)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    45
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    46
lemma BufAC_Asm_F_stream_monoP: "stream_monoP BufAC_Asm_F"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    47
apply (unfold BufAC_Asm_F_def stream_monoP_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    48
apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    49
apply (rule_tac x="Suc (Suc 0)" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    50
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    51
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    52
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    53
lemma adm_BufAC_Asm: "adm (%x. x:BufAC_Asm)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    54
apply (unfold BufAC_Asm_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    55
apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_monoP [THEN fstream_gfp_admI]])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    56
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    57
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    58
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    59
(**** adm_non_BufAC_Asm *******************************************************)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    60
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    61
lemma BufAC_Asm_F_stream_antiP: "stream_antiP BufAC_Asm_F"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    62
apply (unfold stream_antiP_def BufAC_Asm_F_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    63
apply (intro strip)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    64
apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    65
apply (rule_tac x="Suc (Suc 0)" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    66
apply (rule conjI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    67
prefer 2
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    68
apply ( intro strip)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    69
apply ( drule slen_mono)
27101
864d29f11c9d slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents: 26304
diff changeset
    70
apply ( drule (1) order_trans)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    71
apply (force)+
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    72
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    73
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    74
lemma adm_non_BufAC_Asm: "adm (%u. u~:BufAC_Asm)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    75
apply (unfold BufAC_Asm_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    76
apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_antiP [THEN fstream_non_gfp_admI]])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    77
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    78
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    79
(**** adm_BufAC ***************************************************************)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    80
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    81
(*adm_non_BufAC_Asm*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    82
lemma BufAC_Asm_cong [rule_format]: "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\<cdot>s = ff\<cdot>s"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    83
apply (rule fstream_ind2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    84
apply (simp add: adm_non_BufAC_Asm)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    85
apply   (force dest: Buf_f_empty)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    86
apply  (force dest!: BufAC_Asm_d2
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    87
              dest: Buf_f_d elim: ssubst)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    88
apply (safe dest!: BufAC_Asm_d3)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    89
apply (drule Buf_f_d_req)+
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    90
apply (fast elim: ssubst)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    91
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    92
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    93
(*adm_non_BufAC_Asm,BufAC_Asm_cong*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    94
lemma BufAC_Cmt_d_req:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    95
"!!X. [|f:BufEq; s:BufAC_Asm; (s, f\<cdot>s):BufAC_Cmt|] ==> (a\<leadsto>b\<leadsto>s, f\<cdot>(a\<leadsto>b\<leadsto>s)):BufAC_Cmt"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    96
apply (rule BufAC_Cmt_unfold [THEN iffD2])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    97
apply (intro strip)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    98
apply (frule Buf_f_d_req)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    99
apply (auto elim: BufAC_Asm_cong [THEN subst])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   100
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   101
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   102
(*adm_BufAC_Asm*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   103
lemma BufAC_Asm_antiton: "antitonP BufAC_Asm"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   104
apply (rule antitonPI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   105
apply (rule allI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   106
apply (rule fstream_ind2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   107
apply (  rule adm_lemmas)+
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   108
apply (   rule cont_id)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   109
apply (   rule adm_BufAC_Asm)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   110
apply (  safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   111
apply (  rule BufAC_Asm_empty)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   112
apply ( force dest!: fstream_prefix
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   113
              dest: BufAC_Asm_d2 intro: BufAC_Asm_d)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   114
apply ( force dest!: fstream_prefix
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   115
              dest: BufAC_Asm_d3 intro!: BufAC_Asm_d_req)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   116
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   117
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   118
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42151
diff changeset
   119
lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x --> 
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   120
                     (x,f\<cdot>x):down_iterate BufAC_Cmt_F i --> 
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   121
                     (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   122
apply (rule_tac x="%i. 2*i" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   123
apply (rule allI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   124
apply (induct_tac "i")
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   125
apply ( simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   126
apply (simp add: add_commute)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   127
apply (intro strip)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   128
apply (subst BufAC_Cmt_F_def3)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   129
apply (drule_tac P="%x. x" in BufAC_Cmt_F_def3 [THEN subst])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   130
apply safe
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   131
apply (   erule Buf_f_empty)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   132
apply (  erule Buf_f_d)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   133
apply ( drule Buf_f_d_req)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   134
apply ( safe, erule ssubst, simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   135
apply clarsimp
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   136
apply (rename_tac i d xa ya t)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   137
(*
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   138
 1. \<And>i d xa ya t.
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   139
       \<lbrakk>f \<in> BufEq;
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   140
          \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   141
                x \<sqsubseteq> s \<longrightarrow>
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42151
diff changeset
   142
                enat (2 * i) < #x \<longrightarrow>
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   143
                (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   144
                (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42151
diff changeset
   145
          Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; enat (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   146
          (ya, t) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa\<rbrakk>
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   147
       \<Longrightarrow> (xa, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>xa))) \<in> down_iterate BufAC_Cmt_F i
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   148
*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   149
apply (rotate_tac 2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   150
apply (drule BufAC_Asm_prefix2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   151
apply (frule Buf_f_d_req, erule exE, erule conjE, rotate_tac -1, erule ssubst)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   152
apply (frule Buf_f_d_req, erule exE, erule conjE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   153
apply (            subgoal_tac "f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya")
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   154
prefer 2
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   155
apply ( assumption)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   156
apply (            rotate_tac -1)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   157
apply (            simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   158
apply (erule subst)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   159
(*
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   160
 1. \<And>i d xa ya t ff ffa.
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42151
diff changeset
   161
       \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; enat (2 * i) < #ya;
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   162
          (ya, ffa\<cdot>ya) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa; f \<in> BufEq;
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   163
          \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   164
                x \<sqsubseteq> s \<longrightarrow>
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42151
diff changeset
   165
                enat (2 * i) < #x \<longrightarrow>
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   166
                (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   167
                (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   168
          xa \<in> BufAC_Asm; ff \<in> BufEq; ffa \<in> BufEq\<rbrakk>
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   169
       \<Longrightarrow> (xa, ff\<cdot>xa) \<in> down_iterate BufAC_Cmt_F i
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   170
*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   171
apply (drule spec, drule spec, drule (1) mp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   172
apply (drule (1) mp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   173
apply (drule (1) mp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   174
apply (erule impE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   175
apply ( subst BufAC_Asm_cong, assumption)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   176
prefer 3 apply assumption
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   177
apply assumption
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   178
apply ( erule (1) BufAC_Asm_antiton [THEN antitonPD])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   179
apply (subst BufAC_Asm_cong, assumption)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   180
prefer 3 apply assumption
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   181
apply assumption
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   182
apply assumption
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   183
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   184
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   185
lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   186
apply (unfold BufAC_Cmt_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   187
apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   188
apply (fast)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   189
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   190
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   191
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   192
  BufAC_Cmt_2stream_monoP*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   193
lemma adm_BufAC: "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\<cdot>s):BufAC_Cmt)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   194
apply (rule flatstream_admI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   195
apply (subst BufAC_Cmt_iterate_all)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   196
apply (drule BufAC_Cmt_2stream_monoP)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   197
apply safe
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   198
apply (drule spec, erule exE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   199
apply (drule spec, erule impE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   200
apply  (erule BufAC_Asm_antiton [THEN antitonPD])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   201
apply  (erule is_ub_thelub)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   202
apply (tactic "smp_tac 3 1")
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   203
apply (drule is_ub_thelub)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   204
apply (drule (1) mp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   205
apply (drule (1) mp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   206
apply (erule mp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   207
apply (drule BufAC_Cmt_iterate_all [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   208
apply (erule spec)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   209
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   210
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   211
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   212
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   213
(**** Buf_Eq_imp_AC by induction **********************************************)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   214
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   215
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   216
  BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   217
lemma Buf_Eq_imp_AC: "BufEq <= BufAC"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   218
apply (unfold BufAC_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   219
apply (rule subsetI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   220
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   221
apply (rule allI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   222
apply (rule fstream_ind2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   223
back
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   224
apply (   erule adm_BufAC)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   225
apply (  safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   226
apply (   erule BufAC_Cmt_empty)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   227
apply (  erule BufAC_Cmt_d)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   228
apply ( drule BufAC_Asm_prefix2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   229
apply ( simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   230
apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   231
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   232
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   233
(**** new approach for admissibility, reduces itself to absurdity *************)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   234
26304
02fbd0e7954a avoid rebinding of existing facts;
wenzelm
parents: 19763
diff changeset
   235
lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   236
apply (rule def_gfp_admI)
19763
wenzelm
parents: 19759
diff changeset
   237
apply (rule BufAC_Asm_def [THEN eq_reflection])
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   238
apply (safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   239
apply (unfold BufAC_Asm_F_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   240
apply (safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   241
apply (erule contrapos_np)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   242
apply (drule fstream_exhaust_eq [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   243
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   244
apply (drule (1) fstream_lub_lemma)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   245
apply (clarify)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   246
apply (erule_tac x="j" in all_dupE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   247
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   248
apply (drule BufAC_Asm_d2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   249
apply (clarify)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   250
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   251
apply (rule disjCI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   252
apply (erule contrapos_np)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   253
apply (drule fstream_exhaust_eq [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   254
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   255
apply (drule (1) fstream_lub_lemma)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   256
apply (clarsimp)
45653
63ed1be524eb tuned proof;
wenzelm
parents: 43924
diff changeset
   257
apply (simp only: ex_simps [symmetric] all_simps [symmetric])
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   258
apply (rule_tac x="Xa" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   259
apply (rule allI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   260
apply (rotate_tac -1)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   261
apply (erule_tac x="i" in allE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   262
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   263
apply (erule_tac x="jb" in allE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   264
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   265
apply (erule_tac x="jc" in allE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   266
apply (clarsimp dest!: BufAC_Asm_d3)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   267
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   268
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   269
lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   270
apply (rule def_gfp_adm_nonP)
19763
wenzelm
parents: 19759
diff changeset
   271
apply (rule BufAC_Asm_def [THEN eq_reflection])
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   272
apply (unfold BufAC_Asm_F_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   273
apply (safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   274
apply (erule contrapos_np)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   275
apply (drule fstream_exhaust_eq [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   276
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   277
apply (frule fstream_prefix)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   278
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   279
apply (frule BufAC_Asm_d2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   280
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   281
apply (rotate_tac -1)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   282
apply (erule contrapos_pp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   283
apply (drule fstream_exhaust_eq [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   284
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   285
apply (frule fstream_prefix)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   286
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   287
apply (frule BufAC_Asm_d3)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   288
apply (force)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   289
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   290
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   291
lemma adm_BufAC': "f \<in> BufEq \<Longrightarrow> adm (\<lambda>u. u \<in> BufAC_Asm \<longrightarrow> (u, f\<cdot>u) \<in> BufAC_Cmt)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   292
apply (rule triv_admI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   293
apply (clarify)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   294
apply (erule (1) Buf_Eq_imp_AC_lemma)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   295
      (* this is what we originally aimed to show, using admissibilty :-( *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   296
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   297
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   298
end
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   299
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   300