src/HOL/Lambda/ListApplication.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 6128 2acc5d36610c
child 8935 548901d05a0e
permissions -rw-r--r--
expandshort
     1 (*  Title:      HOL/Lambda/ListApplication.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998 TU Muenchen
     5 *)
     6 
     7 Goal "(r$$ts = s$$ts) = (r = s)";
     8 by (rev_induct_tac "ts" 1);
     9 by (Auto_tac);
    10 qed "apps_eq_tail_conv";
    11 AddIffs [apps_eq_tail_conv];
    12 
    13 Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
    14 by (induct_tac "ss" 1);
    15 by (Auto_tac);
    16 qed_spec_mp "Var_eq_apps_conv";
    17 AddIffs [Var_eq_apps_conv];
    18 
    19 Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
    20 by (rev_induct_tac "rs" 1);
    21  by (Simp_tac 1);
    22  by (Blast_tac 1);
    23 by (rtac allI 1);
    24 by (rev_induct_tac "ss" 1);
    25 by (Auto_tac);
    26 qed_spec_mp "Var_apps_eq_Var_apps_conv";
    27 AddIffs [Var_apps_eq_Var_apps_conv];
    28 
    29 Goal "(r$s = t$$ts) = \
    30 \     (if ts = [] then r$s = t \
    31 \      else (? ss. ts = ss@[s] & r = t$$ss))";
    32 by (res_inst_tac [("xs","ts")] rev_exhaust 1);
    33 by (Auto_tac);
    34 qed "App_eq_foldl_conv";
    35 
    36 Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
    37 by (rev_induct_tac "ss" 1);
    38 by (Auto_tac);
    39 qed "Abs_eq_apps_conv";
    40 AddIffs [Abs_eq_apps_conv];
    41 
    42 Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
    43 by (rev_induct_tac "ss" 1);
    44 by (Auto_tac);
    45 qed "apps_eq_Abs_conv";
    46 AddIffs [apps_eq_Abs_conv];
    47 
    48 Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
    49 by (rev_induct_tac "rs" 1);
    50  by (Simp_tac 1);
    51  by (Blast_tac 1);
    52 by (rtac allI 1);
    53 by (rev_induct_tac "ss" 1);
    54 by (Auto_tac);
    55 qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
    56 AddIffs [Abs_apps_eq_Abs_apps_conv];
    57 
    58 Goal "!s t. Abs s $ t ~= (Var n)$$ss";
    59 by (rev_induct_tac "ss" 1);
    60 by (Auto_tac);
    61 qed_spec_mp "Abs_App_neq_Var_apps";
    62 AddIffs [Abs_App_neq_Var_apps];
    63 
    64 Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
    65 by (rev_induct_tac "ss" 1);
    66  by (Simp_tac 1);
    67 by (rtac allI 1);
    68 by (rev_induct_tac "ts" 1);
    69 by (Auto_tac);
    70 qed_spec_mp "Var_apps_neq_Abs_apps";
    71 AddIffs [Var_apps_neq_Abs_apps];
    72 
    73 Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
    74 by (induct_tac "t" 1);
    75   by (res_inst_tac[("x","[]")] exI 1);
    76   by (Simp_tac 1);
    77  by (Clarify_tac 1);
    78  by (rename_tac "ts1 ts2 h1 h2" 1);
    79  by (res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
    80  by (Simp_tac 1);
    81 by (Simp_tac 1);
    82 qed "ex_head_tail";
    83 
    84 Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
    85 by (rev_induct_tac "rs" 1);
    86 by (Auto_tac);
    87 qed "size_apps";
    88 Addsimps [size_apps];
    89 
    90 Goal "[| 0 < k; m <= n |] ==> m < n+k";
    91 by (fast_arith_tac 1);
    92 val lemma = result();
    93 
    94 (* a customized induction schema for $$ *)
    95 
    96 val prems = Goal
    97 "[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
    98 \   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
    99 \|] ==> !t. size t = n --> P t";
   100 by (res_inst_tac [("n","n")] less_induct 1);
   101 by (rtac allI 1);
   102 by (cut_inst_tac [("t","t")] ex_head_tail 1);
   103 by (Clarify_tac 1);
   104 by (etac disjE 1);
   105  by (Clarify_tac 1);
   106  by (resolve_tac prems 1);
   107  by (Clarify_tac 1);
   108  by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   109  by (Simp_tac 1);
   110  by (rtac lemma 1);
   111   by (Force_tac 1);
   112  by (rtac elem_le_sum 1);
   113  by (Force_tac 1);
   114 by (Clarify_tac 1);
   115 by (resolve_tac prems 1);
   116 by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   117 by (Simp_tac 1);
   118 by (Clarify_tac 1);
   119 by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   120 by (Simp_tac 1);
   121 by (rtac le_imp_less_Suc 1);
   122 by (rtac trans_le_add1 1);
   123 by (rtac trans_le_add2 1);
   124 by (rtac elem_le_sum 1);
   125 by (Force_tac 1);
   126 val lemma = result() RS spec RS mp;
   127 
   128 val prems = Goal
   129 "[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
   130 \   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
   131 \|] ==> P t";
   132 by (res_inst_tac [("x1","t")] lemma 1);
   133 by (rtac refl 3);
   134 by (REPEAT(ares_tac prems 1));
   135 qed "Apps_dB_induct";