# HG changeset patch # User wenzelm # Date 1571735692 -7200 # Node ID 05810acd48585d058bc2309735574f47a9ba552e # Parent 1e0ad25c94c85ad137e708f63b6614ca4d1f7150 clarified types (again): 'a is canonical for 'class' (as alternative to 'locale'), 'b is common for Hindley-Milner examples; diff -r 1e0ad25c94c8 -r 05810acd4858 src/HOL/ex/Peano_Axioms.thy --- a/src/HOL/ex/Peano_Axioms.thy Mon Oct 21 16:32:10 2019 +0200 +++ b/src/HOL/ex/Peano_Axioms.thy Tue Oct 22 11:14:52 2019 +0200 @@ -4,12 +4,12 @@ imports Main begin -locale peano = - fixes zero :: 'n - fixes succ :: "'n \ 'n" +locale peano = \ \or: \<^theory_text>\class\\ + fixes zero :: 'a + fixes succ :: "'a \ 'a" assumes succ_neq_zero [simp]: "succ m \ zero" assumes succ_inject [simp]: "succ m = succ n \ m = n" - assumes induct [case_names zero succ, induct type: 'n]: + assumes induct [case_names zero succ, induct type: 'a]: "P zero \ (\n. P n \ P (succ n)) \ P n" begin @@ -19,13 +19,13 @@ text \\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\ -inductive Rec :: "'a \ ('n \ 'a \ 'a) \ 'n \ 'a \ bool" - for e :: 'a and r :: "'n \ 'a \ 'a" +inductive Rec :: "'b \ ('a \ 'b \ 'b) \ 'a \ 'b \ bool" + for e :: 'b and r :: "'a \ 'b \ 'b" where Rec_zero: "Rec e r zero e" | Rec_succ: "Rec e r m n \ Rec e r (succ m) (r m n)" -lemma Rec_functional: "\!y::'a. Rec e r x y" for x :: 'n +lemma Rec_functional: "\!y::'b. Rec e r x y" for x :: 'a proof - let ?R = "Rec e r" show ?thesis @@ -59,7 +59,7 @@ text \\<^medskip> The recursion operator -- polymorphic!\ -definition rec :: "'a \ ('n \ 'a \ 'a) \ 'n \ 'a" +definition rec :: "'b \ ('a \ 'b \ 'b) \ 'a \ 'b" where "rec e r x = (THE y. Rec e r x y)" lemma rec_eval: @@ -84,7 +84,7 @@ text \\<^medskip> Example: addition (monomorphic)\ -definition add :: "'n \ 'n \ 'n" +definition add :: "'a \ 'a \ 'a" where "add m n = rec n (\_ k. succ k) m" lemma add_zero [simp]: "add zero n = n" @@ -107,7 +107,7 @@ text \\<^medskip> Example: replication (polymorphic)\ -definition repl :: "'n \ 'a \ 'a list" +definition repl :: "'a \ 'b \ 'b list" where "repl n x = rec [] (\_ xs. x # xs) n" lemma repl_zero [simp]: "repl zero x = []"