src/HOL/Induct/Term.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5738 0d8698c15439
permissions -rw-r--r--
even more tidying of Goal commands
paulson@3120
     1
(*  Title:      HOL/ex/Term
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120
     4
    Copyright   1992  University of Cambridge
paulson@3120
     5
paulson@3120
     6
Terms over a given alphabet -- function applications; illustrates list functor
paulson@3120
     7
  (essentially the same type as in Trees & Forests)
paulson@3120
     8
*)
paulson@3120
     9
paulson@5223
    10
(** Monotonicity and unfolding of the function **)
paulson@3120
    11
wenzelm@5069
    12
Goal "term(A) = A <*> list(term(A))";
wenzelm@4089
    13
by (fast_tac (claset() addSIs term.intrs
paulson@3120
    14
                      addEs [term.elim]) 1);
paulson@3120
    15
qed "term_unfold";
paulson@3120
    16
paulson@3120
    17
(*This justifies using term in other recursive type definitions*)
paulson@5143
    18
Goalw term.defs "A<=B ==> term(A) <= term(B)";
paulson@3120
    19
by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
paulson@3120
    20
qed "term_mono";
paulson@3120
    21
paulson@3120
    22
(** Type checking -- term creates well-founded sets **)
paulson@3120
    23
wenzelm@5069
    24
Goalw term.defs "term(sexp) <= sexp";
paulson@3120
    25
by (rtac lfp_lowerbound 1);
wenzelm@4089
    26
by (fast_tac (claset() addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
paulson@3120
    27
qed "term_sexp";
paulson@3120
    28
paulson@3120
    29
(* A <= sexp ==> term(A) <= sexp *)
paulson@3120
    30
bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
paulson@3120
    31
paulson@3120
    32
paulson@3120
    33
(** Elimination -- structural induction on the set term(A) **)
paulson@3120
    34
paulson@3120
    35
(*Induction for the set term(A) *)
paulson@3120
    36
val [major,minor] = goal Term.thy 
paulson@3120
    37
    "[| M: term(A);  \
wenzelm@3842
    38
\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x. R(x)}) \
berghofe@5191
    39
\               |] ==> R (Scons x zs)  \
paulson@3120
    40
\    |] ==> R(M)";
paulson@3120
    41
by (rtac (major RS term.induct) 1);
paulson@3120
    42
by (REPEAT (eresolve_tac ([minor] @
paulson@3120
    43
                ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
paulson@3120
    44
(*Proof could also use  mono_Int RS subsetD RS IntE *)
paulson@3120
    45
qed "Term_induct";
paulson@3120
    46
paulson@3120
    47
(*Induction on term(A) followed by induction on list *)
paulson@3120
    48
val major::prems = goal Term.thy
paulson@3120
    49
    "[| M: term(A);  \
berghofe@5191
    50
\       !!x.      [| x: A |] ==> R (Scons x NIL);  \
berghofe@5191
    51
\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R (Scons x zs)  \
berghofe@5191
    52
\                 |] ==> R (Scons x (CONS z zs))  \
paulson@3120
    53
\    |] ==> R(M)";
paulson@3120
    54
by (rtac (major RS Term_induct) 1);
paulson@3120
    55
by (etac list.induct 1);
paulson@3120
    56
by (REPEAT (ares_tac prems 1));
paulson@3120
    57
qed "Term_induct2";
paulson@3120
    58
paulson@3120
    59
(*** Structural Induction on the abstract type 'a term ***)
paulson@3120
    60
paulson@3120
    61
val Rep_term_in_sexp =
paulson@3120
    62
    Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
paulson@3120
    63
paulson@3120
    64
(*Induction for the abstract type 'a term*)
paulson@3120
    65
val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
paulson@3649
    66
    "[| !!x ts. (ALL t: set ts. R t) ==> R(App x ts)  \
paulson@3120
    67
\    |] ==> R(t)";
paulson@3120
    68
by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
paulson@3120
    69
by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
paulson@3120
    70
by (rtac (Rep_term RS Term_induct) 1);
paulson@3120
    71
by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
paulson@3120
    72
    list_subset_sexp, range_Leaf_subset_sexp] 1
paulson@3120
    73
     ORELSE etac rev_subsetD 1));
paulson@3120
    74
by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
paulson@3120
    75
        (Abs_map_inverse RS subst) 1);
paulson@3120
    76
by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
paulson@3120
    77
by (etac Abs_term_inverse 1);
paulson@3120
    78
by (etac rangeE 1);
paulson@3120
    79
by (hyp_subst_tac 1);
paulson@3120
    80
by (resolve_tac prems 1);
paulson@3120
    81
by (etac list.induct 1);
paulson@3120
    82
by (etac CollectE 2);
paulson@3120
    83
by (stac Abs_map_CONS 2);
paulson@3120
    84
by (etac conjunct1 2);
paulson@3120
    85
by (etac rev_subsetD 2);
paulson@3120
    86
by (rtac list_subset_sexp 2);
paulson@3120
    87
by (ALLGOALS Asm_simp_tac);
paulson@3120
    88
by (ALLGOALS Fast_tac);
paulson@3120
    89
qed "term_induct";
paulson@3120
    90
paulson@3120
    91
(*Induction for the abstract type 'a term*)
paulson@3120
    92
val prems = goal Term.thy 
paulson@3120
    93
    "[| !!x. R(App x Nil);  \
paulson@3120
    94
\       !!x t ts. R(App x ts) ==> R(App x (t#ts))  \
paulson@3120
    95
\    |] ==> R(t)";
paulson@3120
    96
by (rtac term_induct 1);  (*types force good instantiation*)
paulson@3120
    97
by (etac rev_mp 1);
paulson@3120
    98
by (rtac list_induct2 1);  (*types force good instantiation*)
wenzelm@4089
    99
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
paulson@3120
   100
qed "term_induct2";
paulson@3120
   101
paulson@3120
   102
(*Perform induction on xs. *)
paulson@3120
   103
fun term_ind2_tac a i = 
paulson@3120
   104
    EVERY [res_inst_tac [("t",a)] term_induct2 i,
paulson@3120
   105
           rename_last_tac a ["1","s"] (i+1)];
paulson@3120
   106
paulson@3120
   107
paulson@3120
   108
paulson@3120
   109
(*** Term_rec -- by wf recursion on pred_sexp ***)
paulson@3120
   110
paulson@5278
   111
Goal "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
paulson@3120
   112
                             \ (%g. Split(%x y. d x y (Abs_map g y)))";
paulson@3120
   113
by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
paulson@3120
   114
bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
paulson@3120
   115
                            ((result() RS eq_reflection) RS def_wfrec));
paulson@3120
   116
paulson@3120
   117
(*---------------------------------------------------------------------------
paulson@3120
   118
 * Old:
paulson@3120
   119
 * val Term_rec_unfold =
paulson@3120
   120
 *     wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
paulson@3120
   121
 *---------------------------------------------------------------------------*)
paulson@3120
   122
paulson@3120
   123
(** conversion rules **)
paulson@3120
   124
paulson@3120
   125
val [prem] = goal Term.thy
paulson@3120
   126
    "N: list(term(A)) ==>  \
paulson@3120
   127
\    !M. (N,M): pred_sexp^+ --> \
paulson@3120
   128
\        Abs_map (cut h (pred_sexp^+) M) N = \
paulson@3120
   129
\        Abs_map h N";
paulson@3120
   130
by (rtac (prem RS list.induct) 1);
paulson@3120
   131
by (Simp_tac 1);
paulson@3120
   132
by (strip_tac 1);
paulson@3120
   133
by (etac (pred_sexp_CONS_D RS conjE) 1);
wenzelm@4089
   134
by (asm_simp_tac (simpset() addsimps [trancl_pred_sexpD1]) 1);
paulson@3120
   135
qed "Abs_map_lemma";
paulson@3120
   136
paulson@3120
   137
val [prem1,prem2,A_subset_sexp] = goal Term.thy
paulson@3120
   138
    "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
berghofe@5191
   139
\    Term_rec (Scons M N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
paulson@3120
   140
by (rtac (Term_rec_unfold RS trans) 1);
paulson@3120
   141
by (simp_tac (HOL_ss addsimps
paulson@3120
   142
      [Split,
paulson@3120
   143
       prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
paulson@3120
   144
       prem1, prem2 RS rev_subsetD, list_subset_sexp,
paulson@3120
   145
       term_subset_sexp, A_subset_sexp]) 1);
paulson@3120
   146
qed "Term_rec";
paulson@3120
   147
paulson@3120
   148
(*** term_rec -- by Term_rec ***)
paulson@3120
   149
paulson@3120
   150
local
paulson@3120
   151
  val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
paulson@3120
   152
                        [("f","Rep_term")] Rep_map_type;
paulson@3120
   153
  val Rep_Tlist = Rep_term RS Rep_map_type1;
paulson@3120
   154
  val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
paulson@3120
   155
paulson@3120
   156
  (*Now avoids conditional rewriting with the premise N: list(term(A)),
paulson@3120
   157
    since A will be uninstantiated and will cause rewriting to fail. *)
paulson@3120
   158
  val term_rec_ss = HOL_ss
paulson@3120
   159
      addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
paulson@3120
   160
                Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
paulson@3120
   161
                inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
paulson@3120
   162
in
paulson@3120
   163
paulson@3120
   164
val term_rec = prove_goalw Term.thy
paulson@3120
   165
         [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
paulson@3120
   166
    "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)"
paulson@3120
   167
 (fn _ => [simp_tac term_rec_ss 1])
paulson@3120
   168
paulson@3120
   169
end;