author  kleing 
Mon, 21 Jun 2004 10:25:57 +0200  
changeset 14981  e73f8140af78 
parent 12937  0c4fd7529467 
child 16417  9bc16273c2d4 
permissions  rwrr 
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 newstyle format;
wenzelm
parents:
5738
diff
changeset

6 
header {* Terms over a given alphabet *} 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

7 

b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

8 
theory Term = Main: 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

10 
datatype ('a, 'b) "term" = 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

11 
Var 'a 
b5f5942781a0
Induct: converted some theories to newstyle 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 newstyle 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 newstyle 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 newstyle 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 newstyle format;
wenzelm
parents:
5738
diff
changeset

30 

b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

31 
text {* \medskip A simple theorem about composition of substitutions *} 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

32 

b5f5942781a0
Induct: converted some theories to newstyle 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 newstyle format;
wenzelm
parents:
5738
diff
changeset

39 

b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

40 

b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

41 
text {* \medskip Alternative induction rule *} 
b5f5942781a0
Induct: converted some theories to newstyle 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" 
12171  47 
and "list_all P ts" 
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 newstyle format;
wenzelm
parents:
5738
diff
changeset

54 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
end 