doc-src/AxClass/out

use HOLogic.Not;
export indexify_names;

- assoc;
val it =
  "(?x::?'a::semigroup) <*> (?y::?'a::semigroup) <*> (?z::?'a::semigroup) =
   ?x <*> (?y <*> ?z)" : thm
- left_unit;
val it = "1 <*> (?x::?'a::group) = ?x" : thm
- left_inv;
val it = "inv (?x::?'a::group) <*> ?x = 1" : thm
- commut;
val it = "(?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x" : thm


- right_unit;
val it = "(?x::?'a::group) <*> 1 = ?x" : thm
- right_inv;
val it = "(?x::?'a::group) <*> inv ?x = 1" : thm
- inv_product;
val it = "inv ((?x::?'a::group) <*> (?y::?'a::group)) = inv ?y <*> inv ?x"
  : thm
- inv_inv;
val it = "inv (inv (?x::?'a::group)) = ?x" : thm
- ex1_inv;
val it = "ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1" : thm


- groupI;
val it =
  "[| OFCLASS(?'a::term, semigroup_class); !!x::?'a::term. 1 <*> x = x;
      !!x::?'a::term. inv x <*> x = 1 |] ==> OFCLASS(?'a::term, group_class)"
  : thm


- open AxClass;
- goal_arity Xor.thy ("bool", [], "agroup");
Level 0
OFCLASS(bool, agroup_class)
 1. OFCLASS(bool, agroup_class)
val it = [] : thm list
- by (axclass_tac Xor.thy []);
Level 1
OFCLASS(bool, agroup_class)
 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)
 2. !!x::bool. 1 <*> x = x
 3. !!x::bool. inv x <*> x = 1
 4. !!(x::bool) y::bool. x <*> y = y <*> x
val it = () : unit

- by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
Level 2
OFCLASS(bool, agroup_class)
 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))
 2. !!x::bool. False ~= x = x
 3. !!x::bool. x ~= x = False
 4. !!(x::bool) y::bool. x ~= y = (y ~= x)
val it = () : unit
- by (ALLGOALS (fast_tac HOL_cs));
Level 3
OFCLASS(bool, agroup_class)
No subgoals!
val it = () : unit
- qed "bool_in_agroup";
val bool_in_agroup = "OFCLASS(bool, agroup_class)" : thm
val it = () : unit


- Product.productI;
val it =
  "OFCLASS(?'a::logic, term_class) ==> OFCLASS(?'a::logic, product_class)"
  : thm