# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308222745 -3600
# Node ID 25a7f421a3badb1c64169df9eb618721380c7584
# Parent  2eeb75cccb8d825324b06527f34f0f7b4662c348
added a test that every function must be of pt-sort

diff -r 2eeb75cccb8d -r 25a7f421a3ba Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Jun 16 11:03:01 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 16 12:12:25 2011 +0100
@@ -10,8 +10,9 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+text {* free name function *}
 
-text {* free name function - returns an atom list *}
+text {* first returns an atom list *}
 
 nominal_primrec 
   frees_lst :: "lam \<Rightarrow> atom list"
@@ -38,7 +39,7 @@
 lemma shows "supp t = set (frees_lst t)"
   by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
 
-text {* free name function - returns an atom set *}
+text {* second returns an atom set - therefore needs an invariant *}
 
 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "lam \<Rightarrow> atom set"
@@ -173,8 +174,6 @@
 apply(simp_all add: swap_fresh_fresh)
 done
 
-declare lam.size[simp]
-
 termination
   by lexicographic_order
 
@@ -362,7 +361,7 @@
 termination
   by lexicographic_order
 
-text {* count bound-variable occurences *}
+text {* count the bound-variable occurences in a lambda-term *}
 
 nominal_primrec
   cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
@@ -521,15 +520,15 @@
 (* function that evaluates a lambda term *)
 nominal_primrec
    eval :: "lam \<Rightarrow> lam" and
-   app :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+   apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 where
   "eval (Var x) = Var x"
 | "eval (Lam [x].t) = Lam [x].(eval t)"
-| "eval (App t1 t2) = sub (eval t1) (eval t2)"
-| "app (Var x) t2 = App (Var x) t2"
-| "app (App t0 t1) t2 = App (App t0 t1) t2"
-| "atom x \<sharp> t2 \<Longrightarrow> app (Lam [x].t1) t2 = eval (t1[x::= t2])"
-apply(simp add: eval_app_graph_def eqvt_def)
+| "eval (App t1 t2) = apply_subst (eval t1) (eval t2)"
+| "apply_subst (Var x) t2 = App (Var x) t2"
+| "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
+| "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
+apply(simp add: eval_apply_subst_graph_def eqvt_def)
 apply(rule, perm_simp, rule)
 apply(rule TrueI)
 apply (case_tac x)
@@ -551,7 +550,6 @@
 apply (simp add: fresh_Inl)
 apply (simp add: eqvt_at_def)
 apply simp
-defer
 apply clarify
 apply(erule Abs_lst1_fcb)
 apply (erule fresh_eqvt_at)
@@ -567,15 +565,20 @@
 apply assumption+
 apply rule
 apply simp
-oops (* can this be defined ? *)
-  (* Yes, if "sub" is a constant. *)
+done
+
+
+(* a small test
+termination sorry
 
-text {* TODO: nominal_primrec throws RSN if an argument is not in FS, but function works *}
-function q where
-  "q (Lam [x]. M) N = Lam [x]. (Lam [x]. (App M (q (Var x) N)))"
-| "q (Var x) N = Var x"
-| "q (App l r) N = App l r"
-oops
+lemma 
+  assumes "x \<noteq> y"
+  shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)"
+using assms
+apply(simp add: lam.supp fresh_def supp_at_base)
+done
+*)
+
 
 text {* TODO: eqvt_at for the other side *}
 nominal_primrec q where
diff -r 2eeb75cccb8d -r 25a7f421a3ba Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Thu Jun 16 11:03:01 2011 +0100
+++ b/Nominal/nominal_function.ML	Thu Jun 16 12:12:25 2011 +0100
@@ -45,6 +45,8 @@
 (* Check for all sorts of errors in the input - nominal needs a different checking function *)
 fun nominal_check_defs ctxt fixes eqs =
   let
+    val _ = tracing ("fixes: " ^ @{make_string} fixes)
+
     val fnames = map (fst o fst) fixes
 
     fun check geq =
@@ -68,7 +70,8 @@
           orelse input_error "Defined function may not occur in premises or arguments"
 
         val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
-        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
+        val funvars = filter (fn q => 
+          exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
         val _ = null funvars orelse (warning (cat_lines
           ["Bound variable" ^ plural " " "s " funvars ^
           commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
@@ -90,9 +93,9 @@
         plural " " "s " not_defined ^ commas_quote not_defined)
 
     fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, @{sort "pt"})
       orelse error (cat_lines
-      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
+      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":",
        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
 
     val _ = map check_sorts fixes
@@ -144,11 +147,7 @@
       empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
 
     val defname = mk_defname fixes
-    val NominalFunctionConfig {partials, default, ...} = config
-    val _ =
-      if is_some default then Output.legacy_feature
-        "'function (default)'. Use 'partial_function'."
-      else ()
+    val NominalFunctionConfig {partials, ...} = config
 
     val ((goal_state, cont), lthy') =
       Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy