src/HOL/Lambda/ListApplication.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11549 e7265e70fd7c
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/Lambda/ListApplication.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998 TU Muenchen
     5 *)
     6 
     7 header {* Application of a term to a list of terms *}
     8 
     9 theory ListApplication = Lambda:
    10 
    11 syntax
    12   "_list_application" :: "dB => dB list => dB"   (infixl "$$" 150)
    13 translations
    14   "t $$ ts" == "foldl (op $) t ts"
    15 
    16 lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
    17   apply (induct_tac ts rule: rev_induct)
    18    apply auto
    19   done
    20 
    21 lemma Var_eq_apps_conv [rule_format, iff]:
    22     "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
    23   apply (induct_tac ss)
    24    apply auto
    25   done
    26 
    27 lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
    28     "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
    29   apply (induct_tac rs rule: rev_induct)
    30    apply simp
    31    apply blast
    32   apply (rule allI)
    33   apply (induct_tac ss rule: rev_induct)
    34    apply auto
    35   done
    36 
    37 lemma App_eq_foldl_conv:
    38   "(r $ s = t $$ ts) =
    39     (if ts = [] then r $ s = t
    40     else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
    41   apply (rule_tac xs = ts in rev_exhaust)
    42    apply auto
    43   done
    44 
    45 lemma Abs_eq_apps_conv [iff]:
    46     "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
    47   apply (induct_tac ss rule: rev_induct)
    48    apply auto
    49   done
    50 
    51 lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
    52   apply (induct_tac ss rule: rev_induct)
    53    apply auto
    54   done
    55 
    56 lemma Abs_apps_eq_Abs_apps_conv [iff]:
    57     "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
    58   apply (induct_tac rs rule: rev_induct)
    59    apply simp
    60    apply blast
    61   apply (rule allI)
    62   apply (induct_tac ss rule: rev_induct)
    63    apply auto
    64   done
    65 
    66 lemma Abs_App_neq_Var_apps [iff]:
    67     "\<forall>s t. Abs s $ t ~= Var n $$ ss"
    68   apply (induct_tac ss rule: rev_induct)
    69    apply auto
    70   done
    71 
    72 lemma Var_apps_neq_Abs_apps [rule_format, iff]:
    73     "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
    74   apply (induct_tac ss rule: rev_induct)
    75    apply simp
    76   apply (rule allI)
    77   apply (induct_tac ts rule: rev_induct)
    78    apply auto
    79   done
    80 
    81 lemma ex_head_tail:
    82   "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
    83   apply (induct_tac t)
    84     apply (rule_tac x = "[]" in exI)
    85     apply simp
    86    apply clarify
    87    apply (rename_tac ts1 ts2 h1 h2)
    88    apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
    89    apply simp
    90   apply simp
    91   done
    92 
    93 lemma size_apps [simp]:
    94   "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
    95   apply (induct_tac rs rule: rev_induct)
    96    apply auto
    97   done
    98 
    99 lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
   100   apply simp
   101   done
   102 
   103 
   104 text {* \medskip A customized induction schema for @{text "$$"}. *}
   105 
   106 lemma lem [rule_format (no_asm)]:
   107   "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   108     !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   109   |] ==> \<forall>t. size t = n --> P t"
   110 proof -
   111   case antecedent
   112   show ?thesis
   113    apply (induct_tac n rule: nat_less_induct)
   114    apply (rule allI)
   115    apply (cut_tac t = t in ex_head_tail)
   116    apply clarify
   117    apply (erule disjE)
   118     apply clarify
   119     apply (rule prems)
   120     apply clarify
   121     apply (erule allE, erule impE)
   122       prefer 2
   123       apply (erule allE, erule mp, rule refl)
   124      apply simp
   125      apply (rule lem0)
   126       apply force
   127      apply (rule elem_le_sum)
   128      apply force
   129     apply clarify
   130     apply (rule prems)
   131      apply (erule allE, erule impE)
   132       prefer 2
   133       apply (erule allE, erule mp, rule refl)
   134      apply simp
   135     apply clarify
   136     apply (erule allE, erule impE)
   137      prefer 2
   138      apply (erule allE, erule mp, rule refl)
   139     apply simp
   140     apply (rule le_imp_less_Suc)
   141     apply (rule trans_le_add1)
   142     apply (rule trans_le_add2)
   143     apply (rule elem_le_sum)
   144     apply force
   145     done
   146 qed
   147 
   148 theorem Apps_dB_induct:
   149   "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   150     !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   151   |] ==> P t"
   152 proof -
   153   case antecedent
   154   show ?thesis
   155     apply (rule_tac t = t in lem)
   156       prefer 3
   157       apply (rule refl)
   158      apply (assumption | rule prems)+
   159     done
   160 qed
   161 
   162 end