src/HOL/Induct/Term.thy
author wenzelm
Sat, 03 Feb 2001 17:40:16 +0100
changeset 11046 b5f5942781a0
parent 5738 0d8698c15439
child 11549 e7265e70fd7c
permissions -rw-r--r--
Induct: converted some theories to new-style format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
     1
(*  Title:      HOL/Induct/Term.thy
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
     3
    Author:     Stefan Berghofer,  TU Muenchen
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
     4
    Copyright   1998  TU Muenchen
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     7
header {* Terms over a given alphabet *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     8
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     9
theory Term = Main:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    11
datatype ('a, 'b) "term" =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    12
    Var 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    13
  | App 'b "('a, 'b) term list"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    15
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    16
text {* \medskip Substitution function on terms *}
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
consts
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    19
  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    20
  subst_term_list ::
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    21
    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    23
primrec
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    24
  "subst_term f (Var a) = f a"
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    25
  "subst_term f (App b ts) = App b (subst_term_list f ts)"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    27
  "subst_term_list f [] = []"
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    28
  "subst_term_list f (t # ts) =
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    29
     subst_term f t # subst_term_list f ts"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    31
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    32
text {* \medskip A simple theorem about composition of substitutions *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    33
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    34
lemma subst_comp:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    35
  "(subst_term ((subst_term f1) \<circ> f2) t) =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    36
    (subst_term f1 (subst_term f2 t)) \<and>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    37
  (subst_term_list ((subst_term f1) \<circ> f2) ts) =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    38
    (subst_term_list f1 (subst_term_list f2 ts))"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    39
  apply (induct t and ts rule: term.induct)
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    40
     apply simp_all
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    41
  done
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    42
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    43
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    44
text {* \medskip Alternative induction rule *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    45
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    46
lemma term_induct2:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    47
  "(!!v. P (Var v)) ==>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    48
    (!!f ts. list_all P ts ==> P (App f ts))
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    49
  ==> P t"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    50
proof -
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    51
  case antecedent
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    52
  have "P t \<and> list_all P ts"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    53
    apply (induct t and ts rule: term.induct)
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    54
       apply (rule antecedent)
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    55
      apply (rule antecedent)
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    56
      apply assumption
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    57
     apply simp_all
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    58
    done
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    59
  thus ?thesis ..
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    60
qed
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    61
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
end