theory VSHOLEx
imports VSHOL
begin

theorem sym: "[| s= t |] ==> t= s"
  apply (rule subst [where P="%x. x= s"])
  apply (assumption)
  apply (rule refl)
  done

theorem trans: "[| s= t; t= u |] ==> s= u"
  apply (rule subst [where P="%x. x= u" and s="t"])
  apply (rule sym)
  apply (assumption)
  apply (assumption)
  done

theorem cong: "[| f= g; x= y |] ==> f x = g y"
  apply (rule subst [where P="%a. f x = g a" and s="x"])
  apply (assumption)  
  apply (rule subst [where P="%a. f x = a x" and s="f"])
  apply (assumption)
  apply (rule refl)
  done

theorem iffI: "[| P==> Q; Q ==> P |] ==> P= Q"
  apply (rule mp [where P="Q--> P"])
  apply (rule mp [where P="P--> Q"])
  apply (rule iff)
  apply (rule impI) 
  apply (assumption)
  apply (rule impI)
  apply (assumption)
  done

theorem iffD2: "[| P= Q; Q |] ==> P"
  apply (rule subst [where s= "Q"])
  apply (rule sym)
  apply (assumption)
  apply (assumption)
  done  

theorem true: "True"
  apply (unfold True_def)
  apply (rule refl)
  done

theorem eqTrueI: "P ==> P= True"
  apply (rule iffI)
  apply (rule true)
  apply (assumption)
  done

theorem eqTrueE: "P= True ==> P"
  apply (rule iffD2 [where Q="True"])
  apply (assumption)
  apply (rule true)
  done

theorem allI: "[| !!x. P x |] ==> ALL x. P x"
  apply (unfold All_def)
  apply (rule ext)
  apply (rule eqTrueI)
  apply (assumption)
  done

theorem spec: "[| ALL x. P x |] ==> P t"
  apply (unfold All_def)
  apply (rule eqTrueE)
  apply (rule cong [where f="P" and g="%x. True" and x="t"])
  apply (assumption)
  apply (rule refl)
  done


  

end