src/HOL/ex/FinFunPred.thy
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 48059 f6ce99d3719b
child 52729 412c9e0381a1
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     1
(*  Author:     Andreas Lochbihler *)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     2
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     3
header {*
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     4
  Predicates modelled as FinFuns
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     5
*}
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     6
48041
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents: 48038
diff changeset
     7
theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     8
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
     9
text {* Instantiate FinFun predicates just like predicates *}
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    10
48034
1c5171abe5cc removed subscripts from FinFun type syntax
Andreas Lochbihler
parents: 48029
diff changeset
    11
type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>f bool"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    12
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    13
instantiation "finfun" :: (type, ord) ord
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    14
begin
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    15
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    16
definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    17
48034
1c5171abe5cc removed subscripts from FinFun type syntax
Andreas Lochbihler
parents: 48029
diff changeset
    18
definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    19
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    20
instance ..
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    21
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    22
lemma le_finfun_code [code]:
48038
72a8506dd59b eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents: 48037
diff changeset
    23
  "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    24
by(simp add: le_finfun_def finfun_All_All o_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    25
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    26
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    27
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    28
instance "finfun" :: (type, preorder) preorder
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    29
  by(intro_classes)(auto simp add: less_finfun_def le_finfun_def intro: order_trans)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    30
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    31
instance "finfun" :: (type, order) order
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    32
by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    33
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    34
instantiation "finfun" :: (type, bot) bot begin
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    35
definition "bot = finfun_const bot"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    36
instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    37
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    38
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    39
lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    40
by(auto simp add: bot_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    41
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    42
instantiation "finfun" :: (type, top) top begin
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    43
definition "top = finfun_const top"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    44
instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    45
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    46
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    47
lemma top_finfun_apply [simp]: "op $ top = (\<lambda>_. top)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    48
by(auto simp add: top_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    49
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    50
instantiation "finfun" :: (type, inf) inf begin
48038
72a8506dd59b eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents: 48037
diff changeset
    51
definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ ($f, g$)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    52
instance ..
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    53
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    54
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    55
lemma inf_finfun_apply [simp]: "op $ (inf f g) = inf (op $ f) (op $ g)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    56
by(auto simp add: inf_finfun_def o_def inf_fun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    57
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    58
instantiation "finfun" :: (type, sup) sup begin
48038
72a8506dd59b eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents: 48037
diff changeset
    59
definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ ($f, g$)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    60
instance ..
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    61
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    62
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    63
lemma sup_finfun_apply [simp]: "op $ (sup f g) = sup (op $ f) (op $ g)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    64
by(auto simp add: sup_finfun_def o_def sup_fun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    65
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    66
instance "finfun" :: (type, semilattice_inf) semilattice_inf
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    67
by(intro_classes)(simp_all add: inf_finfun_def le_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    68
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    69
instance "finfun" :: (type, semilattice_sup) semilattice_sup
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    70
by(intro_classes)(simp_all add: sup_finfun_def le_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    71
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    72
instance "finfun" :: (type, lattice) lattice ..
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    73
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    74
instance "finfun" :: (type, bounded_lattice) bounded_lattice
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    75
by(intro_classes)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    76
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    77
instance "finfun" :: (type, distrib_lattice) distrib_lattice
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    78
by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    79
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    80
instantiation "finfun" :: (type, minus) minus begin
48038
72a8506dd59b eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents: 48037
diff changeset
    81
definition "f - g = split (op -) \<circ>$ ($f, g$)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    82
instance ..
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    83
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    84
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    85
lemma minus_finfun_apply [simp]: "op $ (f - g) = op $ f - op $ g"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    86
by(simp add: minus_finfun_def o_def fun_diff_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    87
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    88
instantiation "finfun" :: (type, uminus) uminus begin
48037
6c4b3e78f03e syntax for FinFun composition without subscripts
Andreas Lochbihler
parents: 48036
diff changeset
    89
definition "- A = uminus \<circ>$ A"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    90
instance ..
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    91
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    92
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
    93
lemma uminus_finfun_apply [simp]: "op $ (- g) = - op $ g"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    94
by(simp add: uminus_finfun_def o_def fun_Compl_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    95
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    96
instance "finfun" :: (type, boolean_algebra) boolean_algebra
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    97
by(intro_classes)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    98
  (simp_all add: uminus_finfun_def inf_finfun_def expand_finfun_eq sup_fun_def inf_fun_def fun_Compl_def o_def inf_compl_bot sup_compl_top diff_eq)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
    99
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   100
text {*
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   101
  Replicate predicate operations for FinFuns
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   102
*}
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   103
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   104
abbreviation finfun_empty :: "'a pred\<^isub>f" ("{}\<^isub>f")
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   105
where "{}\<^isub>f \<equiv> bot"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   106
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   107
abbreviation finfun_UNIV :: "'a pred\<^isub>f" 
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   108
where "finfun_UNIV \<equiv> top"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   109
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   110
definition finfun_single :: "'a \<Rightarrow> 'a pred\<^isub>f"
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   111
where [code]: "finfun_single x = finfun_empty(x $:= True)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   112
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   113
lemma finfun_single_apply [simp]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   114
  "finfun_single x $ y \<longleftrightarrow> x = y"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   115
by(simp add: finfun_single_def finfun_upd_apply)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   116
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   117
lemma [iff]:
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   118
  shows finfun_single_neq_bot: "finfun_single x \<noteq> bot" 
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   119
  and bot_neq_finfun_single: "bot \<noteq> finfun_single x"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   120
by(simp_all add: expand_finfun_eq fun_eq_iff)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   121
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   122
lemma finfun_leI [intro!]: "(!!x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   123
by(simp add: le_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   124
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   125
lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A $ x \<rbrakk> \<Longrightarrow> B $ x"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   126
by(simp add: le_finfun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   127
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   128
text {* Bounded quantification.
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   129
  Warning: @{text "finfun_Ball"} and @{text "finfun_Ex"} may raise an exception, they should not be used for quickcheck
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   130
*}
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   131
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   132
definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   133
where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   134
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   135
lemma finfun_Ball_except_const:
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   136
  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   137
by(auto simp add: finfun_Ball_except_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   138
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   139
lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   140
  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   141
by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   142
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   143
lemma finfun_Ball_except_update:
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   144
  "finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   145
by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   146
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   147
lemma finfun_Ball_except_update_code [code]:
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   148
  fixes a :: "'a :: card_UNIV"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   149
  shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   150
by(simp add: finfun_Ball_except_update)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   151
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   152
definition finfun_Ball :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   153
where [code del]: "finfun_Ball A P = Ball {x. A $ x} P"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   154
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   155
lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   156
by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   157
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   158
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   159
definition finfun_Bex_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   160
where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   161
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   162
lemma finfun_Bex_except_const:
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   163
  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   164
by(auto simp add: finfun_Bex_except_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   165
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   166
lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   167
  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   168
by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   169
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   170
lemma finfun_Bex_except_update: 
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   171
  "finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   172
by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   173
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   174
lemma finfun_Bex_except_update_code [code]:
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   175
  fixes a :: "'a :: card_UNIV"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   176
  shows "finfun_Bex_except xs (finfun_update_code f a b) P \<longleftrightarrow> ((a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) f P)"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   177
by(simp add: finfun_Bex_except_update)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   178
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   179
definition finfun_Bex :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   180
where [code del]: "finfun_Bex A P = Bex {x. A $ x} P"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   181
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   182
lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   183
by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   184
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   185
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   186
text {* Automatically replace predicate operations by finfun predicate operations where possible *}
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   187
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   188
lemma iso_finfun_le [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   189
  "op $ A \<le> op $ B \<longleftrightarrow> A \<le> B"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   190
by (metis le_finfun_def le_funD le_funI)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   191
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   192
lemma iso_finfun_less [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   193
  "op $ A < op $ B \<longleftrightarrow> A < B"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   194
by (metis iso_finfun_le less_finfun_def less_fun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   195
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   196
lemma iso_finfun_eq [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   197
  "op $ A = op $ B \<longleftrightarrow> A = B"
48029
9d9c9069abbc unify Rep_finfun and finfun_apply
Andreas Lochbihler
parents: 48028
diff changeset
   198
by(simp only: expand_finfun_eq)
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   199
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   200
lemma iso_finfun_sup [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   201
  "sup (op $ A) (op $ B) = op $ (sup A B)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   202
by(simp)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   203
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   204
lemma iso_finfun_disj [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   205
  "A $ x \<or> B $ x \<longleftrightarrow> sup A B $ x"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   206
by(simp add: sup_fun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   207
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   208
lemma iso_finfun_inf [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   209
  "inf (op $ A) (op $ B) = op $ (inf A B)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   210
by(simp)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   211
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   212
lemma iso_finfun_conj [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   213
  "A $ x \<and> B $ x \<longleftrightarrow> inf A B $ x"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   214
by(simp add: inf_fun_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   215
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   216
lemma iso_finfun_empty_conv [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   217
  "(\<lambda>_. False) = op $ {}\<^isub>f"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   218
by simp
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   219
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   220
lemma iso_finfun_UNIV_conv [code_unfold]:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   221
  "(\<lambda>_. True) = op $ finfun_UNIV"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   222
by simp
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   223
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   224
lemma iso_finfun_upd [code_unfold]:
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   225
  fixes A :: "'a pred\<^isub>f"
48036
1edcd5f73505 FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents: 48035
diff changeset
   226
  shows "(op $ A)(x := b) = op $ (A(x $:= b))"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   227
by(simp add: fun_eq_iff)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   228
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   229
lemma iso_finfun_uminus [code_unfold]:
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   230
  fixes A :: "'a pred\<^isub>f"
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   231
  shows "- op $ A = op $ (- A)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   232
by(simp)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   233
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   234
lemma iso_finfun_minus [code_unfold]:
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   235
  fixes A :: "'a pred\<^isub>f"
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   236
  shows "op $ A - op $ B = op $ (A - B)"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   237
by(simp)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   238
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   239
text {*
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   240
  Do not declare the following two theorems as @{text "[code_unfold]"},
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   241
  because this causes quickcheck to fail frequently when bounded quantification is used which raises an exception.
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   242
  For code generation, the same problems occur, but then, no randomly generated FinFun is usually around.
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   243
*}
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   244
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   245
lemma iso_finfun_Ball_Ball:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   246
  "(\<forall>x. A $ x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   247
by(simp add: finfun_Ball_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   248
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   249
lemma iso_finfun_Bex_Bex:
48035
2f9584581cf2 replace FinFun application syntax with $
Andreas Lochbihler
parents: 48034
diff changeset
   250
  "(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   251
by(simp add: finfun_Bex_def)
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   252
48037
6c4b3e78f03e syntax for FinFun composition without subscripts
Andreas Lochbihler
parents: 48036
diff changeset
   253
text {* Test code setup *}
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   254
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   255
notepad begin
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   256
have "inf ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) ((\<lambda>_. True)(3 := False)) \<le> 
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   257
      sup ((\<lambda>_. False)(1 := True, 5 := True)) (- ((\<lambda>_. True)(2 := False, 3 := False)))"
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   258
  by eval
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   259
end
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   260
48059
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   261
declare iso_finfun_Ball_Ball[code_unfold]
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   262
notepad begin
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   263
have "(\<forall>x. ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) x \<longrightarrow> x < 3)"
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   264
  by eval
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   265
end
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   266
declare iso_finfun_Ball_Ball[code_unfold del]
f6ce99d3719b simplify card_UNIV type class,
Andreas Lochbihler
parents: 48041
diff changeset
   267
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents:
diff changeset
   268
end