src/HOL/Lambda/ListBeta.thy
author wenzelm
Wed, 01 Feb 2006 22:20:40 +0100
changeset 18888 3b643f81b378
parent 18513 791b53bf4073
child 19086 1b3780be6cc2
permissions -rw-r--r--
updated;
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
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12011
diff changeset
     9
theory ListBeta imports ListApplication ListOrder begin
9762
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
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    20
lemma head_Var_reduction:
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    21
  "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    22
  apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta)
9762
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_tac xs = rs in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    25
     apply simp
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    26
    apply (atomize, force intro: append_step1I)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    27
   apply (rule_tac xs = rs in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    28
    apply simp
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    29
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    30
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    31
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    32
lemma apps_betasE [elim!]:
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    33
  assumes major: "r \<degree>\<degree> rs -> s"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    34
    and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    35
      "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    36
      "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    37
  shows R
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    38
proof -
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    39
  from major have
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    40
   "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    41
    (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    42
    (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    43
    apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    44
       apply (case_tac r)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    45
         apply simp
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    46
        apply (simp add: App_eq_foldl_conv)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    47
        apply (split split_if_asm)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    48
         apply simp
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    49
         apply blast
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    50
        apply simp
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    51
       apply (simp add: App_eq_foldl_conv)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    52
       apply (split split_if_asm)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    53
        apply simp
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    54
       apply simp
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    55
      apply (drule App_eq_foldl_conv [THEN iffD1])
10653
55f33da63366 small mods.
nipkow
parents: 9941
diff changeset
    56
      apply (split split_if_asm)
9762
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 blast
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    59
      apply (force intro!: disjI1 [THEN append_step1I])
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    60
     apply (drule App_eq_foldl_conv [THEN iffD1])
10653
55f33da63366 small mods.
nipkow
parents: 9941
diff changeset
    61
     apply (split split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    62
      apply simp
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    63
      apply blast
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    64
     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    65
    done
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    66
  with cases show ?thesis by blast
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    67
qed
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    68
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    69
lemma apps_preserves_beta [simp]:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11639
diff changeset
    70
    "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    71
  by (induct ss rule: rev_induct) auto
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    72
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    73
lemma apps_preserves_beta2 [simp]:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11639
diff changeset
    74
    "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    75
  apply (induct set: rtrancl)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    76
   apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    77
  apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    78
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    79
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    80
lemma apps_preserves_betas [simp]:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    81
    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    82
  apply (induct rs fixing: ss rule: rev_induct)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    83
   apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    84
  apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    85
  apply (rule_tac xs = ss in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    86
   apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    87
  apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    88
  apply (drule Snoc_step1_SnocD)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    89
  apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    90
  done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
    91
11639
wenzelm
parents: 11549
diff changeset
    92
end