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