3167

1 


2 
 assoc;


3 
val it =


4 
"(?x::?'a::semigroup) <*> (?y::?'a::semigroup) <*> (?z::?'a::semigroup) =


5 
?x <*> (?y <*> ?z)" : thm


6 
 left_unit;


7 
val it = "1 <*> (?x::?'a::group) = ?x" : thm


8 
 left_inv;


9 
val it = "inv (?x::?'a::group) <*> ?x = 1" : thm


10 
 commut;


11 
val it = "(?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x" : thm


12 


13 


14 
 right_unit;


15 
val it = "(?x::?'a::group) <*> 1 = ?x" : thm


16 
 right_inv;


17 
val it = "(?x::?'a::group) <*> inv ?x = 1" : thm


18 
 inv_product;


19 
val it = "inv ((?x::?'a::group) <*> (?y::?'a::group)) = inv ?y <*> inv ?x"


20 
: thm


21 
 inv_inv;


22 
val it = "inv (inv (?x::?'a::group)) = ?x" : thm


23 
 ex1_inv;


24 
val it = "ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1" : thm


25 


26 


27 
 groupI;


28 
val it =


29 
"[ OFCLASS(?'a::term, semigroup_class); !!x::?'a::term. 1 <*> x = x;


30 
!!x::?'a::term. inv x <*> x = 1 ] ==> OFCLASS(?'a::term, group_class)"


31 
: thm


32 


33 


34 
 open AxClass;


35 
 goal_arity Xor.thy ("bool", [], "agroup");


36 
Level 0


37 
OFCLASS(bool, agroup_class)


38 
1. OFCLASS(bool, agroup_class)


39 
val it = [] : thm list


40 
 by (axclass_tac Xor.thy []);


41 
Level 1


42 
OFCLASS(bool, agroup_class)


43 
1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)


44 
2. !!x::bool. 1 <*> x = x


45 
3. !!x::bool. inv x <*> x = 1


46 
4. !!(x::bool) y::bool. x <*> y = y <*> x


47 
val it = () : unit


48 


49 
 by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);


50 
Level 2


51 
OFCLASS(bool, agroup_class)


52 
1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))


53 
2. !!x::bool. False ~= x = x


54 
3. !!x::bool. x ~= x = False


55 
4. !!(x::bool) y::bool. x ~= y = (y ~= x)


56 
val it = () : unit


57 
 by (ALLGOALS (fast_tac HOL_cs));


58 
Level 3


59 
OFCLASS(bool, agroup_class)


60 
No subgoals!


61 
val it = () : unit


62 
 qed "bool_in_agroup";


63 
val bool_in_agroup = "OFCLASS(bool, agroup_class)" : thm


64 
val it = () : unit


65 


66 


67 
 Product.productI;


68 
val it =


69 
"OFCLASS(?'a::logic, term_class) ==> OFCLASS(?'a::logic, product_class)"


70 
: thm
