author | wenzelm |
Tue, 16 Oct 2001 17:58:13 +0200 | |
changeset 11809 | c9ffdd63dd93 |
parent 11649 | dfb59b9954a6 |
child 12171 | dc87f33db447 |
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 |
11649 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
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))" |
11809 | 39 |
apply (induct t and ts) |
11046
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 - |
11549 | 51 |
case rule_context |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
5738
diff
changeset
|
52 |
have "P t \<and> list_all P ts" |
11809 | 53 |
apply (induct t and ts) |
11549 | 54 |
apply (rule rule_context) |
55 |
apply (rule rule_context) |
|
11046
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 |