author  wenzelm 
Mon, 01 Oct 2001 15:46:35 +0200  
changeset 11649  dfb59b9954a6 
parent 11549  e7265e70fd7c 
child 11809  c9ffdd63dd93 
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 
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 newstyle format;
wenzelm
parents:
5738
diff
changeset

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

8 

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

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

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

31 

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

32 
text {* \medskip A simple theorem about composition of substitutions *} 
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 
lemma subst_comp: 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

35 
"(subst_term ((subst_term f1) \<circ> f2) t) = 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

36 
(subst_term f1 (subst_term f2 t)) \<and> 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

37 
(subst_term_list ((subst_term f1) \<circ> f2) ts) = 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

38 
(subst_term_list f1 (subst_term_list f2 ts))" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

39 
apply (induct t and ts rule: term.induct) 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

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

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

42 

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

43 

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

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

45 

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

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

47 
"(!!v. P (Var v)) ==> 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

48 
(!!f ts. list_all P ts ==> P (App f ts)) 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

49 
==> P t" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

50 
proof  
11549  51 
case rule_context 
11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

52 
have "P t \<and> list_all P ts" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

53 
apply (induct t and ts rule: term.induct) 
11549  54 
apply (rule rule_context) 
55 
apply (rule rule_context) 

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

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

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

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

59 
thus ?thesis .. 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5738
diff
changeset

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

61 

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

62 
end 