author | wenzelm |
Thu, 19 Jun 2008 20:48:01 +0200 | |
changeset 27277 | 7b7ce2d7fafe |
parent 18461 | 9125d278fdc8 |
child 36862 | 952b2b102a0a |
permissions | -rw-r--r-- |
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 |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
6 |
header {* Terms over a given alphabet *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
7 |
|
16417 | 8 |
theory Term imports Main begin |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
9 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
10 |
datatype ('a, 'b) "term" = |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
11 |
Var 'a |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
12 |
| App 'b "('a, 'b) term list" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
14 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
15 |
text {* \medskip Substitution function on terms *} |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
consts |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
18 |
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
|
19 |
subst_term_list :: |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
20 |
"('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
|
21 |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
22 |
primrec |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
23 |
"subst_term f (Var a) = f a" |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
24 |
"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
|
25 |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
26 |
"subst_term_list f [] = []" |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
27 |
"subst_term_list f (t # ts) = |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
28 |
subst_term f t # subst_term_list f ts" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
29 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
30 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
31 |
text {* \medskip A simple theorem about composition of substitutions *} |
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 |
lemma subst_comp: |
12171 | 34 |
"subst_term (subst_term f1 \<circ> f2) t = |
35 |
subst_term f1 (subst_term f2 t)" |
|
36 |
and "subst_term_list (subst_term f1 \<circ> f2) ts = |
|
37 |
subst_term_list f1 (subst_term_list f2 ts)" |
|
38 |
by (induct t and ts) simp_all |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
39 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
40 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
41 |
text {* \medskip Alternative induction rule *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
42 |
|
12171 | 43 |
lemma |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12171
diff
changeset
|
44 |
assumes var: "!!v. P (Var v)" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12171
diff
changeset
|
45 |
and app: "!!f ts. list_all P ts ==> P (App f ts)" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12171
diff
changeset
|
46 |
shows term_induct2: "P t" |
18461 | 47 |
and "list_all P ts" |
12171 | 48 |
apply (induct t and ts) |
49 |
apply (rule var) |
|
50 |
apply (rule app) |
|
51 |
apply assumption |
|
52 |
apply simp_all |
|
53 |
done |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
54 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
55 |
end |