# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1589448393 -3600
# Node ID 0bbe0866b7e6f0e94bf0fdacf44e3d123a2dcb50
# Parent  5656ec95493cd94278f8652a3fbb70d3c3554a5d
The Uniq quantifier for FOL too

diff -r 5656ec95493c -r 0bbe0866b7e6 NEWS
--- a/NEWS	Wed May 13 13:00:03 2020 +0200
+++ b/NEWS	Thu May 14 10:26:33 2020 +0100
@@ -42,6 +42,10 @@
 
 * For the natural numbers, Sup{} = 0.
 
+*** FOL ***
+
+* Added the "at most 1" quantifier, Uniq, as in HOL.
+
 New in Isabelle2020 (April 2020)
 --------------------------------
 
diff -r 5656ec95493c -r 0bbe0866b7e6 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed May 13 13:00:03 2020 +0200
+++ b/src/FOL/IFOL.thy	Thu May 14 10:26:33 2020 +0100
@@ -5,7 +5,9 @@
 section \<open>Intuitionistic first-order logic\<close>
 
 theory IFOL
-imports Pure
+  imports Pure
+abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
+
 begin
 
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
@@ -87,6 +89,9 @@
 definition iff  (infixr \<open>\<longleftrightarrow>\<close> 25)
   where \<open>P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)\<close>
 
+definition Uniq :: "('a \<Rightarrow> o) \<Rightarrow> o"
+  where \<open>Uniq(P) \<equiv> (\<forall>x y. P(x) \<longrightarrow> P(y) \<longrightarrow> y = x)\<close>
+
 definition Ex1 :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close>  (binder \<open>\<exists>!\<close> 10)
   where ex1_def: \<open>\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)\<close>
 
@@ -97,6 +102,13 @@
 abbreviation not_equal :: \<open>['a, 'a] \<Rightarrow> o\<close>  (infixl \<open>\<noteq>\<close> 50)
   where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
 
+syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
+
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
 
 subsubsection \<open>Old-style ASCII syntax\<close>
 
@@ -126,38 +138,42 @@
   assumes major: \<open>P \<and> Q\<close>
     and r: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (rule r)
-   apply (rule major [THEN conjunct1])
-  apply (rule major [THEN conjunct2])
-  done
+proof (rule r)
+  show "P"
+    by (rule major [THEN conjunct1])
+  show "Q"
+    by (rule major [THEN conjunct2])
+qed
 
 lemma impE:
   assumes major: \<open>P \<longrightarrow> Q\<close>
     and \<open>P\<close>
   and r: \<open>Q \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (rule r)
-  apply (rule major [THEN mp])
-  apply (rule \<open>P\<close>)
-  done
+proof (rule r)
+  show "Q"
+    by (rule mp [OF major \<open>P\<close>])
+qed
 
 lemma allE:
   assumes major: \<open>\<forall>x. P(x)\<close>
     and r: \<open>P(x) \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (rule r)
-  apply (rule major [THEN spec])
-  done
+proof (rule r)
+  show "P(x)"
+    by (rule major [THEN spec])
+qed
 
 text \<open>Duplicates the quantifier; for use with \<^ML>\<open>eresolve_tac\<close>.\<close>
 lemma all_dupE:
   assumes major: \<open>\<forall>x. P(x)\<close>
     and r: \<open>\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (rule r)
-   apply (rule major [THEN spec])
-  apply (rule major)
-  done
+proof (rule r)
+  show "P(x)"
+    by (rule major [THEN spec])
+qed (rule major)
+
 
 
 subsubsection \<open>Negation rules, which translate between \<open>\<not> P\<close> and \<open>P \<longrightarrow> False\<close>\<close>
@@ -215,18 +231,16 @@
 subsection \<open>If-and-only-if\<close>
 
 lemma iffI: \<open>\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q\<close>
-  apply (unfold iff_def)
-  apply (rule conjI)
-   apply (erule impI)
-  apply (erule impI)
-  done
+  unfolding iff_def
+  by (rule conjI; erule impI)
 
 lemma iffE:
   assumes major: \<open>P \<longleftrightarrow> Q\<close>
-    and r: \<open>P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> R\<close>
+    and r: \<open>\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (insert major, unfold iff_def)
-  apply (erule conjE)
+  using major
+  unfolding iff_def
+  apply (rule conjE)
   apply (erule r)
   apply assumption
   done
@@ -235,13 +249,13 @@
 subsubsection \<open>Destruct rules for \<open>\<longleftrightarrow>\<close> similar to Modus Ponens\<close>
 
 lemma iffD1: \<open>\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q\<close>
-  apply (unfold iff_def)
+  unfolding iff_def
   apply (erule conjunct1 [THEN mp])
   apply assumption
   done
 
 lemma iffD2: \<open>\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P\<close>
-  apply (unfold iff_def)
+  unfolding iff_def
   apply (erule conjunct2 [THEN mp])
   apply assumption
   done
@@ -283,7 +297,7 @@
 \<close>
 
 lemma ex1I: \<open>P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)\<close>
-  apply (unfold ex1_def)
+  unfolding ex1_def
   apply (assumption | rule exI conjI allI impI)+
   done
 
@@ -296,7 +310,7 @@
   done
 
 lemma ex1E: \<open>\<exists>! x. P(x) \<Longrightarrow> (\<And>x. \<lbrakk>P(x); \<forall>y. P(y) \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R\<close>
-  apply (unfold ex1_def)
+  unfolding ex1_def
   apply (assumption | erule exE conjE)+
   done
 
@@ -424,77 +438,6 @@
   done
 
 
-subsubsection \<open>Polymorphic congruence rules\<close>
-
-lemma subst_context: \<open>a = b \<Longrightarrow> t(a) = t(b)\<close>
-  apply (erule ssubst)
-  apply (rule refl)
-  done
-
-lemma subst_context2: \<open>\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)\<close>
-  apply (erule ssubst)+
-  apply (rule refl)
-  done
-
-lemma subst_context3: \<open>\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)\<close>
-  apply (erule ssubst)+
-  apply (rule refl)
-  done
-
-text \<open>
-  Useful with \<^ML>\<open>eresolve_tac\<close> for proving equalities from known
-  equalities.
-
-        a = b
-        |   |
-        c = d
-\<close>
-lemma box_equals: \<open>\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d\<close>
-  apply (rule trans)
-   apply (rule trans)
-    apply (rule sym)
-    apply assumption+
-  done
-
-text \<open>Dual of \<open>box_equals\<close>: for proving equalities backwards.\<close>
-lemma simp_equals: \<open>\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b\<close>
-  apply (rule trans)
-   apply (rule trans)
-    apply assumption+
-  apply (erule sym)
-  done
-
-
-subsubsection \<open>Congruence rules for predicate letters\<close>
-
-lemma pred1_cong: \<open>a = a' \<Longrightarrow> P(a) \<longleftrightarrow> P(a')\<close>
-  apply (rule iffI)
-   apply (erule (1) subst)
-  apply (erule (1) ssubst)
-  done
-
-lemma pred2_cong: \<open>\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> P(a,b) \<longleftrightarrow> P(a',b')\<close>
-  apply (rule iffI)
-   apply (erule subst)+
-   apply assumption
-  apply (erule ssubst)+
-  apply assumption
-  done
-
-lemma pred3_cong: \<open>\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> P(a,b,c) \<longleftrightarrow> P(a',b',c')\<close>
-  apply (rule iffI)
-   apply (erule subst)+
-   apply assumption
-  apply (erule ssubst)+
-  apply assumption
-  done
-
-text \<open>Special case for the equality predicate!\<close>
-lemma eq_cong: \<open>\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> a = b \<longleftrightarrow> a' = b'\<close>
-  apply (erule (1) pred2_cong)
-  done
-
-
 subsection \<open>Simplifications of assumed implications\<close>
 
 text \<open>
@@ -531,9 +474,7 @@
   Still UNSAFE since ~P must be provable -- backtracking needed.\<close>
 lemma not_impE: \<open>\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R\<close>
   apply (drule mp)
-   apply (rule notI)
-   apply assumption
-  apply assumption
+   apply (rule notI | assumption)+
   done
 
 text \<open>Simplifies the implication. UNSAFE.\<close>
@@ -543,8 +484,7 @@
     and r2: \<open>\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P\<close>
     and r3: \<open>S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
-  done
+  by (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
 
 text \<open>What if \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close> is an assumption?
   UNSAFE.\<close>
@@ -553,8 +493,7 @@
     and r1: \<open>\<And>x. P(x)\<close>
     and r2: \<open>S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (rule allI impI major [THEN mp] r1 r2)+
-  done
+  by (rule allI impI major [THEN mp] r1 r2)+
 
 text \<open>
   Unsafe: \<open>\<exists>x. P(x)) \<longrightarrow> S\<close> is equivalent
@@ -563,8 +502,7 @@
   assumes major: \<open>(\<exists>x. P(x)) \<longrightarrow> S\<close>
     and r: \<open>P(x) \<longrightarrow> S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
-  apply (assumption | rule exI impI major [THEN mp] r)+
-  done
+  by (assumption | rule exI impI major [THEN mp] r)+
 
 text \<open>Courtesy of Krzysztof Grabczewski.\<close>
 lemma disj_imp_disj: \<open>P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S\<close>
@@ -658,9 +596,50 @@
 
 
 lemma eq_commute: \<open>a = b \<longleftrightarrow> b = a\<close>
-  apply (rule iffI)
-  apply (erule sym)+
-  done
+  by iprover
+
+
+subsection \<open>Polymorphic congruence rules\<close>
+
+lemma subst_context: \<open>a = b \<Longrightarrow> t(a) = t(b)\<close>
+  by iprover
+
+lemma subst_context2: \<open>\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)\<close>
+  by iprover
+
+lemma subst_context3: \<open>\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)\<close>
+  by iprover
+
+text \<open>
+  Useful with \<^ML>\<open>eresolve_tac\<close> for proving equalities from known
+  equalities.
+
+        a = b
+        |   |
+        c = d
+\<close>
+lemma box_equals: \<open>\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d\<close>
+  by iprover
+
+text \<open>Dual of \<open>box_equals\<close>: for proving equalities backwards.\<close>
+lemma simp_equals: \<open>\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b\<close>
+  by iprover
+
+
+subsubsection \<open>Congruence rules for predicate letters\<close>
+
+lemma pred1_cong: \<open>a = a' \<Longrightarrow> P(a) \<longleftrightarrow> P(a')\<close>
+  by iprover
+
+lemma pred2_cong: \<open>\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> P(a,b) \<longleftrightarrow> P(a',b')\<close>
+  by iprover
+
+lemma pred3_cong: \<open>\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> P(a,b,c) \<longleftrightarrow> P(a',b',c')\<close>
+  by iprover
+
+text \<open>Special case for the equality predicate!\<close>
+lemma eq_cong: \<open>\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> a = b \<longleftrightarrow> a' = b'\<close>
+  by iprover
 
 
 subsection \<open>Atomizing meta-level rules\<close>
@@ -776,7 +755,7 @@
 lemma LetI:
   assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close>
   shows \<open>P(let x = t in u(x))\<close>
-  apply (unfold Let_def)
+  unfolding Let_def
   apply (rule refl [THEN assms])
   done