# HG changeset patch
# User wenzelm
# Date 1594652925 -7200
# Node ID 83456d9f0ed5a16a9fd3d37917ce8763b48fe519
# Parent  759532ef0885b637a62ce9718faa417e21a8a1d1
clarified examples;

diff -r 759532ef0885 -r 83456d9f0ed5 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/Doc/Implementation/Integration.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -131,7 +131,7 @@
 \<close>
 
 text %mlex \<open>
-  The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command
+  The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command
   definitions, with the all-important theory header declarations for outer
   syntax keywords.
 \<close>
diff -r 759532ef0885 -r 83456d9f0ed5 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -543,7 +543,7 @@
   \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
   from well-founded induction and completeness of patterns. This factors out
   some operations that are done internally by the function package and makes
-  them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
+  them available separately. See \<^file>\<open>~~/src/HOL/Examples/Induction_Schema.thy\<close> for
   examples.
 \<close>
 
@@ -662,7 +662,7 @@
   Adhoc overloading allows to overload a constant depending on its type.
   Typically this involves the introduction of an uninterpreted constant (used
   for input and output) and the addition of some variants (used internally).
-  For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
+  For examples see \<^file>\<open>~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy\<close> and
   \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
 
   \<^rail>\<open>
@@ -1010,7 +1010,7 @@
 
 subsubsection \<open>Examples\<close>
 
-text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
+text \<open>See \<^file>\<open>~~/src/HOL/Examples/Records.thy\<close>, for example.\<close>
 
 
 section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
@@ -2150,7 +2150,7 @@
 (*<*)end(*>*)
 
 text \<open>
-  See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
+  See also \<^file>\<open>~~/src/HOL/Examples/Groebner_Examples.thy\<close>.
 \<close>
 
 
@@ -2167,7 +2167,7 @@
 
   \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
   "Bezem-Coquand:2005"}, which covers applications in confluence theory,
-  lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
+  lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/Examples/Coherent.thy\<close>
   for some examples.
 \<close>
 
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -15,7 +15,7 @@
   "HOL-Computational_Algebra.Computational_Algebra"
   "HOL-Computational_Algebra.Polynomial_Factorial"
   "HOL-Number_Theory.Eratosthenes"
-  "HOL-ex.Records"
+  "HOL-Examples.Records"
   "HOL-Word.Word"
 begin
 
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Examples/Ackermann.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -1,3 +1,7 @@
+(*  Title:      HOL/Examples/Ackermann.thy
+    Author:     Larry Paulson
+*)
+
 section \<open>A Tail-Recursive, Stack-Based Ackermann's Function\<close>
 
 theory Ackermann imports Main
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Adhoc_Overloading_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Adhoc_Overloading_Examples.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -0,0 +1,256 @@
+(*  Title:      HOL/Examples/Adhoc_Overloading_Examples.thy
+    Author:     Christian Sternagel
+*)
+
+section \<open>Ad Hoc Overloading\<close>
+
+theory Adhoc_Overloading_Examples
+imports
+  Main
+  "HOL-Library.Infinite_Set"
+  "HOL-Library.Adhoc_Overloading"
+begin
+
+text \<open>Adhoc overloading allows to overload a constant depending on
+its type. Typically this involves to introduce an uninterpreted
+constant (used for input and output) and then add some variants (used
+internally).\<close>
+
+subsection \<open>Plain Ad Hoc Overloading\<close>
+
+text \<open>Consider the type of first-order terms.\<close>
+datatype ('a, 'b) "term" =
+  Var 'b |
+  Fun 'a "('a, 'b) term list"
+
+text \<open>The set of variables of a term might be computed as follows.\<close>
+fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
+  "term_vars (Var x) = {x}" |
+  "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
+
+text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
+rewrite systems (i.e., sets of rules), the set of variables makes
+sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
+
+consts vars :: "'a \<Rightarrow> 'b set"
+
+text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
+adhoc_overloading
+  vars term_vars
+
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
+
+fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
+  "rule_vars (l, r) = vars l \<union> vars r"
+
+adhoc_overloading
+  vars rule_vars
+
+value [nbe] "vars (Var 1, Var 0)"
+
+definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
+  "trs_vars R = \<Union>(rule_vars ` R)"
+
+adhoc_overloading
+  vars trs_vars
+
+value [nbe] "vars {(Var 1, Var 0)}"
+
+text \<open>Sometimes it is necessary to add explicit type constraints
+before a variant can be determined.\<close>
+(*value "vars R" (*has multiple instances*)*)
+value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
+
+text \<open>It is also possible to remove variants.\<close>
+no_adhoc_overloading
+  vars term_vars rule_vars 
+
+(*value "vars (Var 1)" (*does not have an instance*)*)
+
+text \<open>As stated earlier, the overloaded constant is only used for
+input and output. Internally, always a variant is used, as can be
+observed by the configuration option \<open>show_variants\<close>.\<close>
+
+adhoc_overloading
+  vars term_vars
+
+declare [[show_variants]]
+
+term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
+
+
+subsection \<open>Adhoc Overloading inside Locales\<close>
+
+text \<open>As example we use permutations that are parametrized over an
+atom type \<^typ>\<open>'a\<close>.\<close>
+
+definition perms :: "('a \<Rightarrow> 'a) set" where
+  "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
+
+typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
+  by standard (auto simp: perms_def)
+
+text \<open>First we need some auxiliary lemmas.\<close>
+lemma permsI [Pure.intro]:
+  assumes "bij f" and "MOST x. f x = x"
+  shows "f \<in> perms"
+  using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
+
+lemma perms_imp_bij:
+  "f \<in> perms \<Longrightarrow> bij f"
+  by (simp add: perms_def)
+
+lemma perms_imp_MOST_eq:
+  "f \<in> perms \<Longrightarrow> MOST x. f x = x"
+  by (simp add: perms_def) (metis MOST_iff_finiteNeg)
+
+lemma id_perms [simp]:
+  "id \<in> perms"
+  "(\<lambda>x. x) \<in> perms"
+  by (auto simp: perms_def bij_def)
+
+lemma perms_comp [simp]:
+  assumes f: "f \<in> perms" and g: "g \<in> perms"
+  shows "(f \<circ> g) \<in> perms"
+  apply (intro permsI bij_comp)
+  apply (rule perms_imp_bij [OF g])
+  apply (rule perms_imp_bij [OF f])
+  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
+  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
+  by simp
+
+lemma perms_inv:
+  assumes f: "f \<in> perms"
+  shows "inv f \<in> perms"
+  apply (rule permsI)
+  apply (rule bij_imp_bij_inv)
+  apply (rule perms_imp_bij [OF f])
+  apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
+  apply (erule subst, rule inv_f_f)
+  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
+  done
+
+lemma bij_Rep_perm: "bij (Rep_perm p)"
+  using Rep_perm [of p] unfolding perms_def by simp
+
+instantiation perm :: (type) group_add
+begin
+
+definition "0 = Abs_perm id"
+definition "- p = Abs_perm (inv (Rep_perm p))"
+definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
+definition "(p1::'a perm) - p2 = p1 + - p2"
+
+lemma Rep_perm_0: "Rep_perm 0 = id"
+  unfolding zero_perm_def by (simp add: Abs_perm_inverse)
+
+lemma Rep_perm_add:
+  "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"
+  unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
+
+lemma Rep_perm_uminus:
+  "Rep_perm (- p) = inv (Rep_perm p)"
+  unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
+
+instance
+  apply standard
+  unfolding Rep_perm_inject [symmetric]
+  unfolding minus_perm_def
+  unfolding Rep_perm_add
+  unfolding Rep_perm_uminus
+  unfolding Rep_perm_0
+  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+  done
+
+end
+
+lemmas Rep_perm_simps =
+  Rep_perm_0
+  Rep_perm_add
+  Rep_perm_uminus
+
+
+section \<open>Permutation Types\<close>
+
+text \<open>We want to be able to apply permutations to arbitrary types. To
+this end we introduce a constant \<open>PERMUTE\<close> together with
+convenient infix syntax.\<close>
+
+consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
+
+text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
+appliciation of permutations.\<close>
+locale permute =
+  fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
+  assumes permute_zero [simp]: "permute 0 x = x"
+    and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
+begin
+
+adhoc_overloading
+  PERMUTE permute
+
+end
+
+text \<open>Permuting atoms.\<close>
+definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "permute_atom p a = (Rep_perm p) a"
+
+adhoc_overloading
+  PERMUTE permute_atom
+
+interpretation atom_permute: permute permute_atom
+  by standard (simp_all add: permute_atom_def Rep_perm_simps)
+
+text \<open>Permuting permutations.\<close>
+definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
+  "permute_perm p q = p + q - p"
+
+adhoc_overloading
+  PERMUTE permute_perm
+
+interpretation perm_permute: permute permute_perm
+  apply standard
+  unfolding permute_perm_def
+  apply simp
+  apply (simp only: diff_conv_add_uminus minus_add add.assoc)
+  done
+
+text \<open>Permuting functions.\<close>
+locale fun_permute =
+  dom: permute perm1 + ran: permute perm2
+  for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
+  and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
+begin
+
+adhoc_overloading
+  PERMUTE perm1 perm2
+
+definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
+  "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
+
+adhoc_overloading
+  PERMUTE permute_fun
+
+end
+
+sublocale fun_permute \<subseteq> permute permute_fun
+  by (unfold_locales, auto simp: permute_fun_def)
+     (metis dom.permute_plus minus_add)
+
+lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0"
+  unfolding permute_atom_def
+  by (metis Rep_perm_0 id_apply zero_perm_def)
+
+interpretation atom_fun_permute: fun_permute permute_atom permute_atom
+  by (unfold_locales)
+
+adhoc_overloading
+  PERMUTE atom_fun_permute.permute_fun
+
+lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
+  unfolding atom_fun_permute.permute_fun_def
+  unfolding permute_atom_def
+  by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)
+
+end
+
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Coherent.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Coherent.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -0,0 +1,95 @@
+(*  Title:      HOL/Examples/Coherent.thy
+    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
+*)
+
+section \<open>Coherent Logic Problems\<close>
+
+theory Coherent
+imports Main
+begin
+
+subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
+
+no_notation
+  comp (infixl "o" 55) and
+  relcomp (infixr "O" 75)
+
+lemma p1p2:
+  assumes "col a b c l \<and> col d e f m"
+    and "col b f g n \<and> col c e g o"
+    and "col b d h p \<and> col a e h q"
+    and "col c d i r \<and> col a f i s"
+    and "el n o \<Longrightarrow> goal"
+    and "el p q \<Longrightarrow> goal"
+    and "el s r \<Longrightarrow> goal"
+    and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+    and "\<And>A B. pl A B \<Longrightarrow> el B B"
+    and "\<And>A B. el A B \<Longrightarrow> el B A"
+    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+    and "\<And>A B C D E F G H I J K L M N O P Q.
+           col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
+           col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
+           (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
+    and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
+    and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+  shows goal using assms
+  by coherent
+
+lemma p2p1:
+  assumes "col a b c l \<and> col d e f m"
+    and "col b f g n \<and> col c e g o"
+    and "col b d h p \<and> col a e h q"
+    and "col c d i r \<and> col a f i s"
+    and "pl a m \<Longrightarrow> goal"
+    and "pl b m \<Longrightarrow> goal"
+    and "pl c m \<Longrightarrow> goal"
+    and "pl d l \<Longrightarrow> goal"
+    and "pl e l \<Longrightarrow> goal"
+    and "pl f l \<Longrightarrow> goal"
+    and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+    and "\<And>A B. pl A B \<Longrightarrow> el B B"
+    and "\<And>A B. el A B \<Longrightarrow> el B A"
+    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+    and "\<And>A B C D E F G H I J K L M N O P Q.
+           col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
+           col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
+           (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
+    and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
+    and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+  shows goal using assms
+  by coherent
+
+
+subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
+
+lemma diamond:
+  assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
+    and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
+    and "\<And>A. equalish A A" 
+    and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
+    and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
+    and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
+    and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
+    and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
+    and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
+  shows goal using assms
+  by coherent
+
+end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Commands.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Commands.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -0,0 +1,77 @@
+(*  Title:      HOL/Examples/Commands.thy
+    Author:     Makarius
+*)
+
+section \<open>Some Isar command definitions\<close>
+
+theory Commands
+imports Main
+keywords
+  "print_test" :: diag and
+  "global_test" :: thy_decl and
+  "local_test" :: thy_decl
+begin
+
+subsection \<open>Diagnostic command: no state change\<close>
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>print_test\<close> "print term test"
+    (Parse.term >> (fn s => Toplevel.keep (fn st =>
+      let
+        val ctxt = Toplevel.context_of st;
+        val t = Syntax.read_term ctxt s;
+        val ctxt' = Proof_Context.augment t ctxt;
+      in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
+\<close>
+
+print_test x
+print_test "\<lambda>x. x = a"
+
+
+subsection \<open>Old-style global theory declaration\<close>
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>global_test\<close> "test constant declaration"
+    (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
+      let
+        val thy' = Sign.add_consts [(b, \<^typ>\<open>'a\<close>, NoSyn)] thy;
+      in thy' end)));
+\<close>
+
+global_test a
+global_test b
+print_test a
+
+
+subsection \<open>Local theory specification\<close>
+
+ML \<open>
+  Outer_Syntax.local_theory \<^command_keyword>\<open>local_test\<close> "test local definition"
+    (Parse.binding -- (\<^keyword>\<open>=\<close> |-- Parse.term) >> (fn (b, s) => fn lthy =>
+      let
+        val t = Syntax.read_term lthy s;
+        val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
+      in lthy' end));
+\<close>
+
+local_test true = True
+print_test true
+thm true_def
+
+local_test identity = "\<lambda>x. x"
+print_test "identity x"
+thm identity_def
+
+context fixes x y :: nat
+begin
+
+local_test test = "x + y"
+print_test test
+thm test_def
+
+end
+
+print_test "test 0 1"
+thm test_def
+
+end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Groebner_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Groebner_Examples.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -0,0 +1,116 @@
+(*  Title:      HOL/Examples/Groebner_Examples.thy
+    Author:     Amine Chaieb, TU Muenchen
+*)
+
+section \<open>Groebner Basis Examples\<close>
+
+theory Groebner_Examples
+imports Main
+begin
+
+subsection \<open>Basic examples\<close>
+
+lemma
+  fixes x :: int
+  shows "x ^ 3 = x ^ 3"
+  apply (tactic \<open>ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
+  by (rule refl)
+
+lemma
+  fixes x :: int
+  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<^sup>2 + (80 * x + 32))))" 
+  apply (tactic \<open>ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
+  by (rule refl)
+
+schematic_goal
+  fixes x :: int
+  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
+  apply (tactic \<open>ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
+  by (rule refl)
+
+lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
+  apply (simp only: power_Suc power_0)
+  apply (simp only: semiring_norm)
+  oops
+
+lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
+  by algebra
+
+lemma "(4::nat) + 4 = 3 + 5"
+  by algebra
+
+lemma "(4::int) + 0 = 4"
+  apply algebra?
+  by simp
+
+lemma
+  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
+  shows "d\<^sup>2 * c\<^sup>2 - 2 * d * c * a * f + a\<^sup>2 * f\<^sup>2 - e * d * b * c - e * b * a * f +
+    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
+  using assms by algebra
+
+lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
+  by algebra
+
+theorem "x* (x\<^sup>2 - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
+  by algebra
+
+lemma
+  fixes x::"'a::idom"
+  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
+  by algebra
+
+subsection \<open>Lemmas for Lagrange's theorem\<close>
+
+definition
+  sq :: "'a::times => 'a" where
+  "sq x == x*x"
+
+lemma
+  fixes x1 :: "'a::{idom}"
+  shows
+  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
+    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
+    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
+    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
+    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
+  by (algebra add: sq_def)
+
+lemma
+  fixes p1 :: "'a::{idom}"
+  shows
+  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
+   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
+    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
+      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
+      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
+      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
+      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
+      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
+      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
+      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
+  by (algebra add: sq_def)
+
+
+subsection \<open>Colinearity is invariant by rotation\<close>
+
+type_synonym point = "int \<times> int"
+
+definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
+  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
+    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
+
+lemma collinear_inv_rotation:
+  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
+  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
+    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
+  using assms 
+  by (algebra add: collinear_def split_def fst_conv snd_conv)
+
+lemma "\<exists>(d::int). a*y - a*x = n*d \<Longrightarrow> \<exists>u v. a*u + n*v = 1 \<Longrightarrow> \<exists>e. y - x = n*e"
+  by algebra
+
+end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Iff_Oracle.thy
--- a/src/HOL/Examples/Iff_Oracle.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Examples/Iff_Oracle.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Example/Iff_Oracle.thy
+(*  Title:      HOL/Examples/Iff_Oracle.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Makarius
 *)
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Induction_Schema.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Induction_Schema.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -0,0 +1,48 @@
+(*  Title:      HOL/Examples/Induction_Schema.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+section \<open>Examples of automatically derived induction rules\<close>
+
+theory Induction_Schema
+imports Main
+begin
+
+subsection \<open>Some simple induction principles on nat\<close>
+
+lemma nat_standard_induct: (* cf. Nat.thy *)
+  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma nat_induct2:
+  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
+  \<Longrightarrow> P n"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma minus_one_induct:
+  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
+by induction_schema (pat_completeness, lexicographic_order)
+
+theorem diff_induct: (* cf. Nat.thy *)
+  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
+    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma list_induct2': (* cf. List.thy *)
+  "\<lbrakk> P [] [];
+  \<And>x xs. P (x#xs) [];
+  \<And>y ys. P [] (y#ys);
+   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+by induction_schema (pat_completeness, lexicographic_order)
+
+theorem even_odd_induct:
+  assumes "R 0"
+  assumes "Q 0"
+  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
+  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
+  shows "R n" "Q n"
+  using assms
+by induction_schema (pat_completeness+, lexicographic_order)
+
+end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/Examples/Records.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Records.thy	Mon Jul 13 17:08:45 2020 +0200
@@ -0,0 +1,345 @@
+(*  Title:      HOL/Examples/Records.thy
+    Author:     Wolfgang Naraschewski, TU Muenchen
+    Author:     Norbert Schirmer, TU Muenchen
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+section \<open>Using extensible records in HOL -- points and coloured points\<close>
+
+theory Records
+imports Main
+begin
+
+subsection \<open>Points\<close>
+
+record point =
+  xpos :: nat
+  ypos :: nat
+
+text \<open>
+  Apart many other things, above record declaration produces the
+  following theorems:
+\<close>
+
+
+thm point.simps
+thm point.iffs
+thm point.defs
+
+text \<open>
+  The set of theorems @{thm [source] point.simps} is added
+  automatically to the standard simpset, @{thm [source] point.iffs} is
+  added to the Classical Reasoner and Simplifier context.
+
+  \medskip Record declarations define new types and type abbreviations:
+  @{text [display]
+\<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
+'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type\<close>}
+\<close>
+
+consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
+consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
+
+
+subsubsection \<open>Introducing concrete records and record schemes\<close>
+
+definition foo1 :: point
+  where "foo1 = (| xpos = 1, ypos = 0 |)"
+
+definition foo3 :: "'a => 'a point_scheme"
+  where "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
+
+
+subsubsection \<open>Record selection and record update\<close>
+
+definition getX :: "'a point_scheme => nat"
+  where "getX r = xpos r"
+
+definition setX :: "'a point_scheme => nat => 'a point_scheme"
+  where "setX r n = r (| xpos := n |)"
+
+
+subsubsection \<open>Some lemmas about records\<close>
+
+text \<open>Basic simplifications.\<close>
+
+lemma "point.make n p = (| xpos = n, ypos = p |)"
+  by (simp only: point.make_def)
+
+lemma "xpos (| xpos = m, ypos = n, ... = p |) = m"
+  by simp
+
+lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)"
+  by simp
+
+
+text \<open>\medskip Equality of records.\<close>
+
+lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
+  \<comment> \<open>introduction of concrete record equality\<close>
+  by simp
+
+lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
+  \<comment> \<open>elimination of concrete record equality\<close>
+  by simp
+
+lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
+  \<comment> \<open>introduction of abstract record equality\<close>
+  by simp
+
+lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
+  \<comment> \<open>elimination of abstract record equality (manual proof)\<close>
+proof -
+  assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
+  then have "xpos ?lhs = xpos ?rhs" by simp
+  then show ?thesis by simp
+qed
+
+
+text \<open>\medskip Surjective pairing\<close>
+
+lemma "r = (| xpos = xpos r, ypos = ypos r |)"
+  by simp
+
+lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
+  by simp
+
+
+text \<open>
+  \medskip Representation of records by cases or (degenerate)
+  induction.
+\<close>
+
+lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
+proof (cases r)
+  fix xpos ypos more
+  assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
+  then show ?thesis by simp
+qed
+
+lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
+proof (induct r)
+  fix xpos ypos more
+  show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) =
+      (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)"
+    by simp
+qed
+
+lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
+proof (cases r)
+  fix xpos ypos more
+  assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
+  then show ?thesis by simp
+qed
+
+lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
+proof (cases r)
+  case fields
+  then show ?thesis by simp
+qed
+
+lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
+  by (cases r) simp
+
+
+text \<open>
+ \medskip Concrete records are type instances of record schemes.
+\<close>
+
+definition foo5 :: nat
+  where "foo5 = getX (| xpos = 1, ypos = 0 |)"
+
+
+text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close>
+
+definition incX :: "'a point_scheme => 'a point_scheme"
+  where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
+
+lemma "incX r = setX r (Suc (getX r))"
+  by (simp add: getX_def setX_def incX_def)
+
+
+text \<open>An alternative definition.\<close>
+
+definition incX' :: "'a point_scheme => 'a point_scheme"
+  where "incX' r = r (| xpos := xpos r + 1 |)"
+
+
+subsection \<open>Coloured points: record extension\<close>
+
+datatype colour = Red | Green | Blue
+
+record cpoint = point +
+  colour :: colour
+
+
+text \<open>
+  The record declaration defines a new type constructor and abbreviations:
+  @{text [display]
+\<open>cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) =
+  () cpoint_ext_type point_ext_type
+'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) =
+  'a cpoint_ext_type point_ext_type\<close>}
+\<close>
+
+consts foo6 :: cpoint
+consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
+consts foo8 :: "'a cpoint_scheme"
+consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
+
+
+text \<open>
+ Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.
+\<close>
+
+definition foo10 :: nat
+  where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
+
+
+subsubsection \<open>Non-coercive structural subtyping\<close>
+
+text \<open>
+ Term \<^term>\<open>foo11\<close> has type \<^typ>\<open>cpoint\<close>, not type \<^typ>\<open>point\<close> ---
+ Great!
+\<close>
+
+definition foo11 :: cpoint
+  where "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
+
+
+subsection \<open>Other features\<close>
+
+text \<open>Field names contribute to record identity.\<close>
+
+record point' =
+  xpos' :: nat
+  ypos' :: nat
+
+text \<open>
+  \noindent May not apply \<^term>\<open>getX\<close> to @{term [source] "(| xpos' =
+  2, ypos' = 0 |)"} -- type error.
+\<close>
+
+text \<open>\medskip Polymorphic records.\<close>
+
+record 'a point'' = point +
+  content :: 'a
+
+type_synonym cpoint'' = "colour point''"
+
+
+
+text \<open>Updating a record field with an identical value is simplified.\<close>
+lemma "r (| xpos := xpos r |) = r"
+  by simp
+
+text \<open>Only the most recent update to a component survives simplification.\<close>
+lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)"
+  by simp
+
+text \<open>In some cases its convenient to automatically split
+(quantified) records. For this purpose there is the simproc @{ML [source]
+"Record.split_simproc"} and the tactic @{ML [source]
+"Record.split_simp_tac"}.  The simplification procedure
+only splits the records, whereas the tactic also simplifies the
+resulting goal with the standard record simplification rules. A
+(generalized) predicate on the record is passed as parameter that
+decides whether or how `deep' to split the record. It can peek on the
+subterm starting at the quantified occurrence of the record (including
+the quantifier). The value \<^ML>\<open>0\<close> indicates no split, a value
+greater \<^ML>\<open>0\<close> splits up to the given bound of record extension and
+finally the value \<^ML>\<open>~1\<close> completely splits the record.
+@{ML [source] "Record.split_simp_tac"} additionally takes a list of
+equations for simplification and can also split fixed record variables.
+
+\<close>
+
+lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+  apply simp
+  done
+
+lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply simp
+  done
+
+lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+  apply simp
+  done
+
+lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply simp
+  done
+
+lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+  apply auto
+  done
+
+lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply auto
+  done
+
+lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply auto
+  done
+
+lemma True
+proof -
+  {
+    fix P r
+    assume pre: "P (xpos r)"
+    then have "\<exists>x. P x"
+      apply -
+      apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+      apply auto
+      done
+  }
+  show ?thesis ..
+qed
+
+text \<open>The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is
+  illustrated by the following lemma.\<close>
+
+lemma "\<exists>r. xpos r = x"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
+  done
+
+
+subsection \<open>A more complex record expression\<close>
+
+record ('a, 'b, 'c) bar = bar1 :: 'a
+  bar2 :: 'b
+  bar3 :: 'c
+  bar21 :: "'b \<times> 'a"
+  bar32 :: "'c \<times> 'b"
+  bar31 :: "'c \<times> 'a"
+
+print_record "('a,'b,'c) bar"
+
+subsection \<open>Some code generation\<close>
+
+export_code foo1 foo3 foo5 foo10 checking SML
+
+text \<open>
+  Code generation can also be switched off, for instance for very large records
+\<close>
+
+declare [[record_codegen = false]]
+
+record not_so_large_record =
+  bar520 :: nat
+  bar521 :: "nat * nat"
+
+declare [[record_codegen = true]]
+
+end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/ROOT	Mon Jul 13 17:08:45 2020 +0200
@@ -20,14 +20,20 @@
   sessions
     "HOL-Library"
   theories
+    Adhoc_Overloading_Examples
     Ackermann
-    Knaster_Tarski
-    Peirce
+    Cantor
+    Coherent
+    Commands
     Drinker
-    Cantor
+    Groebner_Examples
+    Iff_Oracle
+    Induction_Schema
+    Knaster_Tarski
+    "ML"
+    Peirce
+    Records
     Seq
-    "ML"
-    Iff_Oracle
   document_files
     "root.bib"
     "root.tex"
@@ -605,7 +611,6 @@
     Miscellaneous examples for Higher-Order Logic.
   "
   theories
-    Adhoc_Overloading_Examples
     Antiquote
     Argo_Examples
     Arith_Examples
@@ -623,8 +628,6 @@
     Code_Lazy_Demo
     Code_Timing
     Coercion_Examples
-    Coherent
-    Commands
     Computations
     Conditional_Parametricity_Examples
     Cubic_Quartic
@@ -637,13 +640,11 @@
     Functions
     Function_Growth
     Gauge_Integration
-    Groebner_Examples
     Guess
     HarmonicSeries
     Hebrew
     Hex_Bin_Examples
     IArray_Examples
-    Induction_Schema
     Intuitionistic
     Join_Theory
     Lagrange
@@ -663,7 +664,6 @@
     Pythagoras
     Quicksort
     Radix_Sort
-    Records
     Reflection_Examples
     Refute_Examples
     Residue_Ring
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Jul 12 18:10:06 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(*  Title:      HOL/ex/Adhoc_Overloading_Examples.thy
-    Author:     Christian Sternagel
-*)
-
-section \<open>Ad Hoc Overloading\<close>
-
-theory Adhoc_Overloading_Examples
-imports
-  Main
-  "HOL-Library.Infinite_Set"
-  "HOL-Library.Adhoc_Overloading"
-begin
-
-text \<open>Adhoc overloading allows to overload a constant depending on
-its type. Typically this involves to introduce an uninterpreted
-constant (used for input and output) and then add some variants (used
-internally).\<close>
-
-subsection \<open>Plain Ad Hoc Overloading\<close>
-
-text \<open>Consider the type of first-order terms.\<close>
-datatype ('a, 'b) "term" =
-  Var 'b |
-  Fun 'a "('a, 'b) term list"
-
-text \<open>The set of variables of a term might be computed as follows.\<close>
-fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
-  "term_vars (Var x) = {x}" |
-  "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
-
-text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
-rewrite systems (i.e., sets of rules), the set of variables makes
-sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
-
-consts vars :: "'a \<Rightarrow> 'b set"
-
-text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
-adhoc_overloading
-  vars term_vars
-
-value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
-
-fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
-  "rule_vars (l, r) = vars l \<union> vars r"
-
-adhoc_overloading
-  vars rule_vars
-
-value [nbe] "vars (Var 1, Var 0)"
-
-definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
-  "trs_vars R = \<Union>(rule_vars ` R)"
-
-adhoc_overloading
-  vars trs_vars
-
-value [nbe] "vars {(Var 1, Var 0)}"
-
-text \<open>Sometimes it is necessary to add explicit type constraints
-before a variant can be determined.\<close>
-(*value "vars R" (*has multiple instances*)*)
-value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
-
-text \<open>It is also possible to remove variants.\<close>
-no_adhoc_overloading
-  vars term_vars rule_vars 
-
-(*value "vars (Var 1)" (*does not have an instance*)*)
-
-text \<open>As stated earlier, the overloaded constant is only used for
-input and output. Internally, always a variant is used, as can be
-observed by the configuration option \<open>show_variants\<close>.\<close>
-
-adhoc_overloading
-  vars term_vars
-
-declare [[show_variants]]
-
-term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
-
-
-subsection \<open>Adhoc Overloading inside Locales\<close>
-
-text \<open>As example we use permutations that are parametrized over an
-atom type \<^typ>\<open>'a\<close>.\<close>
-
-definition perms :: "('a \<Rightarrow> 'a) set" where
-  "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
-
-typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
-  by standard (auto simp: perms_def)
-
-text \<open>First we need some auxiliary lemmas.\<close>
-lemma permsI [Pure.intro]:
-  assumes "bij f" and "MOST x. f x = x"
-  shows "f \<in> perms"
-  using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
-
-lemma perms_imp_bij:
-  "f \<in> perms \<Longrightarrow> bij f"
-  by (simp add: perms_def)
-
-lemma perms_imp_MOST_eq:
-  "f \<in> perms \<Longrightarrow> MOST x. f x = x"
-  by (simp add: perms_def) (metis MOST_iff_finiteNeg)
-
-lemma id_perms [simp]:
-  "id \<in> perms"
-  "(\<lambda>x. x) \<in> perms"
-  by (auto simp: perms_def bij_def)
-
-lemma perms_comp [simp]:
-  assumes f: "f \<in> perms" and g: "g \<in> perms"
-  shows "(f \<circ> g) \<in> perms"
-  apply (intro permsI bij_comp)
-  apply (rule perms_imp_bij [OF g])
-  apply (rule perms_imp_bij [OF f])
-  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
-  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
-  by simp
-
-lemma perms_inv:
-  assumes f: "f \<in> perms"
-  shows "inv f \<in> perms"
-  apply (rule permsI)
-  apply (rule bij_imp_bij_inv)
-  apply (rule perms_imp_bij [OF f])
-  apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
-  apply (erule subst, rule inv_f_f)
-  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
-  done
-
-lemma bij_Rep_perm: "bij (Rep_perm p)"
-  using Rep_perm [of p] unfolding perms_def by simp
-
-instantiation perm :: (type) group_add
-begin
-
-definition "0 = Abs_perm id"
-definition "- p = Abs_perm (inv (Rep_perm p))"
-definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
-definition "(p1::'a perm) - p2 = p1 + - p2"
-
-lemma Rep_perm_0: "Rep_perm 0 = id"
-  unfolding zero_perm_def by (simp add: Abs_perm_inverse)
-
-lemma Rep_perm_add:
-  "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"
-  unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
-
-lemma Rep_perm_uminus:
-  "Rep_perm (- p) = inv (Rep_perm p)"
-  unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
-
-instance
-  apply standard
-  unfolding Rep_perm_inject [symmetric]
-  unfolding minus_perm_def
-  unfolding Rep_perm_add
-  unfolding Rep_perm_uminus
-  unfolding Rep_perm_0
-  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
-  done
-
-end
-
-lemmas Rep_perm_simps =
-  Rep_perm_0
-  Rep_perm_add
-  Rep_perm_uminus
-
-
-section \<open>Permutation Types\<close>
-
-text \<open>We want to be able to apply permutations to arbitrary types. To
-this end we introduce a constant \<open>PERMUTE\<close> together with
-convenient infix syntax.\<close>
-
-consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
-
-text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
-appliciation of permutations.\<close>
-locale permute =
-  fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
-  assumes permute_zero [simp]: "permute 0 x = x"
-    and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
-begin
-
-adhoc_overloading
-  PERMUTE permute
-
-end
-
-text \<open>Permuting atoms.\<close>
-definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "permute_atom p a = (Rep_perm p) a"
-
-adhoc_overloading
-  PERMUTE permute_atom
-
-interpretation atom_permute: permute permute_atom
-  by standard (simp_all add: permute_atom_def Rep_perm_simps)
-
-text \<open>Permuting permutations.\<close>
-definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
-  "permute_perm p q = p + q - p"
-
-adhoc_overloading
-  PERMUTE permute_perm
-
-interpretation perm_permute: permute permute_perm
-  apply standard
-  unfolding permute_perm_def
-  apply simp
-  apply (simp only: diff_conv_add_uminus minus_add add.assoc)
-  done
-
-text \<open>Permuting functions.\<close>
-locale fun_permute =
-  dom: permute perm1 + ran: permute perm2
-  for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
-  and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
-begin
-
-adhoc_overloading
-  PERMUTE perm1 perm2
-
-definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
-  "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
-
-adhoc_overloading
-  PERMUTE permute_fun
-
-end
-
-sublocale fun_permute \<subseteq> permute permute_fun
-  by (unfold_locales, auto simp: permute_fun_def)
-     (metis dom.permute_plus minus_add)
-
-lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0"
-  unfolding permute_atom_def
-  by (metis Rep_perm_0 id_apply zero_perm_def)
-
-interpretation atom_fun_permute: fun_permute permute_atom permute_atom
-  by (unfold_locales)
-
-adhoc_overloading
-  PERMUTE atom_fun_permute.permute_fun
-
-lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
-  unfolding atom_fun_permute.permute_fun_def
-  unfolding permute_atom_def
-  by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)
-
-end
-
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ex/Coherent.thy
--- a/src/HOL/ex/Coherent.thy	Sun Jul 12 18:10:06 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(*  Title:      HOL/ex/Coherent.thy
-    Author:     Stefan Berghofer, TU Muenchen
-    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
-*)
-
-section \<open>Coherent Logic Problems\<close>
-
-theory Coherent
-imports Main
-begin
-
-subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
-
-no_notation
-  comp (infixl "o" 55) and
-  relcomp (infixr "O" 75)
-
-lemma p1p2:
-  assumes "col a b c l \<and> col d e f m"
-    and "col b f g n \<and> col c e g o"
-    and "col b d h p \<and> col a e h q"
-    and "col c d i r \<and> col a f i s"
-    and "el n o \<Longrightarrow> goal"
-    and "el p q \<Longrightarrow> goal"
-    and "el s r \<Longrightarrow> goal"
-    and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
-    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
-    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
-    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
-    and "\<And>A B. pl A B \<Longrightarrow> el B B"
-    and "\<And>A B. el A B \<Longrightarrow> el B A"
-    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
-    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
-    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
-    and "\<And>A B C D E F G H I J K L M N O P Q.
-           col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
-           col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
-           (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
-    and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
-    and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
-  shows goal using assms
-  by coherent
-
-lemma p2p1:
-  assumes "col a b c l \<and> col d e f m"
-    and "col b f g n \<and> col c e g o"
-    and "col b d h p \<and> col a e h q"
-    and "col c d i r \<and> col a f i s"
-    and "pl a m \<Longrightarrow> goal"
-    and "pl b m \<Longrightarrow> goal"
-    and "pl c m \<Longrightarrow> goal"
-    and "pl d l \<Longrightarrow> goal"
-    and "pl e l \<Longrightarrow> goal"
-    and "pl f l \<Longrightarrow> goal"
-    and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
-    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
-    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
-    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
-    and "\<And>A B. pl A B \<Longrightarrow> el B B"
-    and "\<And>A B. el A B \<Longrightarrow> el B A"
-    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
-    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
-    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
-    and "\<And>A B C D E F G H I J K L M N O P Q.
-           col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
-           col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
-           (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
-    and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
-    and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
-  shows goal using assms
-  by coherent
-
-
-subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
-
-lemma diamond:
-  assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
-    and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
-    and "\<And>A. equalish A A" 
-    and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
-    and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
-    and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
-    and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
-    and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
-    and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
-  shows goal using assms
-  by coherent
-
-end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ex/Commands.thy
--- a/src/HOL/ex/Commands.thy	Sun Jul 12 18:10:06 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-(*  Title:      HOL/ex/Commands.thy
-    Author:     Makarius
-*)
-
-section \<open>Some Isar command definitions\<close>
-
-theory Commands
-imports Main
-keywords
-  "print_test" :: diag and
-  "global_test" :: thy_decl and
-  "local_test" :: thy_decl
-begin
-
-subsection \<open>Diagnostic command: no state change\<close>
-
-ML \<open>
-  Outer_Syntax.command \<^command_keyword>\<open>print_test\<close> "print term test"
-    (Parse.term >> (fn s => Toplevel.keep (fn st =>
-      let
-        val ctxt = Toplevel.context_of st;
-        val t = Syntax.read_term ctxt s;
-        val ctxt' = Proof_Context.augment t ctxt;
-      in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
-\<close>
-
-print_test x
-print_test "\<lambda>x. x = a"
-
-
-subsection \<open>Old-style global theory declaration\<close>
-
-ML \<open>
-  Outer_Syntax.command \<^command_keyword>\<open>global_test\<close> "test constant declaration"
-    (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
-      let
-        val thy' = Sign.add_consts [(b, \<^typ>\<open>'a\<close>, NoSyn)] thy;
-      in thy' end)));
-\<close>
-
-global_test a
-global_test b
-print_test a
-
-
-subsection \<open>Local theory specification\<close>
-
-ML \<open>
-  Outer_Syntax.local_theory \<^command_keyword>\<open>local_test\<close> "test local definition"
-    (Parse.binding -- (\<^keyword>\<open>=\<close> |-- Parse.term) >> (fn (b, s) => fn lthy =>
-      let
-        val t = Syntax.read_term lthy s;
-        val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
-      in lthy' end));
-\<close>
-
-local_test true = True
-print_test true
-thm true_def
-
-local_test identity = "\<lambda>x. x"
-print_test "identity x"
-thm identity_def
-
-context fixes x y :: nat
-begin
-
-local_test test = "x + y"
-print_test test
-thm test_def
-
-end
-
-print_test "test 0 1"
-thm test_def
-
-end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Sun Jul 12 18:10:06 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(*  Title:      HOL/ex/Groebner_Examples.thy
-    Author:     Amine Chaieb, TU Muenchen
-*)
-
-section \<open>Groebner Basis Examples\<close>
-
-theory Groebner_Examples
-imports Main
-begin
-
-subsection \<open>Basic examples\<close>
-
-lemma
-  fixes x :: int
-  shows "x ^ 3 = x ^ 3"
-  apply (tactic \<open>ALLGOALS (CONVERSION
-    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
-  by (rule refl)
-
-lemma
-  fixes x :: int
-  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<^sup>2 + (80 * x + 32))))" 
-  apply (tactic \<open>ALLGOALS (CONVERSION
-    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
-  by (rule refl)
-
-schematic_goal
-  fixes x :: int
-  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
-  apply (tactic \<open>ALLGOALS (CONVERSION
-    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
-  by (rule refl)
-
-lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
-  apply (simp only: power_Suc power_0)
-  apply (simp only: semiring_norm)
-  oops
-
-lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
-  by algebra
-
-lemma "(4::nat) + 4 = 3 + 5"
-  by algebra
-
-lemma "(4::int) + 0 = 4"
-  apply algebra?
-  by simp
-
-lemma
-  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
-  shows "d\<^sup>2 * c\<^sup>2 - 2 * d * c * a * f + a\<^sup>2 * f\<^sup>2 - e * d * b * c - e * b * a * f +
-    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
-  using assms by algebra
-
-lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
-  by algebra
-
-theorem "x* (x\<^sup>2 - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
-  by algebra
-
-lemma
-  fixes x::"'a::idom"
-  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
-  by algebra
-
-subsection \<open>Lemmas for Lagrange's theorem\<close>
-
-definition
-  sq :: "'a::times => 'a" where
-  "sq x == x*x"
-
-lemma
-  fixes x1 :: "'a::{idom}"
-  shows
-  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
-    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
-    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
-    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
-    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
-  by (algebra add: sq_def)
-
-lemma
-  fixes p1 :: "'a::{idom}"
-  shows
-  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
-   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
-    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
-      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
-      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
-      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
-      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
-      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
-      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
-      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
-  by (algebra add: sq_def)
-
-
-subsection \<open>Colinearity is invariant by rotation\<close>
-
-type_synonym point = "int \<times> int"
-
-definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
-  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
-    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
-
-lemma collinear_inv_rotation:
-  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
-  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
-    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
-  using assms 
-  by (algebra add: collinear_def split_def fst_conv snd_conv)
-
-lemma "\<exists>(d::int). a*y - a*x = n*d \<Longrightarrow> \<exists>u v. a*u + n*v = 1 \<Longrightarrow> \<exists>e. y - x = n*e"
-  by algebra
-
-end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ex/Induction_Schema.thy
--- a/src/HOL/ex/Induction_Schema.thy	Sun Jul 12 18:10:06 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/ex/Induction_Schema.thy
-    Author:     Alexander Krauss, TU Muenchen
-*)
-
-section \<open>Examples of automatically derived induction rules\<close>
-
-theory Induction_Schema
-imports Main
-begin
-
-subsection \<open>Some simple induction principles on nat\<close>
-
-lemma nat_standard_induct: (* cf. Nat.thy *)
-  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
-by induction_schema (pat_completeness, lexicographic_order)
-
-lemma nat_induct2:
-  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
-  \<Longrightarrow> P n"
-by induction_schema (pat_completeness, lexicographic_order)
-
-lemma minus_one_induct:
-  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
-by induction_schema (pat_completeness, lexicographic_order)
-
-theorem diff_induct: (* cf. Nat.thy *)
-  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
-    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
-by induction_schema (pat_completeness, lexicographic_order)
-
-lemma list_induct2': (* cf. List.thy *)
-  "\<lbrakk> P [] [];
-  \<And>x xs. P (x#xs) [];
-  \<And>y ys. P [] (y#ys);
-   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
- \<Longrightarrow> P xs ys"
-by induction_schema (pat_completeness, lexicographic_order)
-
-theorem even_odd_induct:
-  assumes "R 0"
-  assumes "Q 0"
-  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
-  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
-  shows "R n" "Q n"
-  using assms
-by induction_schema (pat_completeness+, lexicographic_order)
-
-end
diff -r 759532ef0885 -r 83456d9f0ed5 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Sun Jul 12 18:10:06 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,344 +0,0 @@
-(*  Title:      HOL/ex/Records.thy
-    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel,
-                TU Muenchen
-*)
-
-section \<open>Using extensible records in HOL -- points and coloured points\<close>
-
-theory Records
-imports Main
-begin
-
-subsection \<open>Points\<close>
-
-record point =
-  xpos :: nat
-  ypos :: nat
-
-text \<open>
-  Apart many other things, above record declaration produces the
-  following theorems:
-\<close>
-
-
-thm point.simps
-thm point.iffs
-thm point.defs
-
-text \<open>
-  The set of theorems @{thm [source] point.simps} is added
-  automatically to the standard simpset, @{thm [source] point.iffs} is
-  added to the Classical Reasoner and Simplifier context.
-
-  \medskip Record declarations define new types and type abbreviations:
-  @{text [display]
-\<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
-'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type\<close>}
-\<close>
-
-consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
-consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
-
-
-subsubsection \<open>Introducing concrete records and record schemes\<close>
-
-definition foo1 :: point
-  where "foo1 = (| xpos = 1, ypos = 0 |)"
-
-definition foo3 :: "'a => 'a point_scheme"
-  where "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
-
-
-subsubsection \<open>Record selection and record update\<close>
-
-definition getX :: "'a point_scheme => nat"
-  where "getX r = xpos r"
-
-definition setX :: "'a point_scheme => nat => 'a point_scheme"
-  where "setX r n = r (| xpos := n |)"
-
-
-subsubsection \<open>Some lemmas about records\<close>
-
-text \<open>Basic simplifications.\<close>
-
-lemma "point.make n p = (| xpos = n, ypos = p |)"
-  by (simp only: point.make_def)
-
-lemma "xpos (| xpos = m, ypos = n, ... = p |) = m"
-  by simp
-
-lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)"
-  by simp
-
-
-text \<open>\medskip Equality of records.\<close>
-
-lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
-  \<comment> \<open>introduction of concrete record equality\<close>
-  by simp
-
-lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
-  \<comment> \<open>elimination of concrete record equality\<close>
-  by simp
-
-lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-  \<comment> \<open>introduction of abstract record equality\<close>
-  by simp
-
-lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
-  \<comment> \<open>elimination of abstract record equality (manual proof)\<close>
-proof -
-  assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
-  then have "xpos ?lhs = xpos ?rhs" by simp
-  then show ?thesis by simp
-qed
-
-
-text \<open>\medskip Surjective pairing\<close>
-
-lemma "r = (| xpos = xpos r, ypos = ypos r |)"
-  by simp
-
-lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
-  by simp
-
-
-text \<open>
-  \medskip Representation of records by cases or (degenerate)
-  induction.
-\<close>
-
-lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-proof (cases r)
-  fix xpos ypos more
-  assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
-  then show ?thesis by simp
-qed
-
-lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-proof (induct r)
-  fix xpos ypos more
-  show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) =
-      (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)"
-    by simp
-qed
-
-lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
-proof (cases r)
-  fix xpos ypos more
-  assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
-  then show ?thesis by simp
-qed
-
-lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
-proof (cases r)
-  case fields
-  then show ?thesis by simp
-qed
-
-lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
-  by (cases r) simp
-
-
-text \<open>
- \medskip Concrete records are type instances of record schemes.
-\<close>
-
-definition foo5 :: nat
-  where "foo5 = getX (| xpos = 1, ypos = 0 |)"
-
-
-text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close>
-
-definition incX :: "'a point_scheme => 'a point_scheme"
-  where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
-
-lemma "incX r = setX r (Suc (getX r))"
-  by (simp add: getX_def setX_def incX_def)
-
-
-text \<open>An alternative definition.\<close>
-
-definition incX' :: "'a point_scheme => 'a point_scheme"
-  where "incX' r = r (| xpos := xpos r + 1 |)"
-
-
-subsection \<open>Coloured points: record extension\<close>
-
-datatype colour = Red | Green | Blue
-
-record cpoint = point +
-  colour :: colour
-
-
-text \<open>
-  The record declaration defines a new type constructor and abbreviations:
-  @{text [display]
-\<open>cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) =
-  () cpoint_ext_type point_ext_type
-'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) =
-  'a cpoint_ext_type point_ext_type\<close>}
-\<close>
-
-consts foo6 :: cpoint
-consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
-consts foo8 :: "'a cpoint_scheme"
-consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
-
-
-text \<open>
- Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.
-\<close>
-
-definition foo10 :: nat
-  where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
-
-
-subsubsection \<open>Non-coercive structural subtyping\<close>
-
-text \<open>
- Term \<^term>\<open>foo11\<close> has type \<^typ>\<open>cpoint\<close>, not type \<^typ>\<open>point\<close> ---
- Great!
-\<close>
-
-definition foo11 :: cpoint
-  where "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
-
-
-subsection \<open>Other features\<close>
-
-text \<open>Field names contribute to record identity.\<close>
-
-record point' =
-  xpos' :: nat
-  ypos' :: nat
-
-text \<open>
-  \noindent May not apply \<^term>\<open>getX\<close> to @{term [source] "(| xpos' =
-  2, ypos' = 0 |)"} -- type error.
-\<close>
-
-text \<open>\medskip Polymorphic records.\<close>
-
-record 'a point'' = point +
-  content :: 'a
-
-type_synonym cpoint'' = "colour point''"
-
-
-
-text \<open>Updating a record field with an identical value is simplified.\<close>
-lemma "r (| xpos := xpos r |) = r"
-  by simp
-
-text \<open>Only the most recent update to a component survives simplification.\<close>
-lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)"
-  by simp
-
-text \<open>In some cases its convenient to automatically split
-(quantified) records. For this purpose there is the simproc @{ML [source]
-"Record.split_simproc"} and the tactic @{ML [source]
-"Record.split_simp_tac"}.  The simplification procedure
-only splits the records, whereas the tactic also simplifies the
-resulting goal with the standard record simplification rules. A
-(generalized) predicate on the record is passed as parameter that
-decides whether or how `deep' to split the record. It can peek on the
-subterm starting at the quantified occurrence of the record (including
-the quantifier). The value \<^ML>\<open>0\<close> indicates no split, a value
-greater \<^ML>\<open>0\<close> splits up to the given bound of record extension and
-finally the value \<^ML>\<open>~1\<close> completely splits the record.
-@{ML [source] "Record.split_simp_tac"} additionally takes a list of
-equations for simplification and can also split fixed record variables.
-
-\<close>
-
-lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
-  apply simp
-  done
-
-lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply simp
-  done
-
-lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
-  apply simp
-  done
-
-lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply simp
-  done
-
-lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
-  apply auto
-  done
-
-lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply auto
-  done
-
-lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply auto
-  done
-
-lemma True
-proof -
-  {
-    fix P r
-    assume pre: "P (xpos r)"
-    then have "\<exists>x. P x"
-      apply -
-      apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-      apply auto
-      done
-  }
-  show ?thesis ..
-qed
-
-text \<open>The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is
-  illustrated by the following lemma.\<close>
-
-lemma "\<exists>r. xpos r = x"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
-  done
-
-
-subsection \<open>A more complex record expression\<close>
-
-record ('a, 'b, 'c) bar = bar1 :: 'a
-  bar2 :: 'b
-  bar3 :: 'c
-  bar21 :: "'b \<times> 'a"
-  bar32 :: "'c \<times> 'b"
-  bar31 :: "'c \<times> 'a"
-
-print_record "('a,'b,'c) bar"
-
-subsection \<open>Some code generation\<close>
-
-export_code foo1 foo3 foo5 foo10 checking SML
-
-text \<open>
-  Code generation can also be switched off, for instance for very large records
-\<close>
-
-declare [[record_codegen = false]]
-
-record not_so_large_record =
-  bar520 :: nat
-  bar521 :: "nat * nat"
-
-declare [[record_codegen = true]]
-
-end