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