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