src/HOL/Proofs/Lambda/StrongNorm.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 50336 1d9a31b58053
child 58622 aa99568f56de
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: 33640
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/StrongNorm.thy
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     3
    Copyright   2000 TU Muenchen
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     4
*)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     5
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     6
header {* Strong normalization for simply-typed lambda calculus *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     7
50336
1d9a31b58053 renamed "Type.thy" to something that's less likely to cause conflicts
blanchet
parents: 50241
diff changeset
     8
theory StrongNorm imports LambdaType InductTermi begin
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
     9
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    10
text {*
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    11
Formalization by Stefan Berghofer. Partly based on a paper proof by
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    12
Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    13
*}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    14
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    15
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    16
subsection {* Properties of @{text IT} *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    17
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    18
lemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 18257
diff changeset
    19
  apply (induct arbitrary: i set: IT)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    20
    apply (simp (no_asm))
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    21
    apply (rule conjI)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    22
     apply
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    23
      (rule impI,
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    24
       rule IT.Var,
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    25
       erule listsp.induct,
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    26
       simp (no_asm),
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    27
       simp (no_asm),
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    28
       rule listsp.Cons,
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    29
       blast,
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    30
       assumption)+
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    31
     apply auto
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    32
   done
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    33
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    34
lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    35
  by (induct ts) auto
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    36
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    37
lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 18257
diff changeset
    38
  apply (induct arbitrary: i j set: IT)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    39
    txt {* Case @{term Var}: *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    40
    apply (simp (no_asm) add: subst_Var)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    41
    apply
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    42
    ((rule conjI impI)+,
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    43
      rule IT.Var,
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    44
      erule listsp.induct,
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    45
      simp (no_asm),
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    46
      simp (no_asm),
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    47
      rule listsp.Cons,
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    48
      fast,
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    49
      assumption)+
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    50
   txt {* Case @{term Lambda}: *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    51
   apply atomize
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    52
   apply simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    53
   apply (rule IT.Lambda)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    54
   apply fast
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    55
  txt {* Case @{term Beta}: *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    56
  apply atomize
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    57
  apply (simp (no_asm_use) add: subst_subst [symmetric])
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    58
  apply (rule IT.Beta)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    59
   apply auto
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    60
  done
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    61
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    62
lemma Var_IT: "IT (Var n)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    63
  apply (subgoal_tac "IT (Var n \<degree>\<degree> [])")
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    64
   apply simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    65
  apply (rule IT.Var)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    66
  apply (rule listsp.Nil)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    67
  done
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    68
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    69
lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    70
  apply (induct set: IT)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    71
    apply (subst app_last)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    72
    apply (rule IT.Var)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    73
    apply simp
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    74
    apply (rule listsp.Cons)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    75
     apply (rule Var_IT)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    76
    apply (rule listsp.Nil)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    77
   apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    78
    apply (erule subst_Var_IT)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    79
   apply (rule Var_IT)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    80
  apply (subst app_last)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    81
  apply (rule IT.Beta)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    82
   apply (subst app_last [symmetric])
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    83
   apply assumption
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    84
  apply assumption
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    85
  done
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    86
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    87
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    88
subsection {* Well-typed substitution preserves termination *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    89
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    90
lemma subst_type_IT:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    91
  "\<And>t e T u i. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    92
    IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    93
  (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    94
proof (induct U)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    95
  fix T t
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    96
  assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    97
  assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    98
  assume "IT t"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
    99
  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   100
  proof induct
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   101
    fix e T' u i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   102
    assume uIT: "IT u"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   103
    assume uT: "e \<turnstile> u : T"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   104
    {
50241
8b0fdeeefef7 eliminated some improper identifiers;
wenzelm
parents: 44890
diff changeset
   105
      case (Var rs n e1 T'1 u1 i1)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   106
      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   107
      let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   108
      let ?R = "\<lambda>t. \<forall>e T' u i.
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   109
        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   110
      show "IT ((Var n \<degree>\<degree> rs)[u/i])"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   111
      proof (cases "n = i")
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   112
        case True
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   113
        show ?thesis
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   114
        proof (cases rs)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   115
          case Nil
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   116
          with uIT True show ?thesis by simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   117
        next
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   118
          case (Cons a as)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   119
          with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   120
          then obtain Ts
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   121
              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   122
              and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   123
            by (rule list_app_typeE)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   124
          from headT obtain T''
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   125
              where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   126
              and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   127
            by cases simp_all
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   128
          from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   129
            by cases auto
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   130
          with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   131
          from T have "IT ((Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   132
            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   133
          proof (rule MI2)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   134
            from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   135
            proof (rule MI1)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   136
              have "IT (lift u 0)" by (rule lift_IT [OF uIT])
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   137
              thus "IT (lift u 0 \<degree> Var 0)" by (rule app_Var_IT)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   138
              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   139
              proof (rule typing.App)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   140
                show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   141
                  by (rule lift_type) (rule uT')
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   142
                show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   143
                  by (rule typing.Var) simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   144
              qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   145
              from Var have "?R a" by cases (simp_all add: Cons)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   146
              with argT uIT uT show "IT (a[u/i])" by simp
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   147
              from argT uT show "e \<turnstile> a[u/i] : T''"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   148
                by (rule subst_lemma) simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   149
            qed
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   150
            thus "IT (u \<degree> a[u/i])" by simp
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   151
            from Var have "listsp ?R as"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   152
              by cases (simp_all add: Cons)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   153
            moreover from argsT have "listsp ?ty as"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   154
              by (rule lists_typings)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   155
            ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) as"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   156
              by simp
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   157
            hence "listsp IT (map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as))"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   158
              (is "listsp IT (?ls as)")
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   159
            proof induct
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   160
              case Nil
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39613
diff changeset
   161
              show ?case by fastforce
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   162
            next
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   163
              case (Cons b bs)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   164
              hence I: "?R b" by simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   165
              from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   166
              with uT uIT I have "IT (b[u/i])" by simp
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   167
              hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   168
              hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   169
                by (rule listsp.Cons) (rule Cons)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   170
              thus ?case by simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   171
            qed
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   172
            thus "IT (Var 0 \<degree>\<degree> ?ls as)" by (rule IT.Var)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   173
            have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   174
              by (rule typing.Var) simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   175
            moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   176
              by (rule substs_lemma)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   177
            hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   178
              by (rule lift_types)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   179
            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   180
              by (rule list_app_typeI)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   181
            from argT uT have "e \<turnstile> a[u/i] : T''"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   182
              by (rule subst_lemma) (rule refl)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   183
            with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   184
              by (rule typing.App)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   185
          qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   186
          with Cons True show ?thesis
33640
0d82107dc07a Remove map_compose, replaced by map_map
hoelzl
parents: 32960
diff changeset
   187
            by (simp add: comp_def)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   188
        qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   189
      next
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   190
        case False
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   191
        from Var have "listsp ?R rs" by simp
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   192
        moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   193
          by (rule list_app_typeE)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   194
        hence "listsp ?ty rs" by (rule lists_typings)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   195
        ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) rs"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   196
          by simp
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   197
        hence "listsp IT (map (\<lambda>x. x[u/i]) rs)"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   198
        proof induct
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   199
          case Nil
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39613
diff changeset
   200
          show ?case by fastforce
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   201
        next
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   202
          case (Cons a as)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   203
          hence I: "?R a" by simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   204
          from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   205
          with uT uIT I have "IT (a[u/i])" by simp
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   206
          hence "listsp IT (a[u/i] # map (\<lambda>t. t[u/i]) as)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   207
            by (rule listsp.Cons) (rule Cons)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   208
          thus ?case by simp
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   209
        qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   210
        with False show ?thesis by (auto simp add: subst_Var)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   211
      qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   212
    next
50241
8b0fdeeefef7 eliminated some improper identifiers;
wenzelm
parents: 44890
diff changeset
   213
      case (Lambda r e1 T'1 u1 i1)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   214
      assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   215
        and "\<And>e T' u i. PROP ?Q r e T' u i T"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   216
      with uIT uT show "IT (Abs r[u/i])"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39613
diff changeset
   217
        by fastforce
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   218
    next
50241
8b0fdeeefef7 eliminated some improper identifiers;
wenzelm
parents: 44890
diff changeset
   219
      case (Beta r a as e1 T'1 u1 i1)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   220
      assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   221
      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   222
      assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   223
      have "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   224
      proof (rule IT.Beta)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   225
        have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> r[a/0] \<degree>\<degree> as"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   226
          by (rule apps_preserves_beta) (rule beta.beta)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   227
        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   228
          by (rule subject_reduction)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   229
        hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23750
diff changeset
   230
          using uIT uT by (rule SI1)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   231
        thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   232
          by (simp del: subst_map add: subst_subst subst_map [symmetric])
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   233
        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   234
          by (rule list_app_typeE) fast
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   235
        then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   236
        thus "IT (a[u/i])" using uIT uT by (rule SI2)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   237
      qed
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   238
      thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   239
    }
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   240
  qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   241
qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   242
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   243
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   244
subsection {* Well-typed terms are strongly normalizing *}
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   245
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   246
lemma type_implies_IT:
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   247
  assumes "e \<turnstile> t : T"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   248
  shows "IT t"
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   249
  using assms
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   250
proof induct
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   251
  case Var
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   252
  show ?case by (rule Var_IT)
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   253
next
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   254
  case Abs
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   255
  show ?case by (rule IT.Lambda) (rule Abs)
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   256
next
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   257
  case (App e s T U t)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   258
  have "IT ((Var 0 \<degree> lift t 0)[s/0])"
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   259
  proof (rule subst_type_IT)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   260
    have "IT (lift t 0)" using `IT t` by (rule lift_IT)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   261
    hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   262
    hence "IT (Var 0 \<degree>\<degree> [lift t 0])" by (rule IT.Var)
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   263
    also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   264
    finally show "IT \<dots>" .
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   265
    have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   266
      by (rule typing.Var) simp
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   267
    moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   268
      by (rule lift_type) (rule App.hyps)
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   269
    ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   270
      by (rule typing.App)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   271
    show "IT s" by fact
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   272
    show "e \<turnstile> s : T \<Rightarrow> U" by fact
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   273
  qed
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   274
  thus ?case by simp
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   275
qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   276
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   277
theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t"
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   278
proof -
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   279
  assume "e \<turnstile> t : T"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   280
  hence "IT t" by (rule type_implies_IT)
14064
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   281
  thus ?thesis by (rule IT_implies_termi)
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   282
qed
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   283
35d36f43ba06 Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
diff changeset
   284
end