author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46914  c2ca2c3d23a6 
child 58249  180f1b3508ed 
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 

46914  7 
theory Term 
8 
imports Main 

9 
begin 

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

10 

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

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

12 
Var 'a 
b5f5942781a0
Induct: converted some theories to newstyle 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 newstyle 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 

37597  18 
primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" 
46914  19 
and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" 
20 
where 

5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset

21 
"subst_term f (Var a) = f a" 
37597  22 
 "subst_term f (App b ts) = App b (subst_term_list f ts)" 
23 
 "subst_term_list f [] = []" 

24 
 "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

25 

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

26 

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

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

28 

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

29 
lemma subst_comp: 
12171  30 
"subst_term (subst_term f1 \<circ> f2) t = 
31 
subst_term f1 (subst_term f2 t)" 

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

33 
subst_term_list f1 (subst_term_list f2 ts)" 

34 
by (induct t and ts) simp_all 

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

35 

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

36 

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

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

38 

12171  39 
lemma 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12171
diff
changeset

40 
assumes var: "!!v. P (Var v)" 
37597  41 
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

42 
shows term_induct2: "P t" 
37597  43 
and "\<forall>t \<in> set ts. P t" 
12171  44 
apply (induct t and ts) 
45 
apply (rule var) 

46 
apply (rule app) 

47 
apply assumption 

48 
apply simp_all 

49 
done 

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

50 

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

51 
end 