# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1306958610 -3600
# Node ID 3b9ef98a03d2bd468d61511dd53649d807303279
# Parent  5ecb857e9de72b0357b445f7237507fa5d2ae4c2
first test to fix the problem with free variables

diff -r 5ecb857e9de7 -r 3b9ef98a03d2 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 16:13:42 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 21:03:30 2011 +0100
@@ -10,6 +10,15 @@
 | 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"
 where
@@ -451,10 +460,12 @@
   apply auto
   done
 
+(*
 lemma db_trans_test:
   assumes a: "y \<noteq> x"
   shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
   using a by simp
+*)
 
 abbreviation
   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
@@ -566,6 +577,7 @@
 
 text {* "HO" functions *}
 
+
 nominal_primrec
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
diff -r 5ecb857e9de7 -r 3b9ef98a03d2 Nominal/Ex/PaperTest.thy
--- a/Nominal/Ex/PaperTest.thy	Wed Jun 01 16:13:42 2011 +0900
+++ b/Nominal/Ex/PaperTest.thy	Wed Jun 01 21:03:30 2011 +0100
@@ -28,7 +28,7 @@
 fun
   usubst :: "utrm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> utrm"  ("_[_:::=_]" [100,100,100] 100)
 where
-  "(UVar x)[y:::=p] = (if x=y then UnPermute x p else (UVar x))"
+  "(UVar x)[y:::=p] = (if x=y then UnPermute p x else (UVar x))"
 | "(UApp t\<^isub>1 t\<^isub>2)[y:::=p] = UApp (t\<^isub>1[y:::=p]) (t\<^isub>2[y:::=p])"
 | "(ULam [x].t)[y:::=p] = (if x=y then (ULam [x].t) else ULam [x].(t[y:::=p]))"
 | "(UConst n)[y:::=p] = UConst n"
@@ -89,6 +89,29 @@
 | "\<parallel>(ULam [x].t)\<parallel> = Lam [x].(\<parallel>t\<parallel>)"
 | "\<parallel>(UApp t1 t2)\<parallel> = App (\<parallel>t1\<parallel>) (\<parallel>t2\<parallel>)"
 
+function
+  utrans :: "trm \<Rightarrow> utrm" ("\<lparr>_\<rparr>" [90] 100)
+where
+  "\<lparr>Var x\<rparr> = UVar x"
+| "\<lparr>Const x\<rparr> = UConst x"
+| "\<lparr>Lam [x].t\<rparr> = ULam [x].\<lparr>t\<rparr>"
+| "\<lparr>App (App (Const ''unpermute'') (Var p)) (Var x)\<rparr> = UnPermute p x"
+| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> \<lparr>App t1 t2\<rparr> = UApp (\<lparr>t1\<rparr>) (\<lparr>t2\<rparr>)"
+defer
+apply(simp_all)
+apply(auto)[1]
+apply(case_tac x)
+apply(simp_all)
+apply(auto)
+apply(blast)
+done
+
+termination
+  apply(relation "measure (\<lambda>t. size t)")
+  apply(simp_all)
+  done
+
+
 lemma elim1:
   "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')"
 apply(erule ufree.induct)
@@ -101,7 +124,7 @@
 apply(auto dest: elim1)
 done
 
-lemma
+lemma ss1:
   "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)"
 apply(erule ufree.induct)
 apply(simp_all)
@@ -111,6 +134,51 @@
 apply(auto)
 done
 
+lemma trans1:
+  shows "\<parallel>\<lparr>t\<rparr>\<parallel> = t"
+apply(induct t)
+apply(simp)
+apply(simp)
+prefer 2
+apply(simp)
+apply(case_tac "(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))")
+apply(erule exE)+
+apply(simp)
+apply(simp)
+done
+
+lemma trans_subst:
+  shows "\<lparr>t[x ::= p]\<rparr> = \<lparr>t\<rparr>[x :::= p]"
+apply(induct rule: subst.induct)
+apply(simp)
+defer
+apply(simp)
+apply(simp)
+apply(simp)
+apply(case_tac "(t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))")
+apply(erule exE)+
+apply(simp only:)
+apply(subst utrans.simps)
+apply(subst usubst.simps)
+apply(case_tac "xa = x")
+apply(subst (asm) subst.simps)
+apply(simp only:)
+apply(subst (asm) utrans.simps)
+apply(simp only: usubst.simps)
+apply(simp)
+apply(auto)[1]
+apply(case_tac "pa = x")
+apply(simp)
+prefer 2
+apply(simp)
+apply(simp)
+done
+
+lemma 
+  "ss (t[x ::= p]) = ss t"
+apply(subst (2) trans1[symmetric])
+apply(subst ss1[symmetric])
+
 
 fun
   fr :: "trm \<Rightarrow> name set"
diff -r 5ecb857e9de7 -r 3b9ef98a03d2 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Wed Jun 01 16:13:42 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Wed Jun 01 21:03:30 2011 +0100
@@ -124,8 +124,9 @@
   end
 
 (** building proof obligations *)
-fun mk_eqvt_proof_obligation qs fvar (_, assms, arg) = 
+fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 
   mk_eqvt_at (fvar, arg)
+  |> curry Term.list_all_free vs
   |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_abs_free qs
   |> strip_abs_body
@@ -265,12 +266,16 @@
     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
@@ -282,6 +287,7 @@
     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
@@ -336,7 +342,7 @@
     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
         (llRI RS ih_eqvt_case)
         |> fold_rev (Thm.implies_intr o cprop_of) CCas
-        (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *)
+        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs 
   in
     map prep_eqvt RCs
     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)