author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5143  b94cd208f073 
child 5223  4cb05273f764 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/Term 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1992 University of Cambridge 
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 
Terms over a given alphabet  function applications; illustrates list functor 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
(essentially the same type as in Trees & Forests) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

9 

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

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

11 

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

12 
(*** Monotonicity and unfolding of the function ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 

5069  14 
Goal "term(A) = A <*> list(term(A))"; 
4089  15 
by (fast_tac (claset() addSIs term.intrs 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
addEs [term.elim]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
qed "term_unfold"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 

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

19 
(*This justifies using term in other recursive type definitions*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

20 
Goalw term.defs "A<=B ==> term(A) <= term(B)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
qed "term_mono"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 

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

24 
(** Type checking  term creates wellfounded sets **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 

5069  26 
Goalw term.defs "term(sexp) <= sexp"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
by (rtac lfp_lowerbound 1); 
4089  28 
by (fast_tac (claset() addIs [sexp.SconsI, list_sexp RS subsetD]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
qed "term_sexp"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 

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

31 
(* A <= sexp ==> term(A) <= sexp *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 
bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 

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

34 

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

35 
(** Elimination  structural induction on the set term(A) **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 

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

37 
(*Induction for the set term(A) *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
val [major,minor] = goal Term.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
"[ M: term(A); \ 
3842  40 
\ !!x zs. [ x: A; zs: list(term(A)); zs: list({x. R(x)}) \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5143
diff
changeset

41 
\ ] ==> R (Scons x zs) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
\ ] ==> R(M)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
by (rtac (major RS term.induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
by (REPEAT (eresolve_tac ([minor] @ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 
([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 
(*Proof could also use mono_Int RS subsetD RS IntE *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
qed "Term_induct"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 

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

49 
(*Induction on term(A) followed by induction on list *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 
val major::prems = goal Term.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
"[ M: term(A); \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5143
diff
changeset

52 
\ !!x. [ x: A ] ==> R (Scons x NIL); \ 
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5143
diff
changeset

53 
\ !!x z zs. [ x: A; z: term(A); zs: list(term(A)); R (Scons x zs) \ 
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5143
diff
changeset

54 
\ ] ==> R (Scons x (CONS z zs)) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
\ ] ==> R(M)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
by (rtac (major RS Term_induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 
by (etac list.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

58 
by (REPEAT (ares_tac prems 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

59 
qed "Term_induct2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 

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

61 
(*** Structural Induction on the abstract type 'a term ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 

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

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

64 
Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 

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

66 
(*Induction for the abstract type 'a term*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 
val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def] 
3649
e530286d4847
Renamed set_of_list to set, and relevant theorems too
paulson
parents:
3427
diff
changeset

68 
"[ !!x ts. (ALL t: set ts. R t) ==> R(App x ts) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

69 
\ ] ==> R(t)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 
by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 
by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 
by (rtac (Rep_term RS Term_induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
list_subset_sexp, range_Leaf_subset_sexp] 1 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 
ORELSE etac rev_subsetD 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 
by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

77 
(Abs_map_inverse RS subst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 
by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

79 
by (etac Abs_term_inverse 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

80 
by (etac rangeE 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
by (hyp_subst_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
by (resolve_tac prems 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
by (etac list.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 
by (etac CollectE 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 
by (stac Abs_map_CONS 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 
by (etac conjunct1 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

87 
by (etac rev_subsetD 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

88 
by (rtac list_subset_sexp 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

89 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

90 
by (ALLGOALS Fast_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

91 
qed "term_induct"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

92 

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

93 
(*Induction for the abstract type 'a term*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

94 
val prems = goal Term.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

95 
"[ !!x. R(App x Nil); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

96 
\ !!x t ts. R(App x ts) ==> R(App x (t#ts)) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 
\ ] ==> R(t)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

98 
by (rtac term_induct 1); (*types force good instantiation*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

99 
by (etac rev_mp 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

100 
by (rtac list_induct2 1); (*types force good instantiation*) 
4089  101 
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

102 
qed "term_induct2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

103 

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

104 
(*Perform induction on xs. *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

105 
fun term_ind2_tac a i = 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

106 
EVERY [res_inst_tac [("t",a)] term_induct2 i, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

107 
rename_last_tac a ["1","s"] (i+1)]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

108 

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

109 

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

110 

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

111 
(*** Term_rec  by wf recursion on pred_sexp ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

112 

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

114 
"(%M. Term_rec M d) = wfrec (trancl pred_sexp) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 
\ (%g. Split(%x y. d x y (Abs_map g y)))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

116 
by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

117 
bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

118 
((result() RS eq_reflection) RS def_wfrec)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

119 

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

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

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

122 
* val Term_rec_unfold = 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

123 
* wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

125 

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

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

127 

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

128 
val [prem] = goal Term.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

129 
"N: list(term(A)) ==> \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

130 
\ !M. (N,M): pred_sexp^+ > \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

131 
\ Abs_map (cut h (pred_sexp^+) M) N = \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
\ Abs_map h N"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

133 
by (rtac (prem RS list.induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

134 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

135 
by (strip_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

136 
by (etac (pred_sexp_CONS_D RS conjE) 1); 
4089  137 
by (asm_simp_tac (simpset() addsimps [trancl_pred_sexpD1]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

138 
qed "Abs_map_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 

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

140 
val [prem1,prem2,A_subset_sexp] = goal Term.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

141 
"[ M: sexp; N: list(term(A)); A<=sexp ] ==> \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5143
diff
changeset

142 
\ Term_rec (Scons M N) d = d M N (Abs_map (%Z. Term_rec Z d) N)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

143 
by (rtac (Term_rec_unfold RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

144 
by (simp_tac (HOL_ss addsimps 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

146 
prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

147 
prem1, prem2 RS rev_subsetD, list_subset_sexp, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

148 
term_subset_sexp, A_subset_sexp]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

149 
qed "Term_rec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

150 

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

151 
(*** term_rec  by Term_rec ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

152 

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

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

154 
val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

155 
[("f","Rep_term")] Rep_map_type; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

156 
val Rep_Tlist = Rep_term RS Rep_map_type1; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

157 
val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

158 

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

159 
(*Now avoids conditional rewriting with the premise N: list(term(A)), 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

160 
since A will be uninstantiated and will cause rewriting to fail. *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

161 
val term_rec_ss = HOL_ss 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

162 
addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse), 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

163 
Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

164 
inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

166 

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

167 
val term_rec = prove_goalw Term.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

168 
[term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

169 
"term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

170 
(fn _ => [simp_tac term_rec_ss 1]) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

171 

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

172 
end; 