1.1 --- a/src/HOL/ex/MT.thy	Thu Feb 28 13:24:51 2013 +0100
     1.2 +++ b/src/HOL/ex/MT.thy	Thu Feb 28 13:33:01 2013 +0100
     1.3 @@ -76,39 +76,38 @@
     1.4    hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
     1.5    hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
     1.6  
     1.7 -axioms
     1.8 -
     1.9  (*
    1.10    Expression constructors must be injective, distinct and it must be possible
    1.11    to do induction over expressions.
    1.12  *)
    1.13  
    1.14  (* All the constructors are injective *)
    1.15 -
    1.16 -  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2"
    1.17 -  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
    1.18 -  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
    1.19 +axiomatization where
    1.20 +  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2" and
    1.21 +  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" and
    1.22 +  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" and
    1.23    e_fix_inj:
    1.24      " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
    1.25 -     ev11 = ev21 & ev12 = ev22 & e1 = e2
    1.26 -   "
    1.27 +     ev11 = ev21 & ev12 = ev22 & e1 = e2" and
    1.28    e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"
    1.29  
    1.30  (* All constructors are distinct *)
    1.31  
    1.32 -  e_disj_const_var: "~e_const(c) = e_var(ev)"
    1.33 -  e_disj_const_fn: "~e_const(c) = fn ev => e"
    1.34 -  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e"
    1.35 -  e_disj_const_app: "~e_const(c) = e1 @@ e2"
    1.36 -  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e"
    1.37 -  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e"
    1.38 -  e_disj_var_app: "~e_var(ev) = e1 @@ e2"
    1.39 -  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2"
    1.40 -  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22"
    1.41 +axiomatization where
    1.42 +  e_disj_const_var: "~e_const(c) = e_var(ev)" and
    1.43 +  e_disj_const_fn: "~e_const(c) = fn ev => e" and
    1.44 +  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e" and
    1.45 +  e_disj_const_app: "~e_const(c) = e1 @@ e2" and
    1.46 +  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e" and
    1.47 +  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e" and
    1.48 +  e_disj_var_app: "~e_var(ev) = e1 @@ e2" and
    1.49 +  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2" and
    1.50 +  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22" and
    1.51    e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"
    1.52  
    1.53  (* Strong elimination, induction on expressions  *)
    1.54  
    1.55 +axiomatization where
    1.56    e_ind:
    1.57      " [|  !!ev. P(e_var(ev));
    1.58           !!c. P(e_const(c));
    1.59 @@ -123,13 +122,15 @@
    1.60  
    1.61  (* All constructors are injective *)
    1.62  
    1.63 -  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2"
    1.64 +axiomatization where
    1.65 +  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2" and
    1.66    t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
    1.67  
    1.68  (* All constructors are distinct, not needed so far ... *)
    1.69  
    1.70  (* Strong elimination, induction on types *)
    1.71  
    1.72 +axiomatization where
    1.73   t_ind:
    1.74      "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
    1.75      ==> P(t)"
    1.76 @@ -139,13 +140,15 @@
    1.77  
    1.78  (* All constructors are injective *)
    1.79  
    1.80 -  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2"
    1.81 +axiomatization where
    1.82 +  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2" and
    1.83    v_clos_inj:
    1.84      " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
    1.85       ev1 = ev2 & e1 = e2 & ve1 = ve2"
    1.86  
    1.87  (* All constructors are distinct *)
    1.88  
    1.89 +axiomatization where
    1.90    v_disj_const_clos: "~v_const(c) = v_clos(cl)"
    1.91  
    1.92  (* No induction on values: they are a codatatype! ... *)
    1.93 @@ -156,18 +159,20 @@
    1.94    properties are needed.
    1.95  *)
    1.96  
    1.97 -  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}"
    1.98 +axiomatization where
    1.99 +  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}" and
   1.100  
   1.101 -  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v"
   1.102 +  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v" and
   1.103    ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
   1.104  
   1.105  
   1.106  (* Type Environments bind variables to types. The following trivial
   1.107  properties are needed.  *)
   1.108  
   1.109 -  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}"
   1.110 +axiomatization where
   1.111 +  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}" and
   1.112  
   1.113 -  te_app_owr1: "te_app (te + {ev |=> t}) ev=t"
   1.114 +  te_app_owr1: "te_app (te + {ev |=> t}) ev=t" and
   1.115    te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
   1.116  
   1.117  
   1.118 @@ -239,7 +244,7 @@
   1.119       )
   1.120     "
   1.121  
   1.122 -axioms
   1.123 +axiomatization where
   1.124    isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
   1.125  
   1.126  defs