src/HOL/Proofs/Lambda/ListBeta.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 39157 b98909faaea8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 36862
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/ListBeta.thy
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     3
    Copyright   1998 TU Muenchen
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     4
*)
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     5
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     6
header {* Lifting beta-reduction to lists *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12011
diff changeset
     8
theory ListBeta imports ListApplication ListOrder begin
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
     9
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    10
text {*
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    11
  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
    12
*}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    13
19363
667b5ea637dd refined 'abbreviation';
wenzelm
parents: 19086
diff changeset
    14
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20503
diff changeset
    15
  list_beta :: "dB list => dB list => bool"  (infixl "=>" 50) where
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    16
  "rs => ss == step1 beta rs ss"
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    17
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    18
lemma head_Var_reduction:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    19
  "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    20
  apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    21
     apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    22
    apply (rule_tac xs = rs in rev_exhaust)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    23
     apply simp
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    24
    apply (atomize, force intro: append_step1I)
9762
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
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    27
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    28
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    29
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    30
lemma apps_betasE [elim!]:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    31
  assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    32
    and cases: "!!r'. [| r \<rightarrow>\<^sub>\<beta> r'; s = r' \<degree>\<degree> rs |] ==> R"
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    33
      "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    34
      "!!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
    35
  shows R
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    36
proof -
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    37
  from major have
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    38
   "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    39
    (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    40
    (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    41
    apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    42
       apply (case_tac r)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    43
         apply simp
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    44
        apply (simp add: App_eq_foldl_conv)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    45
        apply (split split_if_asm)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    46
         apply simp
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    47
         apply blast
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    48
        apply simp
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    49
       apply (simp add: App_eq_foldl_conv)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    50
       apply (split split_if_asm)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    51
        apply simp
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    52
       apply simp
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    53
      apply (drule App_eq_foldl_conv [THEN iffD1])
10653
55f33da63366 small mods.
nipkow
parents: 9941
diff changeset
    54
      apply (split split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    55
       apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    56
       apply blast
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    57
      apply (force intro!: disjI1 [THEN append_step1I])
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    58
     apply (drule App_eq_foldl_conv [THEN iffD1])
10653
55f33da63366 small mods.
nipkow
parents: 9941
diff changeset
    59
     apply (split split_if_asm)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    60
      apply simp
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    61
      apply blast
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    62
     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    63
    done
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    64
  with cases show ?thesis by blast
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    65
qed
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    66
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    67
lemma apps_preserves_beta [simp]:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    68
    "r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    69
  by (induct ss rule: rev_induct) auto
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    70
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    71
lemma apps_preserves_beta2 [simp]:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11639
diff changeset
    72
    "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    73
  apply (induct set: rtranclp)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    74
   apply blast
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    75
  apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    76
  done
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    77
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    78
lemma apps_preserves_betas [simp]:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    79
    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    80
  apply (induct rs arbitrary: ss rule: rev_induct)
9762
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    81
   apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    82
  apply simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    83
  apply (rule_tac xs = ss in rev_exhaust)
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 simp
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    86
  apply (drule Snoc_step1_SnocD)
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    87
  apply blast
66f7eefb3967 ported HOL/Lambda/ListBeta;
wenzelm
parents: 5261
diff changeset
    88
  done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
    89
11639
wenzelm
parents: 11549
diff changeset
    90
end