# HG changeset patch
# User wenzelm
# Date 1126026643 -7200
# Node ID 8608f7a881ebabdfe53c787b85c2cd00888165aa
# Parent  aa3833fb7bee457c4d5bd083eb9762ebb2dbb84f
converted to Isar theory format;

diff -r aa3833fb7bee -r 8608f7a881eb src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Tue Sep 06 19:03:39 2005 +0200
+++ b/src/HOL/ex/MT.ML	Tue Sep 06 19:10:43 2005 +0200
@@ -26,7 +26,7 @@
 
 val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
 
-val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
+val prems = goal (the_context ()) "P a b ==> P (fst (a,b)) (snd (a,b))";
 by (simp_tac (simpset() addsimps prems) 1);
 qed "infsys_p1";
 
@@ -48,14 +48,14 @@
 
 (* Least fixpoints *)
 
-val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
+val prems = goal (the_context ()) "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
 by (rtac subsetD 1);
 by (rtac lfp_lemma2 1);
 by (resolve_tac prems 1);
 by (resolve_tac prems 1);
 qed "lfp_intro2";
 
-val prems = goal MT.thy
+val prems = goal (the_context ())
   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
 \   P(x)";
 by (cut_facts_tac prems 1);
@@ -66,7 +66,7 @@
 by (assume_tac 1);
 qed "lfp_elim2";
 
-val prems = goal MT.thy
+val prems = goal (the_context ())
   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
 \   P(x)";
 by (cut_facts_tac prems 1);
@@ -79,7 +79,7 @@
 
 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
 
-val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
+val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
 by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
 by (rtac (monoh RS monoD) 1);
 by (rtac (UnE RS subsetI) 1);
@@ -90,7 +90,7 @@
 by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
 qed "gfp_coind2";
 
-val [gfph,monoh,caseh] = goal MT.thy 
+val [gfph,monoh,caseh] = goal (the_context ())
   "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
 by (rtac caseh 1);
 by (rtac subsetD 1);
@@ -105,16 +105,16 @@
 
 val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
 
-val e_disjs = 
-  [ e_disj_const_var, 
-    e_disj_const_fn, 
-    e_disj_const_fix, 
+val e_disjs =
+  [ e_disj_const_var,
+    e_disj_const_fn,
+    e_disj_const_fix,
     e_disj_const_app,
-    e_disj_var_fn, 
-    e_disj_var_fix, 
-    e_disj_var_app, 
-    e_disj_fn_fix, 
-    e_disj_fn_app, 
+    e_disj_var_fn,
+    e_disj_var_fix,
+    e_disj_var_app,
+    e_disj_fn_fix,
+    e_disj_fn_app,
     e_disj_fix_app
   ];
 
@@ -151,11 +151,11 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-	(*Naughty!  But the quantifiers are nested VERY deeply...*)
+        (*Naughty!  But the quantifiers are nested VERY deeply...*)
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "eval_const";
 
-Goalw [eval_def, eval_rel_def] 
+Goalw [eval_def, eval_rel_def]
   "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
@@ -163,7 +163,7 @@
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "eval_var2";
 
-Goalw [eval_def, eval_rel_def] 
+Goalw [eval_def, eval_rel_def]
   "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
@@ -171,7 +171,7 @@
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "eval_fn";
 
-Goalw [eval_def, eval_rel_def] 
+Goalw [eval_def, eval_rel_def]
   " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
 \   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
 by (rtac lfp_intro2 1);
@@ -182,19 +182,19 @@
 
 Goalw [eval_def, eval_rel_def]
   " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
-\   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
+\   ve |- e1 @@ e2 ---> v_const(c_app c1 c2)";
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "eval_app1";
 
-Goalw [eval_def, eval_rel_def] 
+Goalw [eval_def, eval_rel_def]
   " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
 \       ve |- e2 ---> v2; \
 \       vem + {xm |-> v2} |- em ---> v \
 \   |] ==> \
-\   ve |- e1 @ e2 ---> v";
+\   ve |- e1 @@ e2 ---> v";
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
@@ -203,7 +203,7 @@
 
 (* Strong elimination, induction on evaluations *)
 
-val prems = goalw MT.thy [eval_def, eval_rel_def]
+val prems = goalw (the_context ()) [eval_def, eval_rel_def]
   " [| ve |- e ---> v; \
 \      !!ve c. P(((ve,e_const(c)),v_const(c))); \
 \      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
@@ -213,13 +213,13 @@
 \        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
 \      !!ve c1 c2 e1 e2. \
 \        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
-\        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
+\        P(((ve,e1 @@ e2),v_const(c_app c1 c2))); \
 \      !!ve vem xm e1 e2 em v v2. \
 \        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
 \            P(((ve,e2),v2)); \
 \            P(((vem + {xm |-> v2},em),v)) \
 \        |] ==> \
-\        P(((ve,e1 @ e2),v)) \
+\        P(((ve,e1 @@ e2),v)) \
 \   |] ==> \
 \   P(((ve,e),v))";
 by (resolve_tac (prems RL [lfp_ind2]) 1);
@@ -231,7 +231,7 @@
 by (ALLGOALS (Blast_tac));
 qed "eval_ind0";
 
-val prems = goal MT.thy 
+val prems = goal (the_context ())
   " [| ve |- e ---> v; \
 \      !!ve c. P ve (e_const c) (v_const c); \
 \      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
@@ -241,12 +241,12 @@
 \        P ve (fix ev2(ev1) = e) (v_clos cl); \
 \      !!ve c1 c2 e1 e2. \
 \        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
-\        P ve (e1 @ e2) (v_const(c_app c1 c2)); \
+\        P ve (e1 @@ e2) (v_const(c_app c1 c2)); \
 \      !!ve vem evm e1 e2 em v v2. \
 \        [|  P ve e1 (v_clos <|evm,em,vem|>); \
 \            P ve e2 v2; \
 \            P (vem + {evm |-> v2}) em v \
-\        |] ==> P ve (e1 @ e2) v \
+\        |] ==> P ve (e1 @@ e2) v \
 \   |] ==> P ve e v";
 by (res_inst_tac [("P","P")] infsys_pp2 1);
 by (rtac eval_ind0 1);
@@ -265,7 +265,7 @@
 
 (* Introduction rules *)
 
-Goalw [elab_def, elab_rel_def] 
+Goalw [elab_def, elab_rel_def]
   "c isof ty ==> te |- e_const(c) ===> ty";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
@@ -273,7 +273,7 @@
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "elab_const";
 
-Goalw [elab_def, elab_rel_def] 
+Goalw [elab_def, elab_rel_def]
   "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
@@ -281,7 +281,7 @@
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "elab_var";
 
-Goalw [elab_def, elab_rel_def] 
+Goalw [elab_def, elab_rel_def]
   "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
@@ -298,9 +298,9 @@
 by (blast_tac (claset() addSIs [exI]) 1);
 qed "elab_fix";
 
-Goalw [elab_def, elab_rel_def] 
+Goalw [elab_def, elab_rel_def]
   "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
-\        te |- e1 @ e2 ===> ty2";
+\        te |- e1 @@ e2 ===> ty2";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
@@ -309,7 +309,7 @@
 
 (* Strong elimination, induction on elaborations *)
 
-val prems = goalw MT.thy [elab_def, elab_rel_def]
+val prems = goalw (the_context ()) [elab_def, elab_rel_def]
   " [| te |- e ===> t; \
 \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
 \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
@@ -325,7 +325,7 @@
 \        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
 \           te |- e2 ===> t1; P(((te,e2),t1)) \
 \        |] ==> \
-\        P(((te,e1 @ e2),t2)) \
+\        P(((te,e1 @@ e2),t2)) \
 \   |] ==> \
 \   P(((te,e),t))";
 by (resolve_tac (prems RL [lfp_ind2]) 1);
@@ -337,7 +337,7 @@
 by (ALLGOALS (Blast_tac));
 qed "elab_ind0";
 
-val prems = goal MT.thy
+val prems = goal (the_context ())
   " [| te |- e ===> t; \
 \       !!te c t. c isof t ==> P te (e_const c) t; \
 \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
@@ -353,7 +353,7 @@
 \        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
 \           te |- e2 ===> t1; P te e2 t1 \
 \        |] ==> \
-\        P te (e1 @ e2) t2 \ 
+\        P te (e1 @@ e2) t2 \
 \   |] ==> \
 \   P te e t";
 by (res_inst_tac [("P","P")] infsys_pp2 1);
@@ -365,7 +365,7 @@
 
 (* Weak elimination, case analysis on elaborations *)
 
-val prems = goalw MT.thy [elab_def, elab_rel_def]
+val prems = goalw (the_context ()) [elab_def, elab_rel_def]
   " [| te |- e ===> t; \
 \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
 \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
@@ -376,7 +376,7 @@
 \        P(((te,fix f(x) = e),t1->t2)); \
 \      !!te e1 e2 t1 t2. \
 \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
-\        P(((te,e1 @ e2),t2)) \
+\        P(((te,e1 @@ e2),t2)) \
 \   |] ==> \
 \   P(((te,e),t))";
 by (resolve_tac (prems RL [lfp_elim2]) 1);
@@ -388,7 +388,7 @@
 by (ALLGOALS (Blast_tac));
 qed "elab_elim0";
 
-val prems = goal MT.thy
+val prems = goal (the_context ())
   " [| te |- e ===> t; \
 \       !!te c t. c isof t ==> P te (e_const c) t; \
 \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
@@ -399,7 +399,7 @@
 \        P te (fix f(x) = e) (t1->t2); \
 \      !!te e1 e2 t1 t2. \
 \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
-\        P te (e1 @ e2) t2 \ 
+\        P te (e1 @@ e2) t2 \
 \   |] ==> \
 \   P te e t";
 by (res_inst_tac [("P","P")] infsys_pp2 1);
@@ -411,13 +411,13 @@
 
 (* Elimination rules for each expression *)
 
-fun elab_e_elim_tac p = 
-  ( (rtac elab_elim 1) THEN 
-    (resolve_tac p 1) THEN 
+fun elab_e_elim_tac p =
+  ( (rtac elab_elim 1) THEN
+    (resolve_tac p 1) THEN
     (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
   );
 
-val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
+val prems = goal (the_context ()) "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
 by (elab_e_elim_tac prems);
 qed "elab_const_elim_lem";
 
@@ -426,7 +426,7 @@
 by (Blast_tac 1);
 qed "elab_const_elim";
 
-val prems = goal MT.thy 
+val prems = goal (the_context ())
   "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
 by (elab_e_elim_tac prems);
 qed "elab_var_elim_lem";
@@ -436,7 +436,7 @@
 by (Blast_tac 1);
 qed "elab_var_elim";
 
-val prems = goal MT.thy 
+val prems = goal (the_context ())
   " te |- e ===> t ==> \
 \   ( e = fn x1 => e1 --> \
 \     (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
@@ -450,10 +450,10 @@
 by (Blast_tac 1);
 qed "elab_fn_elim";
 
-val prems = goal MT.thy 
+val prems = goal (the_context ())
   " te |- e ===> t ==> \
 \   (e = fix f(x) = e1 --> \
-\   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; 
+\   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))";
 by (elab_e_elim_tac prems);
 qed "elab_fix_elim_lem";
 
@@ -463,13 +463,13 @@
 by (Blast_tac 1);
 qed "elab_fix_elim";
 
-val prems = goal MT.thy 
+val prems = goal (the_context ())
   " te |- e ===> t2 ==> \
-\   (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; 
+\   (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))";
 by (elab_e_elim_tac prems);
 qed "elab_app_elim_lem";
 
-Goal "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
+Goal "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
 by (dtac elab_app_elim_lem 1);
 by (Blast_tac 1);
 qed "elab_app_elim";
@@ -480,13 +480,13 @@
 
 (* Monotonicity of hasty_fun *)
 
-Goalw [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
+Goalw [mono_def, hasty_fun_def] "mono(hasty_fun)";
 by infsys_mono_tac;
 by (Blast_tac 1);
 qed "mono_hasty_fun";
 
-(* 
-  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
+(*
+  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
   enjoys two strong indtroduction (co-induction) rules and an elimination rule.
 *)
 
@@ -494,7 +494,7 @@
 
 Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
 by (rtac gfp_coind2 1);
-by (rewtac MT.hasty_fun_def);
+by (rewtac hasty_fun_def);
 by (rtac CollectI 1);
 by (rtac disjI1 1);
 by (Blast_tac 1);
@@ -521,7 +521,7 @@
 
 (* Elimination rule for hasty_rel *)
 
-val prems = goalw MT.thy [hasty_rel_def]
+val prems = goalw (the_context ()) [hasty_rel_def]
   " [| !! c t. c isof t ==> P((v_const(c),t)); \
 \      !! te ev e t ve. \
 \        [| te |- fn ev => e ===> t; \
@@ -540,7 +540,7 @@
 by (REPEAT (ares_tac prems 1));
 qed "hasty_rel_elim0";
 
-val prems = goal MT.thy 
+val prems = goal (the_context ())
   " [| (v,t) : hasty_rel; \
 \      !! c t. c isof t ==> P (v_const c) t; \
 \      !! te ev e t ve. \
@@ -562,7 +562,7 @@
 by (etac hasty_rel_const_coind 1);
 qed "hasty_const";
 
-Goalw [hasty_def,hasty_env_def] 
+Goalw [hasty_def,hasty_env_def]
  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
 by (rtac hasty_rel_clos_coind 1);
 by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
@@ -570,8 +570,8 @@
 
 (* Elimination on constants for hasty *)
 
-Goalw [hasty_def] 
-  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
+Goalw [hasty_def]
+  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
 by (rtac hasty_rel_elim 1);
 by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
 qed "hasty_elim_const_lem";
@@ -583,7 +583,7 @@
 
 (* Elimination on closures for hasty *)
 
-Goalw [hasty_env_def,hasty_def] 
+Goalw [hasty_env_def,hasty_def]
   " v hasty t ==> \
 \   ! x e ve. \
 \     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
@@ -664,7 +664,7 @@
 
 Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
-\      ve hastyenv te ; te |- e1 @ e2 ===> t \
+\      ve hastyenv te ; te |- e1 @@ e2 ===> t \
 \   |] ==> \
 \   v_const(c_app c1 c2) hasty t";
 by (dtac elab_app_elim 1);
@@ -684,7 +684,7 @@
 \      ! t te. \
 \        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
 \      ve hastyenv te ; \
-\      te |- e1 @ e2 ===> t \
+\      te |- e1 @@ e2 ===> t \
 \   |] ==> \
 \   v hasty t";
 by (dtac elab_app_elim 1);
@@ -710,7 +710,7 @@
 
 by (etac eval_ind 1);
 by Safe_tac;
-by (DEPTH_SOLVE 
+by (DEPTH_SOLVE
     (ares_tac [consistency_const, consistency_var, consistency_fn,
                consistency_fix, consistency_app1, consistency_app2] 1));
 qed "consistency";
@@ -719,7 +719,7 @@
 (* The Basic Consistency theorem                                *)
 (* ############################################################ *)
 
-Goalw [isof_env_def,hasty_env_def] 
+Goalw [isof_env_def,hasty_env_def]
   "ve isofenv te ==> ve hastyenv te";
 by Safe_tac;
 by (etac allE 1);
@@ -736,5 +736,3 @@
 by (dtac consistency 1);
 by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
 qed "basic_consistency";
-
-writeln"Reached end of file.";
diff -r aa3833fb7bee -r 8608f7a881eb src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Tue Sep 06 19:03:39 2005 +0200
+++ b/src/HOL/ex/MT.thy	Tue Sep 06 19:10:43 2005 +0200
@@ -13,37 +13,23 @@
     Report 308, Computer Lab, University of Cambridge (1993).
 *)
 
-MT = Inductive + 
-
-types 
-  Const
+theory MT
+imports Main
+begin
 
-  ExVar
-  Ex
+typedecl Const
 
-  TyConst
-  Ty
-
-  Clos
-  Val
+typedecl ExVar
+typedecl Ex
 
-  ValEnv
-  TyEnv
-
-arities 
-  Const :: type
-
-  ExVar :: type
-  Ex :: type
+typedecl TyConst
+typedecl Ty
 
-  TyConst :: type
-  Ty :: type
+typedecl Clos
+typedecl Val
 
-  Clos :: type
-  Val :: type
-
-  ValEnv :: type
-  TyEnv :: type
+typedecl ValEnv
+typedecl TyEnv
 
 consts
   c_app :: "[Const, Const] => Const"
@@ -52,7 +38,7 @@
   e_var :: "ExVar => Ex"
   e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
   e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
-  e_app :: "[Ex, Ex] => Ex" ("_ @ _" [51,51] 1000)
+  e_app :: "[Ex, Ex] => Ex" ("_ @@ _" [51,51] 1000)
   e_const_fst :: "Ex => Const"
 
   t_const :: "TyConst => Ty"
@@ -60,7 +46,7 @@
 
   v_const :: "Const => Val"
   v_clos :: "Clos => Val"
-  
+
   ve_emp :: ValEnv
   ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
   ve_dom :: "ValEnv => ExVar set"
@@ -80,7 +66,7 @@
   elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
   elab_rel :: "((TyEnv * Ex) * Ty) set"
   elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
-  
+
   isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
   isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
 
@@ -89,99 +75,99 @@
   hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
   hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
 
-rules
+axioms
 
-(* 
+(*
   Expression constructors must be injective, distinct and it must be possible
   to do induction over expressions.
 *)
 
 (* All the constructors are injective *)
 
-  e_const_inj "e_const(c1) = e_const(c2) ==> c1 = c2"
-  e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
-  e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
-  e_fix_inj 
-    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> 
-     ev11 = ev21 & ev12 = ev22 & e1 = e2 
+  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2"
+  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
+  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
+  e_fix_inj:
+    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
+     ev11 = ev21 & ev12 = ev22 & e1 = e2
    "
-  e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22"
+  e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"
 
 (* All constructors are distinct *)
 
-  e_disj_const_var "~e_const(c) = e_var(ev)"
-  e_disj_const_fn "~e_const(c) = fn ev => e"
-  e_disj_const_fix "~e_const(c) = fix ev1(ev2) = e"
-  e_disj_const_app "~e_const(c) = e1 @ e2"
-  e_disj_var_fn "~e_var(ev1) = fn ev2 => e"
-  e_disj_var_fix "~e_var(ev) = fix ev1(ev2) = e"
-  e_disj_var_app "~e_var(ev) = e1 @ e2"
-  e_disj_fn_fix "~fn ev1 => e1 = fix ev21(ev22) = e2"
-  e_disj_fn_app "~fn ev1 => e1 = e21 @ e22"
-  e_disj_fix_app "~fix ev11(ev12) = e1 = e21 @ e22"
+  e_disj_const_var: "~e_const(c) = e_var(ev)"
+  e_disj_const_fn: "~e_const(c) = fn ev => e"
+  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e"
+  e_disj_const_app: "~e_const(c) = e1 @@ e2"
+  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e"
+  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e"
+  e_disj_var_app: "~e_var(ev) = e1 @@ e2"
+  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2"
+  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22"
+  e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"
 
 (* Strong elimination, induction on expressions  *)
 
-  e_ind 
-    " [|  !!ev. P(e_var(ev)); 
-         !!c. P(e_const(c)); 
-         !!ev e. P(e) ==> P(fn ev => e); 
-         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); 
-         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) 
-     |] ==> 
-   P(e) 
+  e_ind:
+    " [|  !!ev. P(e_var(ev));
+         !!c. P(e_const(c));
+         !!ev e. P(e) ==> P(fn ev => e);
+         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
+         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @@ e2)
+     |] ==>
+   P(e)
    "
 
 (* Types - same scheme as for expressions *)
 
-(* All constructors are injective *) 
+(* All constructors are injective *)
 
-  t_const_inj "t_const(c1) = t_const(c2) ==> c1 = c2"
-  t_fun_inj "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
+  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2"
+  t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
 
 (* All constructors are distinct, not needed so far ... *)
 
 (* Strong elimination, induction on types *)
 
- t_ind 
-    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] 
+ t_ind:
+    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
     ==> P(t)"
 
 
 (* Values - same scheme again *)
 
-(* All constructors are injective *) 
+(* All constructors are injective *)
 
-  v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2"
-  v_clos_inj 
-    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> 
+  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2"
+  v_clos_inj:
+    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
      ev1 = ev2 & e1 = e2 & ve1 = ve2"
-  
+
 (* All constructors are distinct *)
 
-  v_disj_const_clos "~v_const(c) = v_clos(cl)"
+  v_disj_const_clos: "~v_const(c) = v_clos(cl)"
 
 (* No induction on values: they are a codatatype! ... *)
 
 
-(* 
+(*
   Value environments bind variables to values. Only the following trivial
   properties are needed.
 *)
 
-  ve_dom_owr "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}"
- 
-  ve_app_owr1 "ve_app (ve + {ev |-> v}) ev=v"
-  ve_app_owr2 "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
+  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}"
+
+  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v"
+  ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
 
 
 (* Type Environments bind variables to types. The following trivial
 properties are needed.  *)
 
-  te_dom_owr "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}"
- 
-  te_app_owr1 "te_app (te + {ev |=> t}) ev=t"
-  te_app_owr2 "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
+  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}"
+
+  te_app_owr1: "te_app (te + {ev |=> t}) ev=t"
+  te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
 
 
 (* The dynamic semantics is defined inductively by a set of inference
@@ -190,89 +176,94 @@
 environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
 as the least fixpoint of the functor eval_fun below.  From this definition
 introduction rules and a strong elimination (induction) rule can be
-derived.  
+derived.
 *)
 
-  eval_fun_def 
-    " eval_fun(s) == 
-     { pp. 
-       (? ve c. pp=((ve,e_const(c)),v_const(c))) | 
+defs
+  eval_fun_def:
+    " eval_fun(s) ==
+     { pp.
+       (? ve c. pp=((ve,e_const(c)),v_const(c))) |
        (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
-       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| 
-       ( ? ve e x f cl. 
-           pp=((ve,fix f(x) = e),v_clos(cl)) & 
-           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  
-       ) | 
-       ( ? ve e1 e2 c1 c2. 
-           pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & 
-           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s 
-       ) | 
-       ( ? ve vem e1 e2 em xm v v2. 
-           pp=((ve,e1 @ e2),v) & 
-           ((ve,e1),v_clos(<|xm,em,vem|>)):s & 
-           ((ve,e2),v2):s & 
-           ((vem+{xm |-> v2},em),v):s 
-       ) 
+       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))|
+       ( ? ve e x f cl.
+           pp=((ve,fix f(x) = e),v_clos(cl)) &
+           cl=<|x, e, ve+{f |-> v_clos(cl)} |>
+       ) |
+       ( ? ve e1 e2 c1 c2.
+           pp=((ve,e1 @@ e2),v_const(c_app c1 c2)) &
+           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s
+       ) |
+       ( ? ve vem e1 e2 em xm v v2.
+           pp=((ve,e1 @@ e2),v) &
+           ((ve,e1),v_clos(<|xm,em,vem|>)):s &
+           ((ve,e2),v2):s &
+           ((vem+{xm |-> v2},em),v):s
+       )
      }"
 
-  eval_rel_def "eval_rel == lfp(eval_fun)"
-  eval_def "ve |- e ---> v == ((ve,e),v):eval_rel"
+  eval_rel_def: "eval_rel == lfp(eval_fun)"
+  eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
 
 (* The static semantics is defined in the same way as the dynamic
 semantics.  The relation te |- e ===> t express the expression e has the
 type t in the type environment te.
 *)
 
-  elab_fun_def 
-  "elab_fun(s) == 
-  { pp. 
-    (? te c t. pp=((te,e_const(c)),t) & c isof t) | 
-    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | 
-    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | 
-    (? te f x e t1 t2. 
-       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s 
-    ) | 
-    (? te e1 e2 t1 t2. 
-       pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s 
-    ) 
+  elab_fun_def:
+  "elab_fun(s) ==
+  { pp.
+    (? te c t. pp=((te,e_const(c)),t) & c isof t) |
+    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
+    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
+    (? te f x e t1 t2.
+       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
+    ) |
+    (? te e1 e2 t1 t2.
+       pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
+    )
   }"
 
-  elab_rel_def "elab_rel == lfp(elab_fun)"
-  elab_def "te |- e ===> t == ((te,e),t):elab_rel"
+  elab_rel_def: "elab_rel == lfp(elab_fun)"
+  elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
 
 (* The original correspondence relation *)
 
-  isof_env_def 
-    " ve isofenv te == 
-     ve_dom(ve) = te_dom(te) & 
-     ( ! x. 
-         x:ve_dom(ve) --> 
-         (? c. ve_app ve x = v_const(c) & c isof te_app te x) 
-     ) 
+  isof_env_def:
+    " ve isofenv te ==
+     ve_dom(ve) = te_dom(te) &
+     ( ! x.
+         x:ve_dom(ve) -->
+         (? c. ve_app ve x = v_const(c) & c isof te_app te x)
+     )
    "
 
-  isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
+axioms
+  isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
 
+defs
 (* The extented correspondence relation *)
 
-  hasty_fun_def
-    " hasty_fun(r) == 
-     { p. 
-       ( ? c t. p = (v_const(c),t) & c isof t) | 
-       ( ? ev e ve t te. 
-           p = (v_clos(<|ev,e,ve|>),t) & 
-           te |- fn ev => e ===> t & 
-           ve_dom(ve) = te_dom(te) & 
-           (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) 
-       ) 
-     } 
+  hasty_fun_def:
+    " hasty_fun(r) ==
+     { p.
+       ( ? c t. p = (v_const(c),t) & c isof t) |
+       ( ? ev e ve t te.
+           p = (v_clos(<|ev,e,ve|>),t) &
+           te |- fn ev => e ===> t &
+           ve_dom(ve) = te_dom(te) &
+           (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
+       )
+     }
    "
 
-  hasty_rel_def "hasty_rel == gfp(hasty_fun)"
-  hasty_def "v hasty t == (v,t) : hasty_rel"
-  hasty_env_def 
-    " ve hastyenv te == 
-     ve_dom(ve) = te_dom(te) & 
+  hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
+  hasty_def: "v hasty t == (v,t) : hasty_rel"
+  hasty_env_def:
+    " ve hastyenv te ==
+     ve_dom(ve) = te_dom(te) &
      (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end