theory System_Is_Secure
  imports Main
  begin

consts A :: bool
consts System_Is_Secure :: bool

(* formulation with explicit assumptions, easy for reviewer to spot that user made too strong assumptions *)
theorem System_Is_Secure_1: 
  assumes "A" 
  and "~ A"  
  shows System_Is_Secure
proof-
  from assms show ?thesis by simp
qed

(* Kuncar/Popescu: A Consistent Foundation for Isabelle/HOL, ITP 2015 *)
consts c :: bool
typedef T = "{True, c}" by blast
defs c_bool_def: "c::bool == ~ (ALL(x::T) y. x = y)"
 lemma L: "(ALL(x::T) y. x = y) <-> c"
using Rep_T Rep_T_inject Abs_T_inject by blast
lemma MyFalse: False
using L unfolding c_bool_def by auto

theorem MySystem_Is_Secure [simp]: System_Is_Secure
using MyFalse by simp

(* formulation with implicit assumptions, not that easy for reviewer to spot that user made too strong assumptions *)
theorem System_Is_Secure_2: System_Is_Secure by simp

end