src/HOL/Proofs/Lambda/NormalForm.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 45605 a89b4bc311a5
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: 33704
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/NormalForm.thy
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen, 2003
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     3
*)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     4
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     5
header {* Inductive characterization of lambda terms in normal form *}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     6
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     7
theory NormalForm
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     8
imports ListBeta
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
     9
begin
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    10
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    11
subsection {* Terms in normal form *}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    12
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    13
definition
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    14
  listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    15
  "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    16
33704
6aeb8454efc1 add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
wenzelm
parents: 32960
diff changeset
    17
declare listall_def [extraction_expand_def]
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    18
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    19
theorem listall_nil: "listall P []"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    20
  by (simp add: listall_def)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    21
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    22
theorem listall_nil_eq [simp]: "listall P [] = True"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    23
  by (iprover intro: listall_nil)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    24
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    25
theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    26
  apply (simp add: listall_def)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    27
  apply (rule allI impI)+
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    28
  apply (case_tac i)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    29
  apply simp+
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    30
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    31
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    32
theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \<and> listall P xs)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    33
  apply (rule iffI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    34
  prefer 2
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    35
  apply (erule conjE)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    36
  apply (erule listall_cons)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    37
  apply assumption
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    38
  apply (unfold listall_def)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    39
  apply (rule conjI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    40
  apply (erule_tac x=0 in allE)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    41
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    42
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    43
  apply (rule allI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    44
  apply (erule_tac x="Suc i" in allE)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    45
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    46
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    47
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    48
lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    49
  by (induct xs) simp_all
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    50
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    51
lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    52
  by (induct xs) simp_all
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    53
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    54
lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    55
  apply (induct xs)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    56
   apply (rule iffI, simp, simp)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    57
  apply (rule iffI, simp, simp)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    58
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    59
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    60
lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    61
  apply (rule iffI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    62
  apply (simp add: listall_app)+
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    63
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    64
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    65
lemma listall_cong [cong, extraction_expand]:
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    66
  "xs = ys \<Longrightarrow> listall P xs = listall P ys"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    67
  -- {* Currently needed for strange technical reasons *}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    68
  by (unfold listall_def) simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    69
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    70
text {*
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    71
@{term "listsp"} is equivalent to @{term "listall"}, but cannot be
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    72
used for program extraction.
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    73
*}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    74
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    75
lemma listall_listsp_eq: "listall P xs = listsp P xs"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    76
  by (induct xs) (auto intro: listsp.intros)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    77
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    78
inductive NF :: "dB \<Rightarrow> bool"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    79
where
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    80
  App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    81
| Abs: "NF t \<Longrightarrow> NF (Abs t)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    82
monos listall_def
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    83
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    84
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    85
  apply (induct m)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    86
  apply (case_tac n)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    87
  apply (case_tac [3] n)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    88
  apply (simp only: nat.simps, iprover?)+
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    89
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    90
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    91
lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    92
  apply (induct m)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    93
  apply (case_tac n)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    94
  apply (case_tac [3] n)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    95
  apply (simp del: simp_thms, iprover?)+
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    96
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    97
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    98
lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
    99
  shows "listall NF ts" using NF
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   100
  by cases simp_all
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   101
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   102
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   103
subsection {* Properties of @{text NF} *}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   104
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   105
lemma Var_NF: "NF (Var n)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   106
  apply (subgoal_tac "NF (Var n \<degree>\<degree> [])")
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   107
   apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   108
  apply (rule NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   109
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   110
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   111
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   112
lemma Abs_NF:
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   113
  assumes NF: "NF (Abs t \<degree>\<degree> ts)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   114
  shows "ts = []" using NF
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   115
proof cases
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   116
  case (App us i)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   117
  thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym])
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   118
next
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   119
  case (Abs u)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   120
  thus ?thesis by simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   121
qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   122
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   123
lemma subst_terms_NF: "listall NF ts \<Longrightarrow>
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   124
    listall (\<lambda>t. \<forall>i j. NF (t[Var i/j])) ts \<Longrightarrow>
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   125
    listall NF (map (\<lambda>t. t[Var i/j]) ts)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   126
  by (induct ts) simp_all
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   127
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   128
lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   129
  apply (induct arbitrary: i j set: NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   130
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   131
  apply (frule listall_conj1)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   132
  apply (drule listall_conj2)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   133
  apply (drule_tac i=i and j=j in subst_terms_NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   134
  apply assumption
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39157
diff changeset
   135
  apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   136
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   137
  apply (erule NF.App)
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39157
diff changeset
   138
  apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   139
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   140
  apply (iprover intro: NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   141
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   142
  apply (iprover intro: NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   143
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   144
  apply (iprover intro: NF.Abs)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   145
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   146
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   147
lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   148
  apply (induct set: NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   149
  apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   150
  apply (rule exI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   151
  apply (rule conjI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   152
  apply (rule rtranclp.rtrancl_refl)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   153
  apply (rule NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   154
  apply (drule listall_conj1)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   155
  apply (simp add: listall_app)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   156
  apply (rule Var_NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   157
  apply (rule exI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   158
  apply (rule conjI)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   159
  apply (rule rtranclp.rtrancl_into_rtrancl)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   160
  apply (rule rtranclp.rtrancl_refl)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   161
  apply (rule beta)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   162
  apply (erule subst_Var_NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   163
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   164
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   165
lemma lift_terms_NF: "listall NF ts \<Longrightarrow>
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   166
    listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow>
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   167
    listall NF (map (\<lambda>t. lift t i) ts)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   168
  by (induct ts) simp_all
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   169
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   170
lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   171
  apply (induct arbitrary: i set: NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   172
  apply (frule listall_conj1)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   173
  apply (drule listall_conj2)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   174
  apply (drule_tac i=i in lift_terms_NF)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   175
  apply assumption
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 39157
diff changeset
   176
  apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   177
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   178
  apply (rule NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   179
  apply assumption
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   180
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   181
  apply (rule NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   182
  apply assumption
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   183
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   184
  apply (rule NF.Abs)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   185
  apply simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   186
  done
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   187
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   188
text {*
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   189
@{term NF} characterizes exactly the terms that are in normal form.
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   190
*}
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   191
  
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   192
lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   193
proof
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   194
  assume "NF t"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   195
  then have "\<And>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   196
  proof induct
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   197
    case (App ts t)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   198
    show ?case
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   199
    proof
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   200
      assume "Var t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> t'"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   201
      then obtain rs where "ts => rs"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24537
diff changeset
   202
        by (iprover dest: head_Var_reduction)
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   203
      with App show False
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24537
diff changeset
   204
        by (induct rs arbitrary: ts) auto
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   205
    qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   206
  next
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   207
    case (Abs t)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   208
    show ?case
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   209
    proof
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   210
      assume "Abs t \<rightarrow>\<^sub>\<beta> t'"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   211
      then show False using Abs by cases simp_all
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   212
    qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   213
  qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   214
  then show "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" ..
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   215
next
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   216
  assume H: "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   217
  then show "NF t"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   218
  proof (induct t rule: Apps_dB_induct)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   219
    case (1 n ts)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   220
    then have "\<forall>ts'. \<not> ts => ts'"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   221
      by (iprover intro: apps_preserves_betas)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   222
    with 1(1) have "listall NF ts"
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   223
      by (induct ts) auto
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   224
    then show ?case by (rule NF.App)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   225
  next
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   226
    case (2 u ts)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   227
    show ?case
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   228
    proof (cases ts)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   229
      case Nil
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   230
      from 2 have "\<forall>u'. \<not> u \<rightarrow>\<^sub>\<beta> u'"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24537
diff changeset
   231
        by (auto intro: apps_preserves_beta)
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   232
      then have "NF u" by (rule 2)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   233
      then have "NF (Abs u)" by (rule NF.Abs)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   234
      with Nil show ?thesis by simp
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   235
    next
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   236
      case (Cons r rs)
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   237
      have "Abs u \<degree> r \<rightarrow>\<^sub>\<beta> u[r/0]" ..
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   238
      then have "Abs u \<degree> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24537
diff changeset
   239
        by (rule apps_preserves_beta)
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   240
      with Cons have "Abs u \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24537
diff changeset
   241
        by simp
24537
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   242
      with 2 show ?thesis by iprover
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   243
    qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   244
  qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   245
qed
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   246
57c7dfaa0153 Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff changeset
   247
end