split off mrec into separate theory
authorhaftmann
Mon Jul 12 16:19:15 2010 +0200 (2010-07-12)
changeset 37772026ed2fc15d4
parent 37771 1bec64044b5e
child 37773 786ecb1af09b
split off mrec into separate theory
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Imperative_HOL.thy
src/HOL/Imperative_HOL/Mrec.thy
src/HOL/Imperative_HOL/Relational.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 16:05:08 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 16:19:15 2010 +0200
     1.3 @@ -476,151 +476,6 @@
     1.4    ultimately show ?case by (simp, simp only: execute_bind(1), simp)
     1.5  qed
     1.6  
     1.7 -
     1.8 -subsubsection {* A monadic combinator for simple recursive functions *}
     1.9 -
    1.10 -text {* Using a locale to fix arguments f and g of MREC *}
    1.11 -
    1.12 -locale mrec =
    1.13 -  fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
    1.14 -  and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
    1.15 -begin
    1.16 -
    1.17 -function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
    1.18 -  "mrec x h = (case execute (f x) h of
    1.19 -     Some (Inl r, h') \<Rightarrow> Some (r, h')
    1.20 -   | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
    1.21 -             Some (z, h'') \<Rightarrow> execute (g x s z) h''
    1.22 -           | None \<Rightarrow> None)
    1.23 -   | None \<Rightarrow> None)"
    1.24 -by auto
    1.25 -
    1.26 -lemma graph_implies_dom:
    1.27 -  "mrec_graph x y \<Longrightarrow> mrec_dom x"
    1.28 -apply (induct rule:mrec_graph.induct) 
    1.29 -apply (rule accpI)
    1.30 -apply (erule mrec_rel.cases)
    1.31 -by simp
    1.32 -
    1.33 -lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
    1.34 -  unfolding mrec_def 
    1.35 -  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
    1.36 -
    1.37 -lemma mrec_di_reverse: 
    1.38 -  assumes "\<not> mrec_dom (x, h)"
    1.39 -  shows "
    1.40 -   (case execute (f x) h of
    1.41 -     Some (Inl r, h') \<Rightarrow> False
    1.42 -   | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
    1.43 -   | None \<Rightarrow> False
    1.44 -   )" 
    1.45 -using assms apply (auto split: option.split sum.split)
    1.46 -apply (rule ccontr)
    1.47 -apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
    1.48 -done
    1.49 -
    1.50 -lemma mrec_rule:
    1.51 -  "mrec x h = 
    1.52 -   (case execute (f x) h of
    1.53 -     Some (Inl r, h') \<Rightarrow> Some (r, h')
    1.54 -   | Some (Inr s, h') \<Rightarrow> 
    1.55 -          (case mrec s h' of
    1.56 -             Some (z, h'') \<Rightarrow> execute (g x s z) h''
    1.57 -           | None \<Rightarrow> None)
    1.58 -   | None \<Rightarrow> None
    1.59 -   )"
    1.60 -apply (cases "mrec_dom (x,h)", simp)
    1.61 -apply (frule mrec_default)
    1.62 -apply (frule mrec_di_reverse, simp)
    1.63 -by (auto split: sum.split option.split simp: mrec_default)
    1.64 -
    1.65 -definition
    1.66 -  "MREC x = Heap (mrec x)"
    1.67 -
    1.68 -lemma MREC_rule:
    1.69 -  "MREC x = 
    1.70 -  (do y \<leftarrow> f x;
    1.71 -                (case y of 
    1.72 -                Inl r \<Rightarrow> return r
    1.73 -              | Inr s \<Rightarrow> 
    1.74 -                do z \<leftarrow> MREC s ;
    1.75 -                   g x s z
    1.76 -                done) done)"
    1.77 -  unfolding MREC_def
    1.78 -  unfolding bind_def return_def
    1.79 -  apply simp
    1.80 -  apply (rule ext)
    1.81 -  apply (unfold mrec_rule[of x])
    1.82 -  by (auto split: option.splits prod.splits sum.splits)
    1.83 -
    1.84 -lemma MREC_pinduct:
    1.85 -  assumes "execute (MREC x) h = Some (r, h')"
    1.86 -  assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
    1.87 -  assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
    1.88 -    \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
    1.89 -  shows "P x h h' r"
    1.90 -proof -
    1.91 -  from assms(1) have mrec: "mrec x h = Some (r, h')"
    1.92 -    unfolding MREC_def execute.simps .
    1.93 -  from mrec have dom: "mrec_dom (x, h)"
    1.94 -    apply -
    1.95 -    apply (rule ccontr)
    1.96 -    apply (drule mrec_default) by auto
    1.97 -  from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
    1.98 -    by auto
    1.99 -  from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
   1.100 -  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
   1.101 -    case (1 x h)
   1.102 -    obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
   1.103 -    show ?case
   1.104 -    proof (cases "execute (f x) h")
   1.105 -      case (Some result)
   1.106 -      then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
   1.107 -      note Inl' = this
   1.108 -      show ?thesis
   1.109 -      proof (cases a)
   1.110 -        case (Inl aa)
   1.111 -        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
   1.112 -          by auto
   1.113 -      next
   1.114 -        case (Inr b)
   1.115 -        note Inr' = this
   1.116 -        show ?thesis
   1.117 -        proof (cases "mrec b h1")
   1.118 -          case (Some result)
   1.119 -          then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
   1.120 -          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
   1.121 -            apply (intro 1(2))
   1.122 -            apply (auto simp add: Inr Inl')
   1.123 -            done
   1.124 -          moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
   1.125 -          ultimately show ?thesis
   1.126 -            apply auto
   1.127 -            apply (rule rec_case)
   1.128 -            apply auto
   1.129 -            unfolding MREC_def by auto
   1.130 -        next
   1.131 -          case None
   1.132 -          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
   1.133 -        qed
   1.134 -      qed
   1.135 -    next
   1.136 -      case None
   1.137 -      from this 1(1) mrec 1(3) show ?thesis by simp
   1.138 -    qed
   1.139 -  qed
   1.140 -  from this h'_r show ?thesis by simp
   1.141 -qed
   1.142 -
   1.143 -end
   1.144 -
   1.145 -text {* Providing global versions of the constant and the theorems *}
   1.146 -
   1.147 -abbreviation "MREC == mrec.MREC"
   1.148 -lemmas MREC_rule = mrec.MREC_rule
   1.149 -lemmas MREC_pinduct = mrec.MREC_pinduct
   1.150 -
   1.151 -
   1.152  subsection {* Code generator setup *}
   1.153  
   1.154  subsubsection {* Logical intermediate layer *}
     2.1 --- a/src/HOL/Imperative_HOL/Imperative_HOL.thy	Mon Jul 12 16:05:08 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy	Mon Jul 12 16:19:15 2010 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Entry point into monadic imperative HOL *}
     2.5  
     2.6  theory Imperative_HOL
     2.7 -imports Array Ref Relational
     2.8 +imports Array Ref Relational Mrec
     2.9  begin
    2.10  
    2.11  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Imperative_HOL/Mrec.thy	Mon Jul 12 16:19:15 2010 +0200
     3.3 @@ -0,0 +1,165 @@
     3.4 +theory Mrec
     3.5 +imports Heap_Monad
     3.6 +begin
     3.7 +
     3.8 +subsubsection {* A monadic combinator for simple recursive functions *}
     3.9 +
    3.10 +text {* Using a locale to fix arguments f and g of MREC *}
    3.11 +
    3.12 +locale mrec =
    3.13 +  fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
    3.14 +  and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
    3.15 +begin
    3.16 +
    3.17 +function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
    3.18 +  "mrec x h = (case execute (f x) h of
    3.19 +     Some (Inl r, h') \<Rightarrow> Some (r, h')
    3.20 +   | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
    3.21 +             Some (z, h'') \<Rightarrow> execute (g x s z) h''
    3.22 +           | None \<Rightarrow> None)
    3.23 +   | None \<Rightarrow> None)"
    3.24 +by auto
    3.25 +
    3.26 +lemma graph_implies_dom:
    3.27 +  "mrec_graph x y \<Longrightarrow> mrec_dom x"
    3.28 +apply (induct rule:mrec_graph.induct) 
    3.29 +apply (rule accpI)
    3.30 +apply (erule mrec_rel.cases)
    3.31 +by simp
    3.32 +
    3.33 +lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
    3.34 +  unfolding mrec_def 
    3.35 +  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
    3.36 +
    3.37 +lemma mrec_di_reverse: 
    3.38 +  assumes "\<not> mrec_dom (x, h)"
    3.39 +  shows "
    3.40 +   (case execute (f x) h of
    3.41 +     Some (Inl r, h') \<Rightarrow> False
    3.42 +   | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
    3.43 +   | None \<Rightarrow> False
    3.44 +   )" 
    3.45 +using assms apply (auto split: option.split sum.split)
    3.46 +apply (rule ccontr)
    3.47 +apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
    3.48 +done
    3.49 +
    3.50 +lemma mrec_rule:
    3.51 +  "mrec x h = 
    3.52 +   (case execute (f x) h of
    3.53 +     Some (Inl r, h') \<Rightarrow> Some (r, h')
    3.54 +   | Some (Inr s, h') \<Rightarrow> 
    3.55 +          (case mrec s h' of
    3.56 +             Some (z, h'') \<Rightarrow> execute (g x s z) h''
    3.57 +           | None \<Rightarrow> None)
    3.58 +   | None \<Rightarrow> None
    3.59 +   )"
    3.60 +apply (cases "mrec_dom (x,h)", simp)
    3.61 +apply (frule mrec_default)
    3.62 +apply (frule mrec_di_reverse, simp)
    3.63 +by (auto split: sum.split option.split simp: mrec_default)
    3.64 +
    3.65 +definition
    3.66 +  "MREC x = Heap_Monad.Heap (mrec x)"
    3.67 +
    3.68 +lemma MREC_rule:
    3.69 +  "MREC x = 
    3.70 +  (do y \<leftarrow> f x;
    3.71 +                (case y of 
    3.72 +                Inl r \<Rightarrow> return r
    3.73 +              | Inr s \<Rightarrow> 
    3.74 +                do z \<leftarrow> MREC s ;
    3.75 +                   g x s z
    3.76 +                done) done)"
    3.77 +  unfolding MREC_def
    3.78 +  unfolding bind_def return_def
    3.79 +  apply simp
    3.80 +  apply (rule ext)
    3.81 +  apply (unfold mrec_rule[of x])
    3.82 +  by (auto split: option.splits prod.splits sum.splits)
    3.83 +
    3.84 +lemma MREC_pinduct:
    3.85 +  assumes "execute (MREC x) h = Some (r, h')"
    3.86 +  assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
    3.87 +  assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
    3.88 +    \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
    3.89 +  shows "P x h h' r"
    3.90 +proof -
    3.91 +  from assms(1) have mrec: "mrec x h = Some (r, h')"
    3.92 +    unfolding MREC_def execute.simps .
    3.93 +  from mrec have dom: "mrec_dom (x, h)"
    3.94 +    apply -
    3.95 +    apply (rule ccontr)
    3.96 +    apply (drule mrec_default) by auto
    3.97 +  from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
    3.98 +    by auto
    3.99 +  from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
   3.100 +  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
   3.101 +    case (1 x h)
   3.102 +    obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
   3.103 +    show ?case
   3.104 +    proof (cases "execute (f x) h")
   3.105 +      case (Some result)
   3.106 +      then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
   3.107 +      note Inl' = this
   3.108 +      show ?thesis
   3.109 +      proof (cases a)
   3.110 +        case (Inl aa)
   3.111 +        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
   3.112 +          by auto
   3.113 +      next
   3.114 +        case (Inr b)
   3.115 +        note Inr' = this
   3.116 +        show ?thesis
   3.117 +        proof (cases "mrec b h1")
   3.118 +          case (Some result)
   3.119 +          then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
   3.120 +          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
   3.121 +            apply (intro 1(2))
   3.122 +            apply (auto simp add: Inr Inl')
   3.123 +            done
   3.124 +          moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
   3.125 +          ultimately show ?thesis
   3.126 +            apply auto
   3.127 +            apply (rule rec_case)
   3.128 +            apply auto
   3.129 +            unfolding MREC_def by auto
   3.130 +        next
   3.131 +          case None
   3.132 +          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
   3.133 +        qed
   3.134 +      qed
   3.135 +    next
   3.136 +      case None
   3.137 +      from this 1(1) mrec 1(3) show ?thesis by simp
   3.138 +    qed
   3.139 +  qed
   3.140 +  from this h'_r show ?thesis by simp
   3.141 +qed
   3.142 +
   3.143 +end
   3.144 +
   3.145 +text {* Providing global versions of the constant and the theorems *}
   3.146 +
   3.147 +abbreviation "MREC == mrec.MREC"
   3.148 +lemmas MREC_rule = mrec.MREC_rule
   3.149 +lemmas MREC_pinduct = mrec.MREC_pinduct
   3.150 +
   3.151 +lemma MREC_induct:
   3.152 +  assumes "crel (MREC f g x) h h' r"
   3.153 +  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
   3.154 +  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
   3.155 +    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
   3.156 +  shows "P x h h' r"
   3.157 +proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
   3.158 +  fix x h h1 h2 h' s z r
   3.159 +  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
   3.160 +    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
   3.161 +    "P s h1 h2 z"
   3.162 +    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
   3.163 +  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
   3.164 +  show "P x h h' r" .
   3.165 +next
   3.166 +qed (auto simp add: assms(2)[unfolded crel_def])
   3.167 +
   3.168 +end
     4.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:05:08 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:19:15 2010 +0200
     4.3 @@ -193,21 +193,4 @@
     4.4      done
     4.5  qed
     4.6  
     4.7 -lemma MREC_induct:
     4.8 -  assumes "crel (MREC f g x) h h' r"
     4.9 -  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
    4.10 -  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
    4.11 -    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
    4.12 -  shows "P x h h' r"
    4.13 -proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
    4.14 -  fix x h h1 h2 h' s z r
    4.15 -  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
    4.16 -    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
    4.17 -    "P s h1 h2 z"
    4.18 -    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
    4.19 -  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
    4.20 -  show "P x h h' r" .
    4.21 -next
    4.22 -qed (auto simp add: assms(2)[unfolded crel_def])
    4.23 -
    4.24  end
     5.1 --- a/src/HOL/IsaMakefile	Mon Jul 12 16:05:08 2010 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Mon Jul 12 16:19:15 2010 +0200
     5.3 @@ -810,17 +810,17 @@
     5.4  
     5.5  HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
     5.6  
     5.7 -$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
     5.8 -  Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
     5.9 -  Imperative_HOL/Relational.thy \
    5.10 -  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \
    5.11 -  Imperative_HOL/Imperative_HOL_ex.thy \
    5.12 -  Imperative_HOL/ex/Imperative_Quicksort.thy \
    5.13 -  Imperative_HOL/ex/Imperative_Reverse.thy \
    5.14 -  Imperative_HOL/ex/Linked_Lists.thy \
    5.15 -  Imperative_HOL/ex/SatChecker.thy \
    5.16 -  Imperative_HOL/ex/Sorted_List.thy \
    5.17 -  Imperative_HOL/ex/Subarray.thy \
    5.18 +$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy	\
    5.19 +  Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy			\
    5.20 +  Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\
    5.21 +  Imperative_HOL/Mrec.thy Imperative_HOL/Relational.thy			\
    5.22 +  Imperative_HOL/Ref.thy						\
    5.23 +  Imperative_HOL/ex/Imperative_Quicksort.thy				\
    5.24 +  Imperative_HOL/ex/Imperative_Reverse.thy				\
    5.25 +  Imperative_HOL/ex/Linked_Lists.thy					\
    5.26 +  Imperative_HOL/ex/SatChecker.thy					\
    5.27 +  Imperative_HOL/ex/Sorted_List.thy					\
    5.28 +  Imperative_HOL/ex/Subarray.thy					\
    5.29    Imperative_HOL/ex/Sublist.thy
    5.30  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
    5.31