src/HOL/Induct/Term.ML
author berghofe
Fri, 24 Jul 1998 13:39:47 +0200
changeset 5191 8ceaa19f7717
parent 5143 b94cd208f073
child 5223 4cb05273f764
permissions -rw-r--r--
Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    14
Goal "term(A) = A <*> list(term(A))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    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 well-founded sets **)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    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
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    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
b55686a7b22c fixed dots;
wenzelm
parents: 3649
diff changeset
    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
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   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
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
   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
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   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;