src/HOL/Library/While_Combinator.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 41764 5268aef2fe83
child 45834 9c232d370244
permissions -rw-r--r--
Quotient_Info stores only relation maps
haftmann@22803
     1
(*  Title:      HOL/Library/While_Combinator.thy
wenzelm@10251
     2
    Author:     Tobias Nipkow
krauss@37757
     3
    Author:     Alexander Krauss
wenzelm@10251
     4
    Copyright   2000 TU Muenchen
wenzelm@10251
     5
*)
wenzelm@10251
     6
wenzelm@14706
     7
header {* A general ``while'' combinator *}
wenzelm@10251
     8
nipkow@15131
     9
theory While_Combinator
haftmann@30738
    10
imports Main
nipkow@15131
    11
begin
wenzelm@10251
    12
krauss@37760
    13
subsection {* Partial version *}
krauss@37757
    14
krauss@37757
    15
definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
krauss@37757
    16
"while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
krauss@37757
    17
   then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
krauss@37757
    18
   else None)"
wenzelm@10251
    19
krauss@37757
    20
theorem while_option_unfold[code]:
krauss@37757
    21
"while_option b c s = (if b s then while_option b c (c s) else Some s)"
krauss@37757
    22
proof cases
krauss@37757
    23
  assume "b s"
krauss@37757
    24
  show ?thesis
krauss@37757
    25
  proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
krauss@37757
    26
    case True
krauss@37757
    27
    then obtain k where 1: "~ b ((c ^^ k) s)" ..
krauss@37757
    28
    with `b s` obtain l where "k = Suc l" by (cases k) auto
krauss@37757
    29
    with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
krauss@37757
    30
    then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
krauss@37757
    31
    from 1
krauss@37757
    32
    have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
krauss@37757
    33
      by (rule Least_Suc) (simp add: `b s`)
krauss@37757
    34
    also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
krauss@37757
    35
      by (simp add: funpow_swap1)
krauss@37757
    36
    finally
krauss@37757
    37
    show ?thesis 
krauss@37757
    38
      using True 2 `b s` by (simp add: funpow_swap1 while_option_def)
krauss@37757
    39
  next
krauss@37757
    40
    case False
krauss@37757
    41
    then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
krauss@37757
    42
    then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
krauss@37757
    43
      by (simp add: funpow_swap1)
krauss@37757
    44
    with False  `b s` show ?thesis by (simp add: while_option_def)
krauss@37757
    45
  qed
krauss@37757
    46
next
krauss@37757
    47
  assume [simp]: "~ b s"
krauss@37757
    48
  have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
krauss@37757
    49
    by (rule Least_equality) auto
krauss@37757
    50
  moreover 
krauss@37757
    51
  have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
krauss@37757
    52
  ultimately show ?thesis unfolding while_option_def by auto 
krauss@37757
    53
qed
wenzelm@10251
    54
krauss@37757
    55
lemma while_option_stop:
krauss@37757
    56
assumes "while_option b c s = Some t"
krauss@37757
    57
shows "~ b t"
krauss@37757
    58
proof -
krauss@37757
    59
  from assms have ex: "\<exists>k. ~ b ((c ^^ k) s)"
krauss@37757
    60
  and t: "t = (c ^^ (LEAST k. ~ b ((c ^^ k) s))) s"
krauss@37757
    61
    by (auto simp: while_option_def split: if_splits)
krauss@37757
    62
  from LeastI_ex[OF ex]
krauss@37757
    63
  show "~ b t" unfolding t .
krauss@37757
    64
qed
krauss@37757
    65
krauss@37757
    66
theorem while_option_rule:
krauss@37757
    67
assumes step: "!!s. P s ==> b s ==> P (c s)"
krauss@37757
    68
and result: "while_option b c s = Some t"
krauss@37757
    69
and init: "P s"
krauss@37757
    70
shows "P t"
krauss@37757
    71
proof -
krauss@37757
    72
  def k == "LEAST k. ~ b ((c ^^ k) s)"
krauss@37757
    73
  from assms have t: "t = (c ^^ k) s"
krauss@37757
    74
    by (simp add: while_option_def k_def split: if_splits)    
krauss@37757
    75
  have 1: "ALL i<k. b ((c ^^ i) s)"
krauss@37757
    76
    by (auto simp: k_def dest: not_less_Least)
krauss@37757
    77
krauss@37757
    78
  { fix i assume "i <= k" then have "P ((c ^^ i) s)"
krauss@37757
    79
      by (induct i) (auto simp: init step 1) }
krauss@37757
    80
  thus "P t" by (auto simp: t)
krauss@37757
    81
qed
krauss@37757
    82
krauss@37757
    83
krauss@37760
    84
subsection {* Total version *}
krauss@37757
    85
krauss@37757
    86
definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
krauss@37757
    87
where "while b c s = the (while_option b c s)"
krauss@37757
    88
krauss@37757
    89
lemma while_unfold:
krauss@37757
    90
  "while b c s = (if b s then while b c (c s) else s)"
krauss@37757
    91
unfolding while_def by (subst while_option_unfold) simp
nipkow@10984
    92
wenzelm@18372
    93
lemma def_while_unfold:
wenzelm@18372
    94
  assumes fdef: "f == while test do"
wenzelm@18372
    95
  shows "f x = (if test x then f(do x) else x)"
krauss@37757
    96
unfolding fdef by (fact while_unfold)
nipkow@14300
    97
nipkow@14300
    98
wenzelm@10251
    99
text {*
wenzelm@10251
   100
 The proof rule for @{term while}, where @{term P} is the invariant.
wenzelm@10251
   101
*}
wenzelm@10251
   102
wenzelm@18372
   103
theorem while_rule_lemma:
wenzelm@18372
   104
  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
wenzelm@18372
   105
    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
wenzelm@18372
   106
    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
wenzelm@18372
   107
  shows "P s \<Longrightarrow> Q (while b c s)"
wenzelm@19736
   108
  using wf
wenzelm@19736
   109
  apply (induct s)
wenzelm@18372
   110
  apply simp
wenzelm@18372
   111
  apply (subst while_unfold)
wenzelm@18372
   112
  apply (simp add: invariant terminate)
wenzelm@18372
   113
  done
wenzelm@10251
   114
nipkow@10653
   115
theorem while_rule:
nipkow@10984
   116
  "[| P s;
nipkow@10984
   117
      !!s. [| P s; b s  |] ==> P (c s);
nipkow@10984
   118
      !!s. [| P s; \<not> b s  |] ==> Q s;
wenzelm@10997
   119
      wf r;
nipkow@10984
   120
      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
nipkow@10984
   121
   Q (while b c s)"
wenzelm@19736
   122
  apply (rule while_rule_lemma)
wenzelm@19736
   123
     prefer 4 apply assumption
wenzelm@19736
   124
    apply blast
wenzelm@19736
   125
   apply blast
wenzelm@19736
   126
  apply (erule wf_subset)
wenzelm@19736
   127
  apply blast
wenzelm@19736
   128
  done
nipkow@10653
   129
nipkow@41720
   130
text{* Proving termination: *}
nipkow@41720
   131
nipkow@41720
   132
theorem wf_while_option_Some:
nipkow@41764
   133
  assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
nipkow@41764
   134
  and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
nipkow@41720
   135
  shows "EX t. while_option b c s = Some t"
nipkow@41764
   136
using assms(1,3)
nipkow@41720
   137
apply (induct s)
nipkow@41764
   138
using assms(2)
nipkow@41720
   139
apply (subst while_option_unfold)
nipkow@41720
   140
apply simp
nipkow@41720
   141
done
nipkow@41720
   142
nipkow@41720
   143
theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
nipkow@41764
   144
shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
nipkow@41764
   145
  \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
nipkow@41764
   146
by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
wenzelm@10251
   147
wenzelm@10251
   148
end