src/HOL/Induct/Term.thy
author haftmann
Mon, 28 Jun 2010 15:32:13 +0200
changeset 37597 a02ea93e88c6
parent 36862 952b2b102a0a
child 46914 c2ca2c3d23a6
permissions -rw-r--r--
modernized specifications
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
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
     2
    Author:     Stefan Berghofer,  TU Muenchen
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     5
header {* Terms over a given alphabet *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory Term imports Main begin
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     9
datatype ('a, 'b) "term" =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    10
    Var 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    11
  | App 'b "('a, 'b) term list"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    13
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    14
text {* \medskip Substitution function on terms *}
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    16
primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    17
  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    18
  "subst_term f (Var a) = f a"
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    19
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    20
| "subst_term_list f [] = []"
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    21
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    23
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    24
text {* \medskip A simple theorem about composition of substitutions *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    25
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    26
lemma subst_comp:
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    27
  "subst_term (subst_term f1 \<circ> f2) t =
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    28
    subst_term f1 (subst_term f2 t)"
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    29
and "subst_term_list (subst_term f1 \<circ> f2) ts =
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    30
    subst_term_list f1 (subst_term_list f2 ts)"
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    31
  by (induct t and ts) simp_all
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    32
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
text {* \medskip Alternative induction rule *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    35
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    36
lemma
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12171
diff changeset
    37
  assumes var: "!!v. P (Var v)"
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    38
    and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12171
diff changeset
    39
  shows term_induct2: "P t"
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    40
    and "\<forall>t \<in> set ts. P t"
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    41
  apply (induct t and ts)
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    42
     apply (rule var)
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    43
    apply (rule app)
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    44
    apply assumption
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    45
   apply simp_all
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    46
  done
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    47
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
end