src/FOL/ex/NatClass.thy
author wenzelm
Sun, 26 Nov 2006 23:43:53 +0100
changeset 21539 c5cf9243ad62
parent 21404 eb85850d3eb7
child 29751 e2756594c414
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1246
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
     1
(*  Title:      FOL/ex/NatClass.thy
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
     4
*)
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
     5
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
     6
theory NatClass
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
     7
imports FOL
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
     8
begin
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
     9
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    10
text {*
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    11
  This is an abstract version of theory @{text "Nat"}. Instead of
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    12
  axiomatizing a single type @{text nat} we define the class of all
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    13
  these types (up to isomorphism).
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    14
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    15
  Note: The @{text rec} operator had to be made \emph{monomorphic},
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    16
  because class axioms may not contain more than one type variable.
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    17
*}
1246
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    18
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    19
consts
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    20
  0 :: 'a    ("0")
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    21
  Suc :: "'a => 'a"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    22
  rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"
1246
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    23
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    24
axclass
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    25
  nat < "term"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    26
  induct:        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    27
  Suc_inject:    "Suc(m) = Suc(n) ==> m = n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    28
  Suc_neq_0:     "Suc(m) = 0 ==> R"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    29
  rec_0:         "rec(0, a, f) = a"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1322
diff changeset
    30
  rec_Suc:       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
1246
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    31
19819
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    32
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19819
diff changeset
    33
  add :: "['a::nat, 'a] => 'a"  (infixl "+" 60) where
19819
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    34
  "m + n = rec(m, n, %x y. Suc(y))"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    35
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    36
lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    37
apply (rule_tac n = k in induct)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    38
apply (rule notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    39
apply (erule Suc_neq_0)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    40
apply (rule notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    41
apply (erule notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    42
apply (erule Suc_inject)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    43
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    44
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    45
lemma "(k+m)+n = k+(m+n)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    46
apply (rule induct)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    47
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    48
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    49
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    50
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    51
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    52
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    53
oops
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    54
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    55
lemma add_0 [simp]: "0+n = n"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    56
apply (unfold add_def)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    57
apply (rule rec_0)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    58
done
1246
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    59
19819
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    60
lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    61
apply (unfold add_def)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    62
apply (rule rec_Suc)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    63
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    64
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    65
lemma add_assoc: "(k+m)+n = k+(m+n)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    66
apply (rule_tac n = k in induct)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    67
apply simp
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    68
apply simp
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    69
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    70
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    71
lemma add_0_right: "m+0 = m"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    72
apply (rule_tac n = m in induct)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    73
apply simp
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    74
apply simp
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    75
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    76
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    77
lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    78
apply (rule_tac n = m in induct)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    79
apply simp_all
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    80
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    81
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    82
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    83
  assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    84
  shows "f(i+j) = i+f(j)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    85
apply (rule_tac n = i in induct)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    86
apply simp
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    87
apply (simp add: prem)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17274
diff changeset
    88
done
1246
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    89
706cfddca75c the NatClass demo of the axclass tutorial;
wenzelm
parents:
diff changeset
    90
end