src/HOL/Predicate.thy
changeset 33111 db5af7b86a2f
parent 33110 16f2814653ed
child 33607 9b3c4e95380e
     1.1 --- a/src/HOL/Predicate.thy	Sat Oct 24 16:55:42 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Sat Oct 24 16:55:42 2009 +0200
     1.3 @@ -471,8 +471,8 @@
     1.4    "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
     1.5    by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
     1.6  
     1.7 -definition singleton :: "'a \<Rightarrow> 'a pred \<Rightarrow> 'a" where
     1.8 -  "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault)"
     1.9 +definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
    1.10 +  "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
    1.11  
    1.12  lemma singleton_eqI:
    1.13    "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x"
    1.14 @@ -501,11 +501,11 @@
    1.15  qed
    1.16  
    1.17  lemma singleton_undefinedI:
    1.18 -  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault"
    1.19 +  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()"
    1.20    by (simp add: singleton_def)
    1.21  
    1.22  lemma singleton_bot:
    1.23 -  "singleton dfault \<bottom> = dfault"
    1.24 +  "singleton dfault \<bottom> = dfault ()"
    1.25    by (auto simp add: bot_pred_def intro: singleton_undefinedI)
    1.26  
    1.27  lemma singleton_single:
    1.28 @@ -513,7 +513,7 @@
    1.29    by (auto simp add: intro: singleton_eqI singleI elim: singleE)
    1.30  
    1.31  lemma singleton_sup_single_single:
    1.32 -  "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault)"
    1.33 +  "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())"
    1.34  proof (cases "x = y")
    1.35    case True then show ?thesis by (simp add: singleton_single)
    1.36  next
    1.37 @@ -523,7 +523,7 @@
    1.38    by (auto intro: supI1 supI2 singleI)
    1.39    with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
    1.40      by blast
    1.41 -  then have "singleton dfault (single x \<squnion> single y) = dfault"
    1.42 +  then have "singleton dfault (single x \<squnion> single y) = dfault ()"
    1.43      by (rule singleton_undefinedI)
    1.44    with False show ?thesis by simp
    1.45  qed
    1.46 @@ -538,10 +538,10 @@
    1.47  next
    1.48    case False
    1.49    from False have A_or_B:
    1.50 -    "singleton dfault A = dfault \<or> singleton dfault B = dfault"
    1.51 +    "singleton dfault A = dfault () \<or> singleton dfault B = dfault ()"
    1.52      by (auto intro!: singleton_undefinedI)
    1.53    then have rhs: "singleton dfault
    1.54 -    (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault"
    1.55 +    (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()"
    1.56      by (auto simp add: singleton_sup_single_single singleton_single)
    1.57    from False have not_unique:
    1.58      "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
    1.59 @@ -551,7 +551,7 @@
    1.60        by (blast elim: not_bot)
    1.61      with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
    1.62        by (auto simp add: sup_pred_def bot_pred_def)
    1.63 -    then have "singleton dfault (A \<squnion> B) = dfault" by (rule singleton_undefinedI)
    1.64 +    then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI)
    1.65      with True rhs show ?thesis by simp
    1.66    next
    1.67      case False then show ?thesis by auto
    1.68 @@ -561,7 +561,7 @@
    1.69  lemma singleton_sup:
    1.70    "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
    1.71      else if B = \<bottom> then singleton dfault A
    1.72 -    else if singleton dfault A = singleton dfault B then singleton dfault A else dfault)"
    1.73 +    else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())"
    1.74  using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
    1.75  
    1.76  
    1.77 @@ -743,12 +743,12 @@
    1.78    "is_empty (Seq f) \<longleftrightarrow> null (f ())"
    1.79    by (simp add: null_is_empty Seq_def)
    1.80  
    1.81 -primrec the_only :: "'a \<Rightarrow> 'a seq \<Rightarrow> 'a" where
    1.82 -  [code del]: "the_only dfault Empty = dfault"
    1.83 -  | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault)"
    1.84 +primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
    1.85 +  [code del]: "the_only dfault Empty = dfault ()"
    1.86 +  | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
    1.87    | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
    1.88         else let x = singleton dfault P; y = the_only dfault xq in
    1.89 -       if x = y then x else dfault)"
    1.90 +       if x = y then x else dfault ())"
    1.91  
    1.92  lemma the_only_singleton:
    1.93    "the_only dfault xq = singleton dfault (pred_of_seq xq)"
    1.94 @@ -758,24 +758,28 @@
    1.95  
    1.96  lemma singleton_code [code]:
    1.97    "singleton dfault (Seq f) = (case f ()
    1.98 -   of Empty \<Rightarrow> dfault
    1.99 +   of Empty \<Rightarrow> dfault ()
   1.100      | Insert x P \<Rightarrow> if is_empty P then x
   1.101          else let y = singleton dfault P in
   1.102 -          if x = y then x else dfault
   1.103 +          if x = y then x else dfault ()
   1.104      | Join P xq \<Rightarrow> if is_empty P then the_only dfault xq
   1.105          else if null xq then singleton dfault P
   1.106          else let x = singleton dfault P; y = the_only dfault xq in
   1.107 -          if x = y then x else dfault)"
   1.108 +          if x = y then x else dfault ())"
   1.109    by (cases "f ()")
   1.110     (auto simp add: Seq_def the_only_singleton is_empty_def
   1.111        null_is_empty singleton_bot singleton_single singleton_sup Let_def)
   1.112  
   1.113  definition not_unique :: "'a pred => 'a"
   1.114  where
   1.115 -  "not_unique A = (THE x. eval A x)"
   1.116 +  [code del]: "not_unique A = (THE x. eval A x)"
   1.117  
   1.118 -lemma The_eq_singleton: "(THE x. eval A x) = singleton (not_unique A) A"
   1.119 -by (auto simp add: singleton_def not_unique_def)
   1.120 +definition the :: "'a pred => 'a"
   1.121 +where
   1.122 +  [code del]: "the A = (THE x. eval A x)"
   1.123 +
   1.124 +lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
   1.125 +by (auto simp add: the_def singleton_def not_unique_def)
   1.126  
   1.127  ML {*
   1.128  signature PREDICATE =
   1.129 @@ -857,6 +861,6 @@
   1.130  
   1.131  hide (open) type pred seq
   1.132  hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
   1.133 -  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
   1.134 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
   1.135  
   1.136  end