header {* The main lemma about Num and the Second Fixed Point Theorem *}+
−
+
−
theory Theorem imports Consts begin+
−
+
−
lemmas [simp] = b3[OF bI] b1 b4 b5 supp_Num[unfolded Num_def supp_ltgt] Num_def lam.fresh[unfolded fresh_def] fresh_def b6+
−
lemmas app = Ltgt1_app+
−
+
−
lemma Num:+
−
  shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"+
−
proof (induct M rule: lam.induct)+
−
  case (V n)+
−
  have "Num \<cdot> \<lbrace>V n\<rbrace> = Num \<cdot> (Var \<cdot> V n)" by simp+
−
  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Var \<cdot> V n)" by simp+
−
  also have "... \<approx> Var \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .+
−
  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Var_app .+
−
  also have "... \<approx> A1 \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp+
−
  also have "... \<approx> F1 \<cdot> V n" using A_app(1) .+
−
  also have "... \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V n)" using F_app(1) .+
−
  also have "... = \<lbrace>\<lbrace>V n\<rbrace>\<rbrace>" by simp+
−
  finally show "Num \<cdot> \<lbrace>V n\<rbrace> \<approx> \<lbrace>\<lbrace>V n\<rbrace>\<rbrace>".+
−
next+
−
  case (Ap M N)+
−
  assume IH: "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "Num \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>"+
−
  have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp+
−
  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp+
−
  also have "... \<approx> App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .+
−
  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using App_app .+
−
  also have "... \<approx> A2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp+
−
  also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> Num" using A_app(2) by simp+
−
  also have "... \<approx> App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) .+
−
  also have "... \<approx> App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp+
−
  also have "... \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>" using IH by simp+
−
  finally show "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>".+
−
next+
−
  case (Lm x P)+
−
  assume IH: "Num \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>"+
−
  have "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> = Num \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp+
−
  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp+
−
  also have "... \<approx> Abs \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .+
−
  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 0 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Abs_app .+
−
  also have "... \<approx> A3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp+
−
  also have "... \<approx> F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" using A_app(3) .+
−
  also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Num" by simp+
−
  also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> V x)))" by (rule F3_app) simp_all+
−
  also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp+
−
  also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp+
−
  also have "... = \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" by simp+
−
  finally show "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" .+
−
qed+
−
+
−
lemmas [simp] = Ap Num+
−
lemmas [simp del] = fresh_def Num_def+
−
+
−
theorem SFP:+
−
  fixes F :: lam+
−
  shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>"+
−
proof -+
−
  obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast+
−
  def W \<equiv> "\<integral>x. (F \<cdot> (App \<cdot> V x \<cdot> (Num \<cdot> V x)))"+
−
  def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>"+
−
  have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def ..+
−
  also have "... = (\<integral>x. (F \<cdot> (App \<cdot> V x \<cdot> (Num \<cdot> V x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def ..+
−
  also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp+
−
  also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp+
−
  also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp+
−
  also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..+
−
  finally show ?thesis by blast+
−
qed+
−
+
−
end+
−