# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1306965314 -3600
# Node ID 04f7c4ce8588a08a65e8159532c4cf05d42af20f
# Parent  3b9ef98a03d2bd468d61511dd53649d807303279
hopefully final fix for ho-functions

diff -r 3b9ef98a03d2 -r 04f7c4ce8588 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 21:03:30 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 22:55:14 2011 +0100
@@ -10,14 +10,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
-nominal_primrec
-  Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
-where
-  "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
-unfolding eqvt_def Z_graph_def
-apply (rule, perm_simp, rule)
-oops
-
 
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
@@ -577,7 +569,6 @@
 
 text {* "HO" functions *}
 
-
 nominal_primrec
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
@@ -601,8 +592,6 @@
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
 unfolding eqvt_def Z_graph_def
 apply (rule, perm_simp, rule)
-prefer 2
-ML_prf {* prop_of (hd (#prems (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))))) *}
 oops
 
 (* function tests *)
diff -r 3b9ef98a03d2 -r 04f7c4ce8588 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 21:03:30 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 22:55:14 2011 +0100
@@ -428,6 +428,8 @@
   apply (simp add: alphas fresh_star_zero)
   apply auto[1]
   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
+oops
+(*
   apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
   apply (drule subsetD[OF supp_subst])
   apply auto[1]
@@ -444,7 +446,7 @@
   apply (simp add: fresh_star_def fresh_def)
   apply blast
   done
-
+*)
 
 text {* Some Tests about Alpha-Equality *}
 
diff -r 3b9ef98a03d2 -r 04f7c4ce8588 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Wed Jun 01 21:03:30 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Wed Jun 01 22:55:14 2011 +0100
@@ -126,8 +126,8 @@
 (** building proof obligations *)
 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 
   mk_eqvt_at (fvar, arg)
+  |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_all_free vs
-  |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_abs_free qs
   |> strip_abs_body
 
@@ -266,16 +266,12 @@
     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
 
     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
-
-    val _ = tracing ("eqvtsi\n" ^ cat_lines (map (Syntax.string_of_term_global thy o prop_of) eqvtsi))
-    val _ = tracing ("eqvtsj\n" ^ cat_lines (map (Syntax.string_of_term_global thy o prop_of) eqvtsj))
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-      |> tap (fn t => tracing ("1: " ^ Syntax.string_of_term_global thy (prop_of t)))
       |> fold Thm.elim_implies eqvtsj (* nominal *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
@@ -287,7 +283,6 @@
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      |> tap (fn t => tracing ("2: " ^ Syntax.string_of_term_global thy (prop_of t)))
       |> fold Thm.elim_implies eqvtsi  (* nominal *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj