theory BI imports WordMain begin

consts
  MIN :: "'a :: bit"
  MAX :: "'a :: bit"

arities
  "fun" :: (type, bit) bit

axclass boolean_class < bit
  boolean_thm : "boolean bitAND bitOR bitNOT MIN MAX"

types
  'a binop = "['a, 'a] => 'a"

defs (overloaded)
  fun_AND_def : "bitAND == %f g a. (f a AND g a :: 'b :: bit)" 
  fun_OR_def : "bitOR == %f g a. (f a OR g a :: 'b :: bit)" 
  fun_NOT_def : "bitNOT == %g a. (NOT g a :: 'b :: bit)" 
  fun_MIN_def : "MIN == %a. (MIN :: 'b :: bit)" 
  fun_MAX_def : "MAX == %a. (MAX :: 'b :: bit)" 

lemmas boolexp = boolean_thm [unfolded boolean_def] ;

ML {* 
val boolexp = thm "boolexp" ;

val bool_axioms = Seq.list_of (EVERY'
  [REPEAT o dresolve_tac [conjunct1, conjunct2], REPEAT o etac allE, atac] 1
  (boolexp RS revcut_rl)) ;

val _ = bind_thms ("bool_axioms", bool_axioms) ;
*}
lemmas AND_MAX = bool_axioms (7) ;
lemmas OR_MIN = bool_axioms (8) ;

lemma fun_boolean:
  "boolean bitAND bitOR bitNOT MIN (MAX :: 'a => 'b :: boolean_class)" 
  apply (unfold fun_AND_def fun_OR_def
        fun_NOT_def fun_MIN_def fun_MAX_def boolean_def) ;
  apply safe ;
  apply (rule_tac ext bool_axioms)+ ;
  done ;

instance "fun" :: (type, boolean_class) boolean_class
  apply intro_classes ;
  apply (rule_tac fun_boolean) ;
  done ;

(* application to sets *)
instance bool :: bit ..

defs (overloaded)
  bool_NOT_def: "bitNOT == Not"
  bool_AND_def: "bitAND == op &"
  bool_OR_def: "bitOR == op |"
  bool_MIN_def: "MIN == False"
  bool_MAX_def: "MAX == True"
  bool_XOR_def: "bitXOR == (%x y. x ~= y)"

instance bool :: boolean_class
  apply intro_classes ;
  apply (unfold bool_AND_def bool_OR_def
    bool_NOT_def bool_MIN_def bool_MAX_def boolean_def) ;
  by auto ;

(* application to sets *)

instance set :: (type) bit ..

defs (overloaded)
  set_AND_def : "bitAND == %S T. Collect ((%x. x : S) AND (%x. x : T))" 
  set_OR_def : "bitOR == %S T. Collect ((%x. x : S) OR (%x. x : T))" 
  set_NOT_def : "bitNOT == %S. Collect (NOT (%x. x : S))" 
  set_MIN_def : "MIN == Collect MIN"
  set_MAX_def : "MAX == Collect MAX"

lemma set_boolean:
  "boolean bitAND bitOR bitNOT MIN (MAX :: 'a set)" 
  apply (unfold set_AND_def set_OR_def
        set_NOT_def set_MIN_def set_MAX_def boolean_def) ;
  apply (tactic "REPEAT_ALL_NEW (rtac conjI) 1") ;
  apply (tactic "REPEAT_FIRST (rtac allI)") ;
  apply (simp_all only : mem_Collect_eq) ;
  apply (tactic "TRYALL (rtac Collect_cong)") ;
  ML {* val bffcs0 = bool_axioms RL [fun_cong] *} (* [] - why *)
  ML {* val tt0 = theory_of_thm (hd bool_axioms) *} 
  ML {* val bffcs1 = thms "bool_axioms" RL [fun_cong] *}
  ML {* val bffcs2 = @{thms bool_axioms} RL [fun_cong] *}
  ML {* val bffcs3 = map (transfer (the_context())) bool_axioms
    RL [fun_cong] *} 
  apply (tactic "TRYALL (resolve_tac bffcs1)") ;
  apply (simp_all add : AND_MAX OR_MIN) ;
  done ;

instance set :: (type) boolean_class 
  apply intro_classes ;
  apply (rule_tac set_boolean) ;
  done ;

end

(*
bool_axioms RL [fun_cong] ;
Isar.loop() ; oops ; end ; 
theory x imports BI begin 
*)