src/HOL/BNF_Examples/Stream_Processor.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55076 1e73e090a514
parent 55075 b3d0a02a756d
child 55091 c43394c2e5ec
permissions -rw-r--r--
compile
blanchet@55075
     1
(*  Title:      HOL/BNF_Examples/Stream_Processor.thy
traytel@54961
     2
    Author:     Dmitriy Traytel, TU Muenchen
traytel@54961
     3
    Author:     Andrei Popescu, TU Muenchen
traytel@54961
     4
    Copyright   2014
traytel@54961
     5
traytel@54961
     6
Stream processors---a syntactic representation of continuous functions on streams
traytel@54961
     7
*)
traytel@54961
     8
traytel@54961
     9
header {* Stream Processors *}
traytel@54961
    10
traytel@54961
    11
theory Stream_Processor
blanchet@55076
    12
imports Stream "~~/src/HOL/Library/BNF_Decl"
traytel@54961
    13
begin
traytel@54961
    14
traytel@54961
    15
section {* Continuous Functions on Streams *}
traytel@54961
    16
traytel@54961
    17
datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
traytel@54961
    18
codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
traytel@54961
    19
traytel@54961
    20
primrec_new run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
traytel@54961
    21
  "run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"
traytel@54961
    22
| "run\<^sub>\<mu> (Put b sp) s = ((b, sp), s)"
traytel@54961
    23
traytel@54961
    24
primcorec run\<^sub>\<nu> :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where
traytel@54961
    25
  "run\<^sub>\<nu> sp s = (let ((h, sp), s) = run\<^sub>\<mu> (out sp) s in h ## run\<^sub>\<nu> sp s)"
traytel@54961
    26
traytel@54961
    27
primcorec copy :: "('a, 'a) sp\<^sub>\<nu>" where
traytel@54961
    28
  "copy = In (Get (\<lambda>a. Put a copy))"
traytel@54961
    29
traytel@54961
    30
lemma run\<^sub>\<nu>_copy: "run\<^sub>\<nu> copy s = s"
traytel@54961
    31
  by (coinduction arbitrary: s) simp
traytel@54961
    32
traytel@54961
    33
text {*
traytel@54961
    34
To use the function package for the definition of composition the
traytel@54961
    35
wellfoundedness of the subtree relation needs to be proved first.
traytel@54961
    36
*}
traytel@54961
    37
traytel@54961
    38
definition "sub \<equiv> {(f a, Get f) | a f. True}"
traytel@54961
    39
traytel@54961
    40
lemma subI[intro]: "(f a, Get f) \<in> sub"
traytel@54961
    41
  unfolding sub_def by blast
traytel@54961
    42
traytel@54961
    43
lemma wf_sub[simp, intro]: "wf sub"
traytel@54961
    44
proof (rule wfUNIVI)
traytel@54961
    45
  fix P  :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x
traytel@54961
    46
  assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x"
traytel@54961
    47
  hence I: "\<And>x. (\<forall>y. (\<exists>a f. y = f a \<and> x = Get f) \<longrightarrow> P y) \<Longrightarrow> P x" unfolding sub_def by blast
traytel@54961
    48
  show "P x" by (induct x) (auto intro: I)
traytel@54961
    49
qed
traytel@54961
    50
traytel@54961
    51
function
traytel@54961
    52
  sp\<^sub>\<mu>_comp :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> ('d, 'a, ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu> \<Rightarrow> ('d, 'b, 'c \<times> ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu>"
traytel@54961
    53
  (infixl "o\<^sub>\<mu>" 65)
traytel@54961
    54
where
traytel@54961
    55
  "Put b sp o\<^sub>\<mu> fsp = Put b (sp, In fsp)"
traytel@54961
    56
| "Get f o\<^sub>\<mu> Put b sp = f b o\<^sub>\<mu> out sp"
traytel@54961
    57
| "Get f o\<^sub>\<mu> Get g = Get (\<lambda>a. Get f o\<^sub>\<mu> g a)"
traytel@54961
    58
by pat_completeness auto
traytel@54961
    59
termination by (relation "lex_prod sub sub") auto
traytel@54961
    60
traytel@54961
    61
primcorec sp\<^sub>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where
traytel@54961
    62
  "out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')"
traytel@54961
    63
traytel@54961
    64
lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
blanchet@55066
    65
proof (rule ext, unfold comp_apply)
traytel@54961
    66
  fix s
traytel@54961
    67
  show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
traytel@54961
    68
  proof (coinduction arbitrary: sp sp' s)
traytel@54961
    69
    case Eq_stream
traytel@54961
    70
    show ?case
traytel@54961
    71
    proof (induct "out sp" "out sp'" arbitrary: sp sp' s rule: sp\<^sub>\<mu>_comp.induct)
traytel@54961
    72
      case (1 b sp'')
traytel@54961
    73
      show ?case by (auto simp add: 1[symmetric])
traytel@54961
    74
    next
traytel@54961
    75
      case (2 f b sp'')
traytel@54961
    76
      from 2(1)[of "In (f b)" sp''] show ?case by (simp add: 2(2,3)[symmetric])
traytel@54961
    77
    next
traytel@54961
    78
      case (3 f h)
traytel@54961
    79
      from 3(1)[of _ "shd s" "In (h (shd s))", OF 3(2)] show ?case by (simp add: 3(2,3)[symmetric])
traytel@54961
    80
    qed
traytel@54961
    81
  qed
traytel@54961
    82
qed
traytel@54961
    83
traytel@54961
    84
text {* Alternative definition of composition using primrec_new instead of function *}
traytel@54961
    85
traytel@54961
    86
primrec_new sp\<^sub>\<mu>_comp2R  where
traytel@54961
    87
  "sp\<^sub>\<mu>_comp2R f (Put b sp) = f b (out sp)"
traytel@54961
    88
| "sp\<^sub>\<mu>_comp2R f (Get h) = Get (sp\<^sub>\<mu>_comp2R f o h)"
traytel@54961
    89
traytel@54961
    90
primrec_new sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
traytel@54961
    91
  "Put b sp o\<^sup>*\<^sub>\<mu> fsp = Put b (sp, In fsp)"
traytel@54961
    92
| "Get f o\<^sup>*\<^sub>\<mu> fsp = sp\<^sub>\<mu>_comp2R (op o\<^sup>*\<^sub>\<mu> o f) fsp"
traytel@54961
    93
traytel@54961
    94
primcorec sp\<^sub>\<nu>_comp2 (infixl "o\<^sup>*\<^sub>\<nu>" 65) where
traytel@54961
    95
  "out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')"
traytel@54961
    96
traytel@54961
    97
lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
blanchet@55066
    98
proof (rule ext, unfold comp_apply)
traytel@54961
    99
  fix s
traytel@54961
   100
  show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
traytel@54961
   101
  proof (coinduction arbitrary: sp sp' s)
traytel@54961
   102
    case Eq_stream
traytel@54961
   103
    show ?case
traytel@54961
   104
    proof (induct "out sp" arbitrary: sp sp' s)
traytel@54961
   105
      case (Put b sp'')
traytel@54961
   106
      show ?case by (auto simp add: Put[symmetric])
traytel@54961
   107
    next
traytel@54961
   108
      case (Get f)
traytel@54961
   109
      then show ?case
traytel@54961
   110
      proof (induct "out sp'" arbitrary: sp sp' s)
traytel@54961
   111
        case (Put b sp'')
traytel@54961
   112
        from Put(2)[of "In (f b)" sp''] show ?case by (simp add: Put(1,3)[symmetric])
traytel@54961
   113
      next
traytel@54961
   114
        case (Get h)
traytel@54961
   115
        from Get(1)[OF _ Get(3,4), of "In (h (shd s))"] show ?case by (simp add: Get(2,4)[symmetric])
traytel@54961
   116
      qed
traytel@54961
   117
    qed
traytel@54961
   118
  qed
traytel@54961
   119
qed
traytel@54961
   120
traytel@54961
   121
text {* The two definitions are equivalent *}
traytel@54961
   122
traytel@54961
   123
lemma sp\<^sub>\<mu>_comp_sp\<^sub>\<mu>_comp2[simp]: "sp o\<^sub>\<mu> sp' = sp o\<^sup>*\<^sub>\<mu> sp'"
traytel@54961
   124
  by (induct sp sp' rule: sp\<^sub>\<mu>_comp.induct) auto
traytel@54961
   125
traytel@54961
   126
(*will be provided by the package*)
traytel@54961
   127
lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
traytel@54961
   128
  "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
traytel@54961
   129
  rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
traytel@54961
   130
by (tactic {*
traytel@54961
   131
  let val ks = 1 upto 2;
traytel@54961
   132
  in
traytel@54961
   133
    BNF_Tactics.unfold_thms_tac @{context}
traytel@54961
   134
      @{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN
traytel@54961
   135
    HEADGOAL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
traytel@54961
   136
      BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac,
traytel@54961
   137
      rtac @{thm conversepI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
traytel@54961
   138
      BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks,
traytel@54961
   139
      REPEAT_DETERM o eresolve_tac @{thms relcomppE conversepE GrpE},
traytel@54961
   140
      hyp_subst_tac @{context}, atac])
traytel@54961
   141
  end
traytel@54961
   142
*})
traytel@54961
   143
traytel@54961
   144
lemma sp\<^sub>\<mu>_rel_self: "\<lbrakk>op = \<le> R1; op = \<le> R2\<rbrakk> \<Longrightarrow> rel_sp\<^sub>\<mu> R1 R2 x x"
traytel@54961
   145
  by (erule (1) predicate2D[OF sp\<^sub>\<mu>.rel_mono]) (simp only: sp\<^sub>\<mu>.rel_eq)
traytel@54961
   146
traytel@54961
   147
lemma sp\<^sub>\<nu>_comp_sp\<^sub>\<nu>_comp2: "sp o\<^sub>\<nu> sp' = sp o\<^sup>*\<^sub>\<nu> sp'"
traytel@54961
   148
  by (coinduction arbitrary: sp sp') (auto intro!: sp\<^sub>\<mu>_rel_self)
traytel@54961
   149
traytel@54961
   150
traytel@54961
   151
section {* Generalization to an Arbitrary BNF as Codomain *}
traytel@54961
   152
traytel@54961
   153
bnf_decl ('a, 'b) F (map: F)
traytel@54961
   154
traytel@54961
   155
definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
traytel@54961
   156
   "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
traytel@54961
   157
traytel@54961
   158
(* The strength laws for \<theta>: *)
traytel@54961
   159
lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
blanchet@55066
   160
  unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
traytel@54961
   161
traytel@54961
   162
definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
traytel@54961
   163
  "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
traytel@54961
   164
traytel@54961
   165
lemma \<theta>_rid: "F id fst o \<theta> = fst"
blanchet@55066
   166
  unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
traytel@54961
   167
traytel@54961
   168
lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
blanchet@55066
   169
  unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
traytel@54961
   170
traytel@54961
   171
datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
traytel@54961
   172
codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
traytel@54961
   173
traytel@54961
   174
codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F")
traytel@54961
   175
traytel@54961
   176
(* Definition of run for an arbitrary final coalgebra as codomain: *)
traytel@54961
   177
traytel@54961
   178
primrec_new
traytel@54961
   179
  runF\<^sub>\<mu> :: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> (('b, ('a, 'b) spF\<^sub>\<nu>) F) \<times> 'a stream" 
traytel@54961
   180
where
traytel@54961
   181
  "runF\<^sub>\<mu> (GetF f) s = (runF\<^sub>\<mu> o f) (shd s) (stl s)"
traytel@54961
   182
| "runF\<^sub>\<mu> (PutF x) s = (x, s)"
traytel@54961
   183
traytel@54961
   184
primcorec runF\<^sub>\<nu> :: "('a, 'b) spF\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b JF" where
traytel@54961
   185
  "runF\<^sub>\<nu> sp s = (let (x, s) = runF\<^sub>\<mu> (outF sp) s in Ctor (F id (\<lambda> sp. runF\<^sub>\<nu> sp s) x))"
traytel@54961
   186
traytel@54961
   187
end