author  haftmann 
Mon, 28 Jun 2010 15:32:13 +0200  
changeset 37597  a02ea93e88c6 
parent 36862  952b2b102a0a 
child 46914  c2ca2c3d23a6 
permissions  rwrr 
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 newstyle format;
wenzelm
parents:
5738
diff
changeset

5 
header {* Terms over a given alphabet *} 
b5f5942781a0
Induct: converted some theories to newstyle 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 newstyle format;
wenzelm
parents:
5738
diff
changeset

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

10 
Var 'a 
b5f5942781a0
Induct: converted some theories to newstyle 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 newstyle 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  16 
primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" 
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  19 
 "subst_term f (App b ts) = App b (subst_term_list f ts)" 
20 
 "subst_term_list f [] = []" 

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 newstyle format;
wenzelm
parents:
5738
diff
changeset

23 

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

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

25 

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

26 
lemma subst_comp: 
12171  27 
"subst_term (subst_term f1 \<circ> f2) t = 
28 
subst_term f1 (subst_term f2 t)" 

29 
and "subst_term_list (subst_term f1 \<circ> f2) ts = 

30 
subst_term_list f1 (subst_term_list f2 ts)" 

31 
by (induct t and ts) simp_all 

11046
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 

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

34 
text {* \medskip Alternative induction rule *} 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

35 

12171  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  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  40 
and "\<forall>t \<in> set ts. P t" 
12171  41 
apply (induct t and ts) 
42 
apply (rule var) 

43 
apply (rule app) 

44 
apply assumption 

45 
apply simp_all 

46 
done 

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

47 

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

48 
end 