src/HOL/Predicate.thy
changeset 33110 16f2814653ed
parent 33104 560372b461e5
child 33111 db5af7b86a2f
     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,49 +471,49 @@
     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 pred \<Rightarrow> 'a" where
     1.8 -  "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)"
     1.9 +definition singleton :: "'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 A = x"
    1.14 +  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x"
    1.15    by (auto simp add: singleton_def)
    1.16  
    1.17  lemma eval_singletonI:
    1.18 -  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)"
    1.19 +  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
    1.20  proof -
    1.21    assume assm: "\<exists>!x. eval A x"
    1.22    then obtain x where "eval A x" ..
    1.23 -  moreover with assm have "singleton A = x" by (rule singleton_eqI)
    1.24 +  moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
    1.25    ultimately show ?thesis by simp 
    1.26  qed
    1.27  
    1.28  lemma single_singleton:
    1.29 -  "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A"
    1.30 +  "\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A"
    1.31  proof -
    1.32    assume assm: "\<exists>!x. eval A x"
    1.33 -  then have "eval A (singleton A)"
    1.34 +  then have "eval A (singleton dfault A)"
    1.35      by (rule eval_singletonI)
    1.36 -  moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x"
    1.37 +  moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
    1.38      by (rule singleton_eqI)
    1.39 -  ultimately have "eval (single (singleton A)) = eval A"
    1.40 +  ultimately have "eval (single (singleton dfault A)) = eval A"
    1.41      by (simp (no_asm_use) add: single_def expand_fun_eq) blast
    1.42    then show ?thesis by (simp add: eval_inject)
    1.43  qed
    1.44  
    1.45  lemma singleton_undefinedI:
    1.46 -  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined"
    1.47 +  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault"
    1.48    by (simp add: singleton_def)
    1.49  
    1.50  lemma singleton_bot:
    1.51 -  "singleton \<bottom> = undefined"
    1.52 +  "singleton dfault \<bottom> = dfault"
    1.53    by (auto simp add: bot_pred_def intro: singleton_undefinedI)
    1.54  
    1.55  lemma singleton_single:
    1.56 -  "singleton (single x) = x"
    1.57 +  "singleton dfault (single x) = x"
    1.58    by (auto simp add: intro: singleton_eqI singleI elim: singleE)
    1.59  
    1.60  lemma singleton_sup_single_single:
    1.61 -  "singleton (single x \<squnion> single y) = (if x = y then x else undefined)"
    1.62 +  "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault)"
    1.63  proof (cases "x = y")
    1.64    case True then show ?thesis by (simp add: singleton_single)
    1.65  next
    1.66 @@ -523,25 +523,25 @@
    1.67    by (auto intro: supI1 supI2 singleI)
    1.68    with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
    1.69      by blast
    1.70 -  then have "singleton (single x \<squnion> single y) = undefined"
    1.71 +  then have "singleton dfault (single x \<squnion> single y) = dfault"
    1.72      by (rule singleton_undefinedI)
    1.73    with False show ?thesis by simp
    1.74  qed
    1.75  
    1.76  lemma singleton_sup_aux:
    1.77 -  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
    1.78 -    else if B = \<bottom> then singleton A
    1.79 -    else singleton
    1.80 -      (single (singleton A) \<squnion> single (singleton B)))"
    1.81 +  "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
    1.82 +    else if B = \<bottom> then singleton dfault A
    1.83 +    else singleton dfault
    1.84 +      (single (singleton dfault A) \<squnion> single (singleton dfault B)))"
    1.85  proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
    1.86    case True then show ?thesis by (simp add: single_singleton)
    1.87  next
    1.88    case False
    1.89    from False have A_or_B:
    1.90 -    "singleton A = undefined \<or> singleton B = undefined"
    1.91 +    "singleton dfault A = dfault \<or> singleton dfault B = dfault"
    1.92      by (auto intro!: singleton_undefinedI)
    1.93 -  then have rhs: "singleton
    1.94 -    (single (singleton A) \<squnion> single (singleton B)) = undefined"
    1.95 +  then have rhs: "singleton dfault
    1.96 +    (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault"
    1.97      by (auto simp add: singleton_sup_single_single singleton_single)
    1.98    from False have not_unique:
    1.99      "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
   1.100 @@ -551,7 +551,7 @@
   1.101        by (blast elim: not_bot)
   1.102      with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
   1.103        by (auto simp add: sup_pred_def bot_pred_def)
   1.104 -    then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI)
   1.105 +    then have "singleton dfault (A \<squnion> B) = dfault" by (rule singleton_undefinedI)
   1.106      with True rhs show ?thesis by simp
   1.107    next
   1.108      case False then show ?thesis by auto
   1.109 @@ -559,10 +559,10 @@
   1.110  qed
   1.111  
   1.112  lemma singleton_sup:
   1.113 -  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
   1.114 -    else if B = \<bottom> then singleton A
   1.115 -    else if singleton A = singleton B then singleton A else undefined)"
   1.116 -using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single)
   1.117 +  "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
   1.118 +    else if B = \<bottom> then singleton dfault A
   1.119 +    else if singleton dfault A = singleton dfault B then singleton dfault A else dfault)"
   1.120 +using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
   1.121  
   1.122  
   1.123  subsubsection {* Derived operations *}
   1.124 @@ -743,33 +743,40 @@
   1.125    "is_empty (Seq f) \<longleftrightarrow> null (f ())"
   1.126    by (simp add: null_is_empty Seq_def)
   1.127  
   1.128 -primrec the_only :: "'a seq \<Rightarrow> 'a" where
   1.129 -  [code del]: "the_only Empty = undefined"
   1.130 -  | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)"
   1.131 -  | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P
   1.132 -       else let x = singleton P; y = the_only xq in
   1.133 -       if x = y then x else undefined)"
   1.134 +primrec the_only :: "'a \<Rightarrow> 'a seq \<Rightarrow> 'a" where
   1.135 +  [code del]: "the_only dfault Empty = dfault"
   1.136 +  | "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.137 +  | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
   1.138 +       else let x = singleton dfault P; y = the_only dfault xq in
   1.139 +       if x = y then x else dfault)"
   1.140  
   1.141  lemma the_only_singleton:
   1.142 -  "the_only xq = singleton (pred_of_seq xq)"
   1.143 +  "the_only dfault xq = singleton dfault (pred_of_seq xq)"
   1.144    by (induct xq)
   1.145      (auto simp add: singleton_bot singleton_single is_empty_def
   1.146      null_is_empty Let_def singleton_sup)
   1.147  
   1.148  lemma singleton_code [code]:
   1.149 -  "singleton (Seq f) = (case f ()
   1.150 -   of Empty \<Rightarrow> undefined
   1.151 +  "singleton dfault (Seq f) = (case f ()
   1.152 +   of Empty \<Rightarrow> dfault
   1.153      | Insert x P \<Rightarrow> if is_empty P then x
   1.154 -        else let y = singleton P in
   1.155 -          if x = y then x else undefined
   1.156 -    | Join P xq \<Rightarrow> if is_empty P then the_only xq
   1.157 -        else if null xq then singleton P
   1.158 -        else let x = singleton P; y = the_only xq in
   1.159 -          if x = y then x else undefined)"
   1.160 +        else let y = singleton dfault P in
   1.161 +          if x = y then x else dfault
   1.162 +    | Join P xq \<Rightarrow> if is_empty P then the_only dfault xq
   1.163 +        else if null xq then singleton dfault P
   1.164 +        else let x = singleton dfault P; y = the_only dfault xq in
   1.165 +          if x = y then x else dfault)"
   1.166    by (cases "f ()")
   1.167     (auto simp add: Seq_def the_only_singleton is_empty_def
   1.168        null_is_empty singleton_bot singleton_single singleton_sup Let_def)
   1.169  
   1.170 +definition not_unique :: "'a pred => 'a"
   1.171 +where
   1.172 +  "not_unique A = (THE x. eval A x)"
   1.173 +
   1.174 +lemma The_eq_singleton: "(THE x. eval A x) = singleton (not_unique A) A"
   1.175 +by (auto simp add: singleton_def not_unique_def)
   1.176 +
   1.177  ML {*
   1.178  signature PREDICATE =
   1.179  sig
   1.180 @@ -815,6 +822,8 @@
   1.181  code_const Seq and Empty and Insert and Join
   1.182    (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
   1.183  
   1.184 +code_abort not_unique
   1.185 +
   1.186  text {* dummy setup for @{text code_pred} and @{text values} keywords *}
   1.187  
   1.188  ML {*