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