# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1296155953 -3600
# Node ID eb4a2f4078ae162060f37d1e0b288b188b0fadaf
# Parent  5964c84ece5d7a6bfcc0ce35532af2444b512671
some experiments

diff -r 5964c84ece5d -r eb4a2f4078ae Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Jan 27 04:24:17 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jan 27 20:19:13 2011 +0100
@@ -4,6 +4,42 @@
 
 section {*** Type Schemes ***}
 
+nominal_datatype 
+  A = Aa bool | Ab B
+and 
+  B = Ba bool | Bb A
+
+lemma
+  "(p \<bullet> (Sum_Type.Projl (f (Inl x)))) = Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> x)))"
+apply(perm_simp)
+apply(subst permute_fun_def)
+sorry
+
+
+nominal_primrec
+    even :: "nat \<Rightarrow> A"
+and odd  :: "nat \<Rightarrow> B"
+where
+  "even 0 = Aa True"
+| "even (Suc n) = Ab (odd n)"
+| "odd 0 = Ba False"
+| "odd (Suc n) = Bb (even n)"
+thm even_odd_graph.intros even_odd_sumC_def
+thm sum.cases Product_Type.split
+thm even_odd_graph_def 
+term Inr
+term Sum_Type.Projr
+term even_odd_sumC
+thm even_odd_sumC_def
+unfolding even_odd_sumC_def
+sorry
+
+ML {* the *}
+
+thm even.psimps odd.psimps
+
+
+
 atom_decl name 
 
 (* defined as a single nominal datatype *)
@@ -40,6 +76,24 @@
 apply(simp_all)
 done
 
+lemma test:
+  assumes a: "f x = Inl y"
+  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
+using a 
+apply(frule_tac p="p" in permute_boolI)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst (asm) permute_fun_app_eq)
+back
+apply(simp)
+done
+
+lemma
+  "(p \<bullet> (Sum_Type.Projl x)) = Sum_Type.Projl (p \<bullet> x)"
+apply(case_tac x)
+apply(simp)
+apply(simp)
+
+
 nominal_primrec
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
@@ -47,7 +101,9 @@
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
+
 term subst_substs_sumC
+thm subst_substs_sumC_def
 term Inl
 thm subst_substs_graph.induct
 thm subst_substs_graph.intros
@@ -73,12 +129,123 @@
 apply(erule subst_substs_graph.induct)
 apply(perm_simp)
 apply(rule subst_substs_graph.intros)
+thm subst_substs_graph.cases
+apply(erule subst_substs_graph.cases)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst test)
+back
+apply(assumption)
+apply(rotate_tac 1)
+apply(erule subst_substs_graph.cases)
+apply(subst test)
+back
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(subst test)
+back
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(simp)
+--"A"
+apply(simp (no_asm_use) only: eqvts)
+apply(subst test)
+back
+apply(assumption)
+apply(rotate_tac 1)
+apply(erule subst_substs_graph.cases)
+apply(subst test)
+back
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(subst test)
+back
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(simp)
+--"A"
+apply(simp)
+apply(erule subst_substs_graph.cases)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst test)
+back
+back
+apply(assumption)
+apply(rule subst_substs_graph.intros)
+defer
+apply(perm_simp)
+apply(assumption)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst test)
+back
+back
+apply(assumption)
+apply(rule subst_substs_graph.intros)
+defer
+apply(perm_simp)
+apply(assumption)
+apply(simp)
+apply(simp_all add: ty_tys.distinct)
+defer
+apply(simp add: ty_tys.eq_iff)
+apply(simp add: ty_tys.eq_iff)
+apply(erule conjE)+
+apply(simp add: ty_tys.eq_iff)
+apply(subst (asm) Abs_eq_iff2)
+apply(erule exE)
+apply(simp add: alphas)
+apply(clarify)
+thm subst_def
+
+
+apply(assumption)
+apply(subst test)
+back
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(subst test)
+back
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(simp)
+
+
+apply(rotate_tac 1)
+apply(erule subst_substs_graph.cases)
+apply(subst test)
+back
+apply(assumption)
+
+
+apply(auto)[4]
+thm  subst_substs_graph.cases
+thm subst_substs_graph.intros
+thm subst_substs_graph.intros(2)[THEN permute_boolI]
+term subst_substs_graph
 apply(simp only: eqvts)
 thm Projl.simps
 term Inl
 term Inr
 apply(perm_simp)
 thm subst_substs_graph.intros
+apply(simp add: permute_fun_def)
 thm Projl.simps
 oops
 
diff -r 5964c84ece5d -r eb4a2f4078ae Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Thu Jan 27 04:24:17 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Thu Jan 27 20:19:13 2011 +0100
@@ -482,6 +482,9 @@
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
+ 
+    val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm)
+    val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
 
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses