--- 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>
--- 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>
--- 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
--- 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
--- /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
+
--- /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
--- /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
--- /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
--- 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
*)
--- /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
--- /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
--- 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
--- 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
-
--- 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
--- 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
--- 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
--- 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
--- 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