src/HOL/Partial_Function.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 73411 1f1366966296
child 75669 43f5dfb7fa35
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
     1
(* Title:    HOL/Partial_Function.thy
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
     2
   Author:   Alexander Krauss, TU Muenchen
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
     3
*)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
     5
section \<open>Partial Function Definitions\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
     6
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
     7
theory Partial_Function
66364
fa3247e6ee4b tuning imports
blanchet
parents: 64634
diff changeset
     8
  imports Complete_Partial_Order Option
69913
ca515cf61651 more specific keyword kinds;
wenzelm
parents: 69745
diff changeset
     9
  keywords "partial_function" :: thy_defn
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    10
begin
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    11
57959
1bfed12a7646 updated to named_theorems;
wenzelm
parents: 55085
diff changeset
    12
named_theorems partial_function_mono "monotonicity rules for partial function definitions"
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    13
ML_file \<open>Tools/Function/partial_function.ML\<close>
57959
1bfed12a7646 updated to named_theorems;
wenzelm
parents: 55085
diff changeset
    14
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    15
lemma (in ccpo) in_chain_finite:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    16
  assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}"
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    17
  shows "\<Squnion>A \<in> A"
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    18
using assms(2,1,3)
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    19
proof induction
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    20
  case empty thus ?case by simp
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    21
next
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    22
  case (insert x A)
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    23
  note chain = \<open>Complete_Partial_Order.chain (\<le>) (insert x A)\<close>
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    24
  show ?case
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    25
  proof(cases "A = {}")
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    26
    case True thus ?thesis by simp
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    27
  next
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    28
    case False
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    29
    from chain have chain': "Complete_Partial_Order.chain (\<le>) A"
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    30
      by(rule chain_subset) blast
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    31
    hence "\<Squnion>A \<in> A" using False by(rule insert.IH)
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    32
    show ?thesis
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    33
    proof(cases "x \<le> \<Squnion>A")
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    34
      case True
69745
aec42cee2521 more canonical and less specialized syntax
nipkow
parents: 69605
diff changeset
    35
      have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    36
        by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
69745
aec42cee2521 more canonical and less specialized syntax
nipkow
parents: 69605
diff changeset
    37
      hence "\<Squnion>(insert x A) = \<Squnion>A"
