author | wenzelm |
Wed, 12 May 2010 14:17:26 +0200 | |
changeset 36862 | 952b2b102a0a |
parent 18461 | 9125d278fdc8 |
child 37597 | a02ea93e88c6 |
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 |
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 | 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 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
consts |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
17 |
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
|
18 |
subst_term_list :: |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
19 |
"('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
|
20 |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
21 |
primrec |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
22 |
"subst_term f (Var a) = f a" |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
23 |
"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
|
24 |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
25 |
"subst_term_list f [] = []" |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
26 |
"subst_term_list f (t # ts) = |
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
27 |
subst_term f t # subst_term_list f ts" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
28 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
29 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
30 |
text {* \medskip A simple theorem about composition of substitutions *} |
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 |
lemma subst_comp: |
12171 | 33 |
"subst_term (subst_term f1 \<circ> f2) t = |
34 |
subst_term f1 (subst_term f2 t)" |
|
35 |
and "subst_term_list (subst_term f1 \<circ> f2) ts = |
|
36 |
subst_term_list f1 (subst_term_list f2 ts)" |
|
37 |
by (induct t and ts) simp_all |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
38 |
|
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 |
text {* \medskip Alternative induction rule *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
41 |
|
12171 | 42 |
lemma |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12171
diff
changeset
|
43 |
assumes var: "!!v. P (Var v)" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12171
diff
changeset
|
44 |
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
|
45 |
shows term_induct2: "P t" |
18461 | 46 |
and "list_all P ts" |
12171 | 47 |
apply (induct t and ts) |
48 |
apply (rule var) |
|
49 |
apply (rule app) |
|
50 |
apply assumption |
|
51 |
apply simp_all |
|
52 |
done |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
53 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
54 |
end |