--- a/ProgTutorial/Essential.thy	Mon May 31 22:43:31 2010 +0200
+++ b/ProgTutorial/Essential.thy	Mon May 31 23:29:06 2010 +0200
@@ -982,7 +982,7 @@
   @{ML_response [display, gray]
   "let
   val trm_list = 
-        [@{term_pat \"?X\"},              @{term_pat \"a\"},
+        [@{term_pat \"?X\"}, @{term_pat \"a\"},
          @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
          @{term_pat \"\<lambda>a b. (op +) a b\"},
          @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
@@ -1024,6 +1024,106 @@
   "Envir.type_env"}. An assumption of this function is that the terms to be
   unified have already the same type. In case of failure, the exceptions that
   are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
+*}
+
+(*
+ML {*
+  fun patunif_in_emptyenv (t, u) =
+    let
+      val init = Envir.empty 0;
+      val env = Pattern.unify @{theory} (t, u) init;
+    in
+      (env |> Envir.term_env |> Vartab.dest,
+       env |> Envir.type_env |> Vartab.dest)
+    end
+*}
+
+text {*
+@{ML_response [display, gray]
+ "val t1 = @{term_pat \"(% x y. ?f y x)\"};
+ val u1 = @{term_pat \"z::bool\"};
+   (* type conflict isnt noticed *)
+ patunif_in_emptyenv (t1, u1);"
+ "check missing"
+*}
+@{ML_response [display, gray] 
+ "val t2 = @{term_pat \"(% y. ?f y)\"} |> Term.strip_abs_body;
+ val u2 = @{term_pat \"z::bool\"};
+   (* fails because of loose bounds *)
+ (* patunif_in_emptyenv (t2, u2) *)"
+ "check missing"
+*}
+@{ML_response [display, gray]
+ "val t3 = @{term_pat \"(% y. plu (?f y) (% x. g x))\"};
+ val u3 = @{term_pat \"(% y. plu y (% x. g x))\"};
+   (* eta redexe im term egal, hidden polym wird inst *)
+ patunif_in_emptyenv (t3, u3)"
+ "check missing"
+*}
+@{ML_response [display, gray] 
+ "val t4 = @{term_pat \"(% y. plu (?f y) ((% x. g x) k))\"};
+ val u4 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
+   (* beta redexe are largely ignored, hidden polymorphism is instantiated *)
+ patunif_in_emptyenv (t4, u4)"
+ "check missing"
+*}
+@{ML_response [display, gray]
+ "val t5 = @{term_pat \"(% y. plu ((% x. ?f) y) ((% x. g x) k))\"};
+ val u5 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
+   (* fails: can't have beta redexes which seperate a var from its arguments *)
+ (* patunif_in_emptyenv (t5, u5) *)"
+*}
+
+@{ML_response [display, gray] 
+ "val t6 = @{term_pat \"(% x y. ?f x y) a b\"};
+ val u6 = @{term_pat \"c\"};
+ (* Pattern.pattern assumes argument is beta-normal *)
+ Pattern.pattern t6; 
+   (* fails: can't have beta redexes which seperate a var from its arguments,
+       otherwise this would be general unification for general a,b,c *)
+ (* patunif_in_emptyenv (t6, u6) *)"
+*}
+@{ML_response [display, gray]
+ "val t7 = @{term_pat \"(% y. plu ((% x. ?f x) y) ((% x. g x) k))\"};
+ val u7 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
+   (* eta redexe die Pattern trennen brauchen nicht normalisiert sein *)
+ patunif_in_emptyenv (t7, u7)"
+*}
+@{ML_response [display, gray] 
+ "val t8 = @{term_pat \"(% y. ?f y)\"};
+ val u8 = @{term_pat \"(% y. y ?f)\"};
+   (* variables of the same name are identified *)
+ (* patunif_in_emptyenv (t8, u8) *)"
+*}
+
+@{ML_response [display, gray]
+ "val t9 = @{term_pat \"(% y. ?f y)\"};
+ val u9 = @{term_pat \"(% y. ?f y)\"};
+   (* trivial solutions are empty and don't contain ?f = ?f etc *)
+ patunif_in_emptyenv (t9, u9)"
+*}
+@{ML_response [display, gray] 
+ "val t10 = @{term_pat \"(% y. (% x. ?f x) y)\"};
+ val u10 = @{term_pat \"(% y. ?f y)\"};
+   (* trivial solutions are empty and don't contain ?f = ?f etc *)
+ patunif_in_emptyenv (t10, u10)"
+*}
+@{ML_response [display, gray]
+ "val t11 = @{term_pat \"(% z. ?f z)\"};
+ val u11 = @{term_pat \"(% z. k (?f z))\"};
+   (* fails: occurs check *)
+ (* patunif_in_emptyenv (t11, u11) *)"
+*}
+@{ML_response [display, gray]
+ "val t12 = @{term_pat \"(% z. ?f z)\"};
+ val u12 = @{term_pat \"?g a\"};
+   (* fails: *both* terme have to be higher-order patterns *)
+ (* patunif_in_emptyenv (t12, u12) *)"
+*}
+*}
+*)
+
+text {*
 
   As mentioned before, unrestricted higher-order unification, respectively
   unrestricted higher-order matching, is in general undecidable and might also