doc-src/AxClass/out
author oheimb
Wed, 12 Nov 1997 18:58:50 +0100
changeset 4223 f60e3d2c81d3
parent 3167 4e1eae442821
permissions -rw-r--r--
added thin_refl to hyp_subst_tac
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3167
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     2
- assoc;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     3
val it =
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     4
  "(?x::?'a::semigroup) <*> (?y::?'a::semigroup) <*> (?z::?'a::semigroup) =
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     5
   ?x <*> (?y <*> ?z)" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     6
- left_unit;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     7
val it = "1 <*> (?x::?'a::group) = ?x" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     8
- left_inv;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     9
val it = "inv (?x::?'a::group) <*> ?x = 1" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    10
- commut;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    11
val it = "(?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    12
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    13
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    14
- right_unit;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    15
val it = "(?x::?'a::group) <*> 1 = ?x" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    16
- right_inv;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    17
val it = "(?x::?'a::group) <*> inv ?x = 1" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    18
- inv_product;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    19
val it = "inv ((?x::?'a::group) <*> (?y::?'a::group)) = inv ?y <*> inv ?x"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    20
  : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    21
- inv_inv;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    22
val it = "inv (inv (?x::?'a::group)) = ?x" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    23
- ex1_inv;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    24
val it = "ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    25
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    26
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    27
- groupI;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    28
val it =
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    29
  "[| OFCLASS(?'a::term, semigroup_class); !!x::?'a::term. 1 <*> x = x;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    30
      !!x::?'a::term. inv x <*> x = 1 |] ==> OFCLASS(?'a::term, group_class)"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    31
  : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    32
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    33
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    34
- open AxClass;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    35
- goal_arity Xor.thy ("bool", [], "agroup");
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    36
Level 0
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    37
OFCLASS(bool, agroup_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    38
 1. OFCLASS(bool, agroup_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    39
val it = [] : thm list
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    40
- by (axclass_tac Xor.thy []);
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    41
Level 1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    42
OFCLASS(bool, agroup_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    43
 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    44
 2. !!x::bool. 1 <*> x = x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    45
 3. !!x::bool. inv x <*> x = 1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    46
 4. !!(x::bool) y::bool. x <*> y = y <*> x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    47
val it = () : unit
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    48
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    49
- by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    50
Level 2
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    51
OFCLASS(bool, agroup_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    52
 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    53
 2. !!x::bool. False ~= x = x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    54
 3. !!x::bool. x ~= x = False
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    55
 4. !!(x::bool) y::bool. x ~= y = (y ~= x)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    56
val it = () : unit
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    57
- by (ALLGOALS (fast_tac HOL_cs));
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    58
Level 3
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    59
OFCLASS(bool, agroup_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    60
No subgoals!
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    61
val it = () : unit
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    62
- qed "bool_in_agroup";
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    63
val bool_in_agroup = "OFCLASS(bool, agroup_class)" : thm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    64
val it = () : unit
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    65
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    66
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    67
- Product.productI;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    68
val it =
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    69
  "OFCLASS(?'a::logic, term_class) ==> OFCLASS(?'a::logic, product_class)"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    70
  : thm