src/HOL/Lambda/ListBeta.thy
author wenzelm
Mon, 04 Sep 2000 11:21:24 +0200
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9906 5c027cca6262
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Lambda/ListBeta.thy
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     4
    Copyright   1998 TU Muenchen
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     5
*)
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     6
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     7
header {* Lifting beta-reduction to lists *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     8
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
     9
theory ListBeta = ListApplication + ListOrder:
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    10
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    11
text {*
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    12
  Lifting beta-reduction to lists of terms, reducing exactly one element.
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    13
*}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    14
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    15
syntax
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    16
  "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    17
translations
9827
wenzelm
parents: 9811
diff changeset
    18
  "rs => ss" == "(rs, ss) : step1 beta"
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    19
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    20
lemma head_Var_reduction_aux:
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    21
  "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    22
  apply (erule beta.induct)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    23
     apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    24
    apply (rule allI)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    25
    apply (rule_tac xs = rs in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    26
     apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    27
    apply (force intro: append_step1I)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    28
   apply (rule allI)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    29
   apply (rule_tac xs = rs in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    30
    apply simp
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    31
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    32
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    33
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    34
lemma head_Var_reduction:
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    35
  "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    36
  apply (drule head_Var_reduction_aux)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    37
  apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    38
  done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
    39
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    40
lemma apps_betasE_aux:
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    41
  "u -> u' ==> \<forall>r rs. u = r $$ rs -->
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    42
    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    43
     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    44
     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    45
  apply (erule beta.induct)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    46
     apply (clarify del: disjCI)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    47
     apply (case_tac r)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    48
       apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    49
      apply (simp add: App_eq_foldl_conv)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    50
      apply (split (asm) split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    51
       apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    52
       apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    53
      apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    54
     apply (simp add: App_eq_foldl_conv)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    55
     apply (split (asm) split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    56
      apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    57
     apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    58
    apply (clarify del: disjCI)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    59
    apply (drule App_eq_foldl_conv [THEN iffD1])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    60
    apply (split (asm) split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    61
     apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    62
     apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    63
    apply (force intro: disjI1 [THEN append_step1I])
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    64
   apply (clarify del: disjCI)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    65
   apply (drule App_eq_foldl_conv [THEN iffD1])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    66
   apply (split (asm) split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    67
    apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    68
    apply blast
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    69
   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    70
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    71
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    72
lemma apps_betasE [elim!]:
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    73
  "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    74
    !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    75
    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    76
  ==> R"
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    77
proof -
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    78
  assume major: "r $$ rs -> s"
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    79
  case antecedent
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    80
  show ?thesis
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    81
    apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    82
    apply (assumption | rule refl | erule prems exE conjE impE disjE)+
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    83
    done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    84
qed
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    85
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    86
lemma apps_preserves_beta [simp]:
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    87
    "r -> s ==> r $$ ss -> s $$ ss"
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    88
  apply (induct_tac ss rule: rev_induct)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    89
  apply auto
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    90
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    91
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    92
lemma apps_preserves_beta2 [simp]:
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    93
    "r ->> s ==> r $$ ss ->> s $$ ss"
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    94
  apply (erule rtrancl_induct)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    95
   apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    96
  apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    97
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    98
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    99
lemma apps_preserves_betas [rulify, simp]:
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
   100
    "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   101
  apply (induct_tac rs rule: rev_induct)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   102
   apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   103
  apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   104
  apply clarify
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   105
  apply (rule_tac xs = ss in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   106
   apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   107
  apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   108
  apply (drule Snoc_step1_SnocD)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   109
  apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
   110
  done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
   111
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
   112
end