equal
deleted
inserted
replaced
53 |
53 |
54 theorem SFP: |
54 theorem SFP: |
55 fixes F :: lam |
55 fixes F :: lam |
56 shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>" |
56 shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>" |
57 proof - |
57 proof - |
58 obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast |
58 obtain x :: name where [simp]:"atom x \<sharp> F" using obtain_fresh by blast |
59 def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))" |
59 def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))" |
60 def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>" |
60 def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>" |
61 have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def .. |
61 have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def .. |
62 also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def .. |
62 also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def .. |
63 also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp |
63 also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp |