--- a/src/HOL/MiniML/I.ML Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/I.ML Fri Dec 08 19:48:15 1995 +0100
@@ -115,7 +115,7 @@
addss !simpset) 1);
by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
by ((dtac new_tv_subst_tel 1) THEN (atac 1));
-by ((dres_inst_tac [("a","$ s a")] new_tv_list_le 1) THEN (atac 1));
+by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
by ((dtac new_tv_subst_tel 1) THEN (atac 1));
by (fast_tac (HOL_cs addDs [new_tv_W] addss
(!simpset addsimps [subst_comp_tel])) 1);
--- a/src/HOL/MiniML/I.thy Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/I.thy Fri Dec 08 19:48:15 1995 +0100
@@ -8,17 +8,16 @@
I = W +
consts
- I :: [expr, type_expr list, nat, subst] => result_W
+ I :: [expr, typ list, nat, subst] => result_W
primrec I expr
I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
else Fail)"
- I_Abs "I (Abs e) a n s = I e ((TVar n)#a) (Suc n) s bind
- (%(s,t,m). Ok(s, Fun (TVar n) t, m) )"
+ I_Abs "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+ Ok(s, TVar n -> t, m) )"
I_App "I (App e1 e2) a n s =
- I e1 a n s bind
- (%(s1,t1,m1). I e2 a m1 s1 bind
- (%(s2,t2,m2). mgu ($s2 t1) (Fun ($s2 t2) (TVar m2)) bind
- (%u. Ok($u o s2, TVar m2, Suc m2) ) ))"
-
+ ( (s1,t1,m1) := I e1 a n s;
+ (s2,t2,m2) := I e2 a m1 s1;
+ u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+ Ok($u o s2, TVar m2, Suc m2) )"
end
--- a/src/HOL/MiniML/Maybe.thy Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Maybe.thy Fri Dec 08 19:48:15 1995 +0100
@@ -15,4 +15,7 @@
defs
bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
+syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
+translations "P := E; F" == "E bind (%P.F)"
+
end
--- a/src/HOL/MiniML/MiniML.thy Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/MiniML.thy Fri Dec 08 19:48:15 1995 +0100
@@ -14,9 +14,9 @@
(* type inference rules *)
consts
- has_type :: "(type_expr list * expr * type_expr)set"
+ has_type :: "(typ list * expr * typ)set"
syntax
- "@has_type" :: [type_expr list, expr, type_expr] => bool
+ "@has_type" :: [typ list, expr, typ] => bool
("((_) |-/ (_) :: (_))" 60)
translations
"a |- e :: t" == "(a,e,t):has_type"
@@ -24,8 +24,8 @@
inductive "has_type"
intrs
VarI "[| n < length a |] ==> a |- Var n :: nth n a"
- AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: Fun t1 t2"
- AppI "[| a |- e1 :: Fun t2 t1; a |- e2 :: t2 |]
+ AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+ AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
==> a |- App e1 e2 :: t1"
end
--- a/src/HOL/MiniML/Type.ML Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Type.ML Fri Dec 08 19:48:15 1995 +0100
@@ -13,18 +13,18 @@
(* application of id_subst does not change type expression *)
goalw thy [id_subst_def]
- "$ id_subst = (%t::type_expr.t)";
+ "$ id_subst = (%t::typ.t)";
by (rtac ext 1);
-by (type_expr.induct_tac "t" 1);
+by (typ.induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_te";
Addsimps [app_subst_id_te];
(* application of id_subst does not change list of type expressions *)
goalw thy [app_subst_list]
- "$ id_subst = (%l::type_expr list.l)";
+ "$ id_subst = (%ts::typ list.ts)";
by (rtac ext 1);
-by (list.induct_tac "l" 1);
+by (list.induct_tac "ts" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_tel";
Addsimps [app_subst_id_tel];
@@ -60,14 +60,14 @@
(* composition of substitutions *)
goal thy
- "$ g ($ f t::type_expr) = $ (%x. $ g (f x) ) t";
-by (type_expr.induct_tac "t" 1);
+ "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
+by (typ.induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_comp_te";
goalw thy [app_subst_list]
- "$ g ($ f l::type_expr list) = $ (%x. $ g (f x)) l";
-by (list.induct_tac "l" 1);
+ "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
+by (list.induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
@@ -82,7 +82,7 @@
qed "app_subst_Nil";
goalw thy [app_subst_list]
- "$ s (x#l) = ($ s x)#($ s l)";
+ "$ s (t#ts) = ($ s t)#($ s ts)";
by (Simp_tac 1);
qed "app_subst_Cons";
@@ -95,7 +95,7 @@
qed "new_tv_TVar";
goalw thy [new_tv_def]
- "new_tv n (Fun t1 t2) = (new_tv n t1 & new_tv n t2)";
+ "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
by (fast_tac (HOL_cs addss !simpset) 1);
qed "new_tv_Fun";
@@ -105,7 +105,7 @@
qed "new_tv_Nil";
goalw thy [new_tv_def]
- "new_tv n (x#l) = (new_tv n x & new_tv n l)";
+ "new_tv n (t#ts) = (new_tv n t & new_tv n ts)";
by (fast_tac (HOL_cs addss !simpset) 1);
qed "new_tv_Cons";
@@ -142,23 +142,23 @@
(* substitution affects only variables occurring freely *)
goal thy
- "new_tv n (t::type_expr) --> $(%x. if x=n then t' else s x) t = $s t";
-by (type_expr.induct_tac "t" 1);
+ "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
+by (typ.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "subst_te_new_tv";
Addsimps [subst_te_new_tv];
goal thy
- "new_tv n (a::type_expr list) --> $(%x. if x=n then t else s x) a = $s a";
-by (list.induct_tac "a" 1);
+ "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
+by (list.induct_tac "ts" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "subst_tel_new_tv";
Addsimps [subst_tel_new_tv];
(* all greater variables are also new *)
goal thy
- "n<=m --> new_tv n (t::type_expr) --> new_tv m t";
-by (type_expr.induct_tac "t" 1);
+ "n<=m --> new_tv n (t::typ) --> new_tv m t";
+by (typ.induct_tac "t" 1);
(* case TVar n *)
by( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
(* case Fun t1 t2 *)
@@ -167,8 +167,8 @@
Addsimps [lessI RS less_imp_le RS new_tv_le];
goal thy
- "n<=m --> new_tv n (a::type_expr list) --> new_tv m a";
-by( list.induct_tac "a" 1);
+ "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
+by( list.induct_tac "ts" 1);
(* case [] *)
by(Simp_tac 1);
(* case a#al *)
@@ -195,25 +195,25 @@
qed "new_tv_subst_var";
goal thy
- "new_tv n s --> new_tv n (t::type_expr) --> new_tv n ($ s t)";
-by (type_expr.induct_tac "t" 1);
+ "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
+by (typ.induct_tac "t" 1);
by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
bind_thm ("new_tv_subst_te",result() RS mp RS mp);
Addsimps [new_tv_subst_te];
-goal thy
- "new_tv n s --> new_tv n (a::type_expr list) --> new_tv n ($ s a)";
+goal thy
+ "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
by( simp_tac (!simpset addsimps [new_tv_list]) 1);
-by (list.induct_tac "a" 1);
+by (list.induct_tac "ts" 1);
by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
bind_thm ("new_tv_subst_tel",result() RS mp RS mp);
Addsimps [new_tv_subst_tel];
(* auxilliary lemma *)
goal thy
- "new_tv n a --> new_tv (Suc n) ((TVar n)#a)";
+ "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
by( simp_tac (!simpset addsimps [new_tv_list]) 1);
-by (list.induct_tac "a" 1);
+by (list.induct_tac "ts" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "new_tv_Suc_list";
@@ -241,8 +241,8 @@
Addsimps [new_tv_not_free_tv];
goal thy
- "(t::type_expr) mem l --> free_tv t <= free_tv l";
-by (list.induct_tac "l" 1);
+ "(t::typ) mem ts --> free_tv t <= free_tv ts";
+by (list.induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
@@ -255,8 +255,8 @@
structure the substitutions coincide on the free type variables
occurring in the type structure *)
goal thy
- "$ s1 (t::type_expr) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (type_expr.induct_tac "t" 1);
+ "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
+by (typ.induct_tac "t" 1);
(* case TVar n *)
by (fast_tac (HOL_cs addss !simpset) 1);
(* case Fun t1 t2 *)
@@ -264,8 +264,8 @@
bind_thm ("eq_subst_te_eq_free",result() RS mp RS mp);
goal thy
- "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::type_expr) = $ s2 t";
-by (type_expr.induct_tac "t" 1);
+ "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
+by (typ.induct_tac "t" 1);
(* case TVar n *)
by (fast_tac (HOL_cs addss !simpset) 1);
(* case Fun t1 t2 *)
@@ -273,8 +273,8 @@
bind_thm ("eq_free_eq_subst_te",result() RS mp);
goal thy
- "$ s1 (l::type_expr list) = $ s2 l --> n:(free_tv l) --> s1 n = s2 n";
-by (list.induct_tac "l" 1);
+ "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
+by (list.induct_tac "ts" 1);
(* case [] *)
by (fast_tac (HOL_cs addss !simpset) 1);
(* case x#xl *)
@@ -282,8 +282,8 @@
bind_thm ("eq_subst_tel_eq_free",result() RS mp RS mp);
goal thy
- "(!n. n:(free_tv l) --> s1 n = s2 n) --> $s1 (l::type_expr list) = $s2 l";
-by (list.induct_tac "l" 1);
+ "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
+by (list.induct_tac "ts" 1);
(* case [] *)
by (fast_tac (HOL_cs addss !simpset) 1);
(* case x#xl *)
@@ -315,8 +315,8 @@
qed "free_tv_subst_var";
goal thy
- "free_tv ($ s (e::type_expr)) <= cod s Un free_tv e";
-by( type_expr.induct_tac "e" 1);
+ "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
+by( typ.induct_tac "t" 1);
(* case TVar n *)
by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
(* case Fun t1 t2 *)
@@ -324,8 +324,8 @@
qed "free_tv_app_subst_te";
goal thy
- "free_tv ($ s (l::type_expr list)) <= cod s Un free_tv l";
-by( list.induct_tac "l" 1);
+ "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
+by( list.induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case a#al *)
@@ -334,8 +334,7 @@
qed "free_tv_app_subst_tel";
goalw thy [free_tv_subst,dom_def]
- "free_tv (%u::nat. $ s1 ($ s2 (s3 u)) :: type_expr ) <= \
+ "free_tv (%u::nat. $ s1 ($ s2 (s3 u)) :: typ) <= \
\ free_tv s1 Un free_tv s2 Un free_tv s3";
by( fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,free_tv_subst_var RS subsetD] addss (!simpset addsimps [cod_def,dom_def])) 1);
qed "free_tv_comp_subst";
-
--- a/src/HOL/MiniML/Type.thy Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Type.thy Fri Dec 08 19:48:15 1995 +0100
@@ -14,14 +14,14 @@
(* type expressions *)
datatype
- type_expr = TVar nat | Fun type_expr type_expr
+ typ = TVar nat | "->" typ typ (infixr 70)
(* type variable substitution *)
types
- subst = nat => type_expr
+ subst = nat => typ
arities
- type_expr::type_struct
+ typ::type_struct
list::(type_struct)type_struct
fun::(term,type_struct)type_struct
@@ -39,7 +39,7 @@
rules
app_subst_TVar "$ s (TVar n) = s n"
- app_subst_Fun "$ s (Fun t1 t2) = Fun ($ s t1) ($ s t2)"
+ app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)"
defs
app_subst_list "$ s == map ($ s)"
@@ -49,7 +49,7 @@
rules
free_tv_TVar "free_tv (TVar m) = {m}"
- free_tv_Fun "free_tv (Fun t1 t2) = (free_tv t1) Un (free_tv t2)"
+ free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
free_tv_Nil "free_tv [] = {}"
free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)"
@@ -78,12 +78,12 @@
(* unification algorithm mgu *)
consts
- mgu :: [type_expr,type_expr] => subst maybe
+ mgu :: [typ,typ] => subst maybe
rules
- mgu_eq "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2"
- mgu_mg "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==>
- ? r. s = ($ r) o u"
- mgu_Ok "$ s t1 = $ s t2 ==> ? u. mgu t1 t2 = Ok u"
+ mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
+ mgu_mg "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
+ ? r. s = $r o u"
+ mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
end
--- a/src/HOL/MiniML/W.ML Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/W.ML Fri Dec 08 19:48:15 1995 +0100
@@ -37,7 +37,7 @@
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
by (rtac (app_subst_Fun RS subst) 1);
-by (res_inst_tac [("t","$ sc (Fun tb (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1);
+by (res_inst_tac [("t","$ sc (tb -> (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1);
by (Asm_full_simp_tac 1);
by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
@@ -255,7 +255,7 @@
by (eresolve_tac has_type_casesE 1);
by (eres_inst_tac [("x","s'")] allE 1);
by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","Fun t2 t'")] allE 1);
+by (eres_inst_tac [("x","t2 -> t'")] allE 1);
by (eres_inst_tac [("x","n")] allE 1);
by (safe_tac HOL_cs);
by (eres_inst_tac [("x","r")] allE 1);
@@ -275,10 +275,10 @@
"$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
\ else ra x)) ($ sa t) = \
\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
-\ else ra x)) (Fun ta (TVar ma))" 1);
+\ else ra x)) (ta -> (TVar ma))" 1);
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
\ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
- ("s","Fun ($ ra ta) t'")] ssubst 2);
+ ("s","($ ra ta) -> t'")] ssubst 2);
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
br eq_free_eq_subst_te 2;
by (strip_tac 2);
@@ -290,7 +290,7 @@
by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
setloop (split_tac [expand_if])) 3);
(* na : free_tv sa *)
-by (dres_inst_tac [("l1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
+by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
bd eq_subst_tel_eq_free 2;
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
by (Asm_simp_tac 2);
@@ -324,7 +324,7 @@
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
(* case na : free_tv t - free_tv sa *)
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
-by (dres_inst_tac [("l1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
+by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
bd eq_subst_tel_eq_free 2;
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2);
@@ -343,7 +343,7 @@
by (dres_inst_tac [("x","ma")] fun_cong 2);
by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
-by (res_inst_tac [("l2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN
+by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN
(2,trans)) 1);
by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
br eq_free_eq_subst_tel 1;
--- a/src/HOL/MiniML/W.thy Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/W.thy Fri Dec 08 19:48:15 1995 +0100
@@ -9,20 +9,20 @@
W = MiniML +
types
- result_W = "(subst * type_expr * nat)maybe"
+ result_W = "(subst * typ * nat)maybe"
(* type inference algorithm W *)
consts
- W :: [expr, type_expr list, nat] => result_W
+ W :: [expr, typ list, nat] => result_W
primrec W expr
W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
else Fail)"
- W_Abs "W (Abs e) a n = W e ((TVar n)#a) (Suc n) bind
- (%(s,t,m). Ok(s, Fun (s n) t, m) )"
+ W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
+ Ok(s, (s n) -> t, m) )"
W_App "W (App e1 e2) a n =
- W e1 a n bind
- (%(s1,t1,m1). W e2 ($ s1 a) m1 bind
- (%(s2,t2,m2). mgu ($ s2 t1) (Fun t2 (TVar m2)) bind
- (%u. Ok( ($ u) o (($ s2) o s1), $ u (TVar m2), Suc m2) )))"
+ ( (s1,t1,m1) := W e1 a n;
+ (s2,t2,m2) := W e2 ($ s1 a) m1;
+ u := mgu ($ s2 t1) (t2 -> (TVar m2));
+ Ok( ($ u) o (($ s2) o s1), $ u (TVar m2), Suc m2) )"
end