73411
1f1366966296 avoid name clash
haftmann
parents: 69913
diff changeset
    38
        by(rule order.antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
    39
      with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    40
    next
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    41
      case False
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
    42
      with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close>
69745
aec42cee2521 more canonical and less specialized syntax
nipkow
parents: 69605
diff changeset
    43
      have "\<Squnion>(insert x A) = x"
73411
1f1366966296 avoid name clash
haftmann
parents: 69913
diff changeset
    44
        by(auto intro: order.antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
60062
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    45
      thus ?thesis by simp
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    46
    qed
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    47
  qed
4c5de5a860ee move lemma from AFP/Coinductive
Andreas Lochbihler
parents: 59647
diff changeset
    48
qed
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    49
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62390
diff changeset
    50
lemma (in ccpo) admissible_chfin:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    51
  "(\<forall>S. Complete_Partial_Order.chain (\<le>) S \<longrightarrow> finite S)
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    52
  \<Longrightarrow> ccpo.admissible Sup (\<le>) P"
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62390
diff changeset
    53
using in_chain_finite by (blast intro: ccpo.admissibleI)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62390
diff changeset
    54
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
    55
subsection \<open>Axiomatic setup\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    56
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
    57
text \<open>This techical locale constains the requirements for function
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
    58
  definitions with ccpo fixed points.\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    59
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    60
definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    61
definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    62
definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    63
definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    64
43081
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    65
lemma chain_fun: 
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    66
  assumes A: "chain (fun_ord ord) A"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    67
  shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    68
proof (rule chainI)
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    69
  fix x y assume "x \<in> ?C" "y \<in> ?C"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    70
  then obtain f g where fg: "f \<in> A" "g \<in> A" 
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    71
    and [simp]: "x = f a" "y = g a" by blast
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    72
  from chainD[OF A fg]
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    73
  show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    74
qed
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
    75
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    76
lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    77
by (rule monotoneI) (auto simp: fun_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    78
40288
520199d8b66e added rule let_mono
krauss
parents: 40252
diff changeset
    79
lemma let_mono[partial_function_mono]:
520199d8b66e added rule let_mono
krauss
parents: 40252
diff changeset
    80
  "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
520199d8b66e added rule let_mono
krauss
parents: 40252
diff changeset
    81
  \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
520199d8b66e added rule let_mono
krauss
parents: 40252
diff changeset
    82
by (simp add: Let_def)
520199d8b66e added rule let_mono
krauss
parents: 40252
diff changeset
    83
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    84
lemma if_mono[partial_function_mono]: "monotone orda ordb F 
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    85
\<Longrightarrow> monotone orda ordb G
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    86
\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    87
unfolding monotone_def by simp
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    88
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    89
definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    90
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    91
locale partial_function_definitions = 
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    92
  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    93
  fixes lub :: "'a set \<Rightarrow> 'a"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    94
  assumes leq_refl: "leq x x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    95
  assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    96
  assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    97
  assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    98
  assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
    99
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   100
lemma partial_function_lift:
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   101
  assumes "partial_function_definitions ord lb"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   102
  shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   103
proof -
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   104
  interpret partial_function_definitions ord lb by fact
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   105
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   106
  show ?thesis
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   107
  proof
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   108
    fix x show "?ordf x x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   109
      unfolding fun_ord_def by (auto simp: leq_refl)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   110
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   111
    fix x y z assume "?ordf x y" "?ordf y z"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   112
    thus "?ordf x z" unfolding fun_ord_def 
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   113
      by (force dest: leq_trans)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   114
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   115
    fix x y assume "?ordf x y" "?ordf y x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   116
    thus "x = y" unfolding fun_ord_def
43081
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   117
      by (force intro!: dest: leq_antisym)
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   118
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   119
    fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   120
    thus "?ordf f (?lubf A)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   121
      unfolding fun_lub_def fun_ord_def
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   122
      by (blast intro: lub_upper chain_fun[OF A] f)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   123
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   124
    fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   125
    assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   126
    show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   127
      by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   128
   qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   129
qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   130
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   131
lemma ccpo: assumes "partial_function_definitions ord lb"
46041
1e3ff542e83e remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents: 45297
diff changeset
   132
  shows "class.ccpo lb ord (mk_less ord)"
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   133
using assms unfolding partial_function_definitions_def mk_less_def
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   134
by unfold_locales blast+
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   135
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   136
lemma partial_function_image:
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   137
  assumes "partial_function_definitions ord Lub"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   138
  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   139
  assumes inv: "\<And>x. f (g x) = x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   140
  shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   141
proof -
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   142
  let ?iord = "img_ord f ord"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   143
  let ?ilub = "img_lub f g Lub"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   144
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   145
  interpret partial_function_definitions ord Lub by fact
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   146
  show ?thesis
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   147
  proof
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   148
    fix A x assume "chain ?iord A" "x \<in> A"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   149
    then have "chain ord (f ` A)" "f x \<in> f ` A"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   150
      by (auto simp: img_ord_def intro: chainI dest: chainD)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   151
    thus "?iord x (?ilub A)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   152
      unfolding inv img_lub_def img_ord_def by (rule lub_upper)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   153
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   154
    fix A x assume "chain ?iord A"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   155
      and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   156
    then have "chain ord (f ` A)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   157
      by (auto simp: img_ord_def intro: chainI dest: chainD)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   158
    thus "?iord (?ilub A) x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   159
      unfolding inv img_lub_def img_ord_def
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   160
      by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   161
  qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   162
qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   163
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   164
context partial_function_definitions
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   165
begin
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   166
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   167
abbreviation "le_fun \<equiv> fun_ord leq"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   168
abbreviation "lub_fun \<equiv> fun_lub lub"
46041
1e3ff542e83e remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents: 45297
diff changeset
   169
abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun"
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   170
abbreviation "mono_body \<equiv> monotone le_fun leq"
46041
1e3ff542e83e remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents: 45297
diff changeset
   171
abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun"
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   172
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   173
text \<open>Interpret manually, to avoid flooding everything with facts about
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   174
  orders\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   175
46041
1e3ff542e83e remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents: 45297
diff changeset
   176
lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)"
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   177
apply (rule ccpo)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   178
apply (rule partial_function_lift)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   179
apply (rule partial_function_definitions_axioms)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   180
done
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   181
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   182
text \<open>The crucial fixed-point theorem\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   183
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   184
lemma mono_body_fixp: 
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   185
  "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   186
by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   187
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   188
text \<open>Version with curry/uncurry combinators, to be used by package\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   189
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   190
lemma fixp_rule_uc:
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   191
  fixes F :: "'c \<Rightarrow> 'c" and
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   192
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   193
    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   194
  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   195
  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   196
  assumes inverse: "\<And>f. C (U f) = f"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   197
  shows "f = F f"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   198
proof -
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   199
  have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   200
  also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   201
    by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   202
  also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   203
  also have "... = F f" by (simp add: eq)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   204
  finally show "f = F f" .
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   205
qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   206
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   207
text \<open>Fixpoint induction rule\<close>
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   208
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   209
lemma fixp_induct_uc:
59647
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   210
  fixes F :: "'c \<Rightarrow> 'c"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   211
    and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   212
    and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   213
    and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   214
  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
59647
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   215
    and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   216
    and inverse: "\<And>f. U (C f) = f"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   217
    and adm: "ccpo.admissible lub_fun le_fun P"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   218
    and bot: "P (\<lambda>_. lub {})"
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   219
    and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   220
  shows "P (U f)"
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   221
unfolding eq inverse
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   222
apply (rule ccpo.fixp_induct[OF ccpo adm])
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   223
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
59647
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   224
apply (rule_tac f5="C x" in step)
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   225
apply (simp add: inverse)
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 59517
diff changeset
   226
done
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   227
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   228
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67399
diff changeset
   229
text \<open>Rules for \<^term>\<open>mono_body\<close>:\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   230
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   231
lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   232
by (rule monotoneI) (rule leq_refl)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   233
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   234
end
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   235
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   236
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   237
subsection \<open>Flat interpretation: tailrec and option\<close>
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   238
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   239
definition 
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   240
  "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   241
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   242
definition 
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   243
  "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   244
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   245
lemma flat_interpretation:
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   246
  "partial_function_definitions (flat_ord b) (flat_lub b)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   247
proof
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   248
  fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   249
  show "flat_ord b x (flat_lub b A)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   250
  proof cases
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   251
    assume "x = b"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   252
    thus ?thesis by (simp add: flat_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   253
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   254
    assume "x \<noteq> b"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   255
    with 1 have "A - {b} = {x}"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   256
      by (auto elim: chainE simp: flat_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   257
    then have "flat_lub b A = x"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   258
      by (auto simp: flat_lub_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   259
    thus ?thesis by (auto simp: flat_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   260
  qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   261
next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   262
  fix A z assume A: "chain (flat_ord b) A"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   263
    and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   264
  show "flat_ord b (flat_lub b A) z"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   265
  proof cases
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   266
    assume "A \<subseteq> {b}"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   267
    thus ?thesis
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   268
      by (auto simp: flat_lub_def flat_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   269
  next
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   270
    assume nb: "\<not> A \<subseteq> {b}"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   271
    then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   272
    with A have "A - {b} = {y}"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   273
      by (auto elim: chainE simp: flat_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   274
    with nb have "flat_lub b A = y"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   275
      by (auto simp: flat_lub_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   276
    with z y show ?thesis by auto    
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   277
  qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   278
qed (auto simp: flat_ord_def)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   279
59517
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   280
lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y"
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   281
by(auto simp add: flat_ord_def)
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   282
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   283
lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   284
by(auto simp add: flat_ord_def)
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   285
64634
5bd30359e46e proper logical constants
haftmann
parents: 63561
diff changeset
   286
lemma antisymp_flat_ord: "antisymp (flat_ord a)"
5bd30359e46e proper logical constants
haftmann
parents: 63561
diff changeset
   287
by(rule antisympI)(auto dest: flat_ord_antisym)
59517
22c9e6cf5572 add lemmas about flat_ord
Andreas Lochbihler
parents: 58889
diff changeset
   288
61605
1bf7b186542e qualifier is mandatory by default;
wenzelm
parents: 61566
diff changeset
   289
interpretation tailrec:
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   290
  partial_function_definitions "flat_ord undefined" "flat_lub undefined"
61566
c3d6e570ccef Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents: 60758
diff changeset
   291
  rewrites "flat_lub undefined {} \<equiv> undefined"
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   292
by (rule flat_interpretation)(simp add: flat_lub_def)
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   293
61605
1bf7b186542e qualifier is mandatory by default;
wenzelm
parents: 61566
diff changeset
   294
interpretation option:
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   295
  partial_function_definitions "flat_ord None" "flat_lub None"
61566
c3d6e570ccef Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents: 60758
diff changeset
   296
  rewrites "flat_lub None {} \<equiv> None"
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   297
by (rule flat_interpretation)(simp add: flat_lub_def)
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   298
42949
618adb3584e5 separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
krauss
parents: 40288
diff changeset
   299
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   300
abbreviation "tailrec_ord \<equiv> flat_ord undefined"
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   301
abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord"
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   302
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   303
lemma tailrec_admissible:
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   304
  "ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c))
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   305
     (\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> P x (a x))"
53361
1cb7d3c0cf31 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents: 52728
diff changeset
   306
proof(intro ccpo.admissibleI strip)
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   307
  fix A x
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   308
  assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A"
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   309
    and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)"
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   310
    and defined: "fun_lub (flat_lub c) A x \<noteq> c"
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   311
  from defined obtain f where f: "f \<in> A" "f x \<noteq> c"
62390
842917225d56 more canonical names
nipkow
parents: 61841
diff changeset
   312
    by(auto simp add: fun_lub_def flat_lub_def split: if_split_asm)
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   313
  hence "P x (f x)" by(rule P)
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   314
  moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x"
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   315
    by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   316
  hence "fun_lub (flat_lub c) A x = f x"
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   317
    using f by(auto simp add: fun_lub_def flat_lub_def)
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   318
  ultimately show "P x (fun_lub (flat_lub c) A x)" by simp
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   319
qed
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   320
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   321
lemma fixp_induct_tailrec:
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   322
  fixes F :: "'c \<Rightarrow> 'c" and
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   323
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   324
    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   325
    P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   326
    x :: "'b"
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   327
  assumes mono: "\<And>x. monotone (fun_ord (flat_ord c)) (flat_ord c) (\<lambda>f. U (F (C f)) x)"
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   328
  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (\<lambda>f. U (F (C f))))"
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   329
  assumes inverse2: "\<And>f. U (C f) = f"
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   330
  assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y"
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   331
  assumes result: "U f x = y"
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   332
  assumes defined: "y \<noteq> c"
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   333
  shows "P x y"
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   334
proof -
53949
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   335
  have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y"
021a8ef97f5f generalise lemma
Andreas Lochbihler
parents: 53361
diff changeset
   336
    by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   337
      (auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def)
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   338
  thus ?thesis using result defined by blast
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   339
qed
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   340
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   341
lemma admissible_image:
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   342
  assumes pfun: "partial_function_definitions le lub"
67091
1393c2340eec more symbols;
wenzelm
parents: 66364
diff changeset
   343
  assumes adm: "ccpo.admissible lub le (P \<circ> g)"
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   344
  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   345
  assumes inv: "\<And>x. f (g x) = x"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   346
  shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
53361
1cb7d3c0cf31 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents: 52728
diff changeset
   347
proof (rule ccpo.admissibleI)
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   348
  fix A assume "chain (img_ord f le) A"
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   349
  then have ch': "chain le (f ` A)"
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   350
    by (auto simp: img_ord_def intro: chainI dest: chainD)
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   351
  assume "A \<noteq> {}"
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   352
  assume P_A: "\<forall>x\<in>A. P x"
67091
1393c2340eec more symbols;
wenzelm
parents: 66364
diff changeset
   353
  have "(P \<circ> g) (lub (f ` A))" using adm ch'
53361
1cb7d3c0cf31 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents: 52728
diff changeset
   354
  proof (rule ccpo.admissibleD)
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   355
    fix x assume "x \<in> f ` A"
67091
1393c2340eec more symbols;
wenzelm
parents: 66364
diff changeset
   356
    with P_A show "(P \<circ> g) x" by (auto simp: inj[OF inv])
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   357
  qed(simp add: \<open>A \<noteq> {}\<close>)
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   358
  thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   359
qed
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   360
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   361
lemma admissible_fun:
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   362
  assumes pfun: "partial_function_definitions le lub"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   363
  assumes adm: "\<And>x. ccpo.admissible lub le (Q x)"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   364
  shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))"
53361
1cb7d3c0cf31 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents: 52728
diff changeset
   365
proof (rule ccpo.admissibleI)
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   366
  fix A :: "('b \<Rightarrow> 'a) set"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   367
  assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   368
  assume ch: "chain (fun_ord le) A"
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   369
  assume "A \<noteq> {}"
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   370
  hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   371
  show "\<forall>x. Q x (fun_lub lub A x)"
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   372
    unfolding fun_lub_def
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   373
    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty])
51485
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   374
      (auto simp: Q)
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   375
qed
637aa1649ac7 added rudimentary induction rule for partial_function (heap)
krauss
parents: 51459
diff changeset
   376
51459
bc3651180a09 add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents: 48891
diff changeset
   377
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   378
abbreviation "option_ord \<equiv> flat_ord None"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   379
abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   380
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   381
lemma bind_mono[partial_function_mono]:
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   382
assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   383
shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   384
proof (rule monotoneI)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   385
  fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   386
  with mf
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   387
  have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   388
  then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   389
    unfolding flat_ord_def by auto    
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   390
  also from mg
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   391
  have "\<And>y'. option_ord (C y' f) (C y' g)"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   392
    by (rule monotoneD) (rule fg)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   393
  then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   394
    unfolding flat_ord_def by (cases "B g") auto
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   395
  finally (option.leq_trans)
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   396
  show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   397
qed
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   398
43081
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   399
lemma flat_lub_in_chain:
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   400
  assumes ch: "chain (flat_ord b) A "
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   401
  assumes lub: "flat_lub b A = a"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   402
  shows "a = b \<or> a \<in> A"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   403
proof (cases "A \<subseteq> {b}")
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   404
  case True
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   405
  then have "flat_lub b A = b" unfolding flat_lub_def by simp
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   406
  with lub show ?thesis by simp
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   407
next
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   408
  case False
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   409
  then obtain c where "c \<in> A" and "c \<noteq> b" by auto
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   410
  { fix z assume "z \<in> A"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   411
    from chainD[OF ch \<open>c \<in> A\<close> this] have "z = c \<or> z = b"
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   412
      unfolding flat_ord_def using \<open>c \<noteq> b\<close> by auto }
43081
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   413
  with False have "A - {b} = {c}" by auto
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   414
  with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   415
  with \<open>c \<in> A\<close> lub show ?thesis by simp
43081
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   416
qed
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   417
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   418
lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   419
  (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
53361
1cb7d3c0cf31 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents: 52728
diff changeset
   420
proof (rule ccpo.admissibleI)
43081
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   421
  fix A :: "('a \<Rightarrow> 'b option) set"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   422
  assume ch: "chain option.le_fun A"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   423
    and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   424
  from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   425
  show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   426
  proof (intro allI impI)
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   427
    fix x y assume "option.lub_fun A x = Some y"
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   428
    from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   429
    have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   430
    then have "\<exists>f\<in>A. f x = Some y" by auto
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   431
    with IH show "P x y" by auto
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   432
  qed
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   433
qed
1a39c9898ae6 admissibility on option type
krauss
parents: 43080
diff changeset
   434
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   435
lemma fixp_induct_option:
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   436
  fixes F :: "'c \<Rightarrow> 'c" and
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   437
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   438
    C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   439
    P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   440
  assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
46041
1e3ff542e83e remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents: 45297
diff changeset
   441
  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))"
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   442
  assumes inverse2: "\<And>f. U (C f) = f"
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   443
  assumes step: "\<And>f x y. (\<And>x y. U f x = Some y \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = Some y \<Longrightarrow> P x y"
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   444
  assumes defined: "U f x = Some y"
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   445
  shows "P x y"
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   446
  using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
54630
9061af4d5ebc restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents: 53949
diff changeset
   447
  unfolding fun_lub_def flat_lub_def by(auto 9 2)
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   448
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67399
diff changeset
   449
declaration \<open>Partial_Function.init "tailrec" \<^term>\<open>tailrec.fixp_fun\<close>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67399
diff changeset
   450
  \<^term>\<open>tailrec.mono_body\<close> @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 61605
diff changeset
   451
  (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   452
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67399
diff changeset
   453
declaration \<open>Partial_Function.init "option" \<^term>\<open>option.fixp_fun\<close>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67399
diff changeset
   454
  \<^term>\<open>option.mono_body\<close> @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60062
diff changeset
   455
  (SOME @{thm fixp_induct_option})\<close>
43082
8d0c44de9773 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents: 43081
diff changeset
   456
40252
029400b6c893 hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
krauss
parents: 40107
diff changeset
   457
hide_const (open) chain
40107
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   458
374f3ef9f940 first version of partial_function package
krauss
parents:
diff changeset
   459
end