1 header {* The main lemma about Num and the Second Fixed Point Theorem *}

     1 header {* The main lemma about Num and the Second Fixed Point Theorem *}

     2 theory Theorem imports Consts begin

     2 theory Theorem imports Consts begin

     3 

     3 

     5 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

     4 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

     6 lemmas app = Ltgt1_app

     5 lemmas app = Ltgt1_app

     8 

     6 

     9 lemma Num:

     7 lemma Num:

    10   shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"

     8   shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"

    11 proof (induct M rule: lam.induct)

     9 proof (induct M rule: lam.induct)

    12   case (V n)

    10   case (V n)

    65   also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp

    63   also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp

    66   also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp

    64   also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp

    67   also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..

    65   also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..

    68   finally show ?thesis by blast

    66   finally show ?thesis by blast

    69 qed

    67 qed