# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271018929 -7200
# Node ID 894930834ca874ebda3ba8b97872bcb82b721f86
# Parent  08e4d3cbcf8c4318b9e74465ff8b44cd17ec88a4
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _

diff -r 08e4d3cbcf8c -r 894930834ca8 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 22:48:49 2010 +0200
@@ -1,8 +1,9 @@
 (*  Title:      Nominal2_Eqvt
-    Authors:    Brian Huffman, Christian Urban
+    Author:     Brian Huffman, 
+    Author:     Christian Urban
 
     Equivariance, Supp and Fresh Lemmas for Operators. 
-    (Contains most, but not all such lemmas.)
+    (Contains many, but not all such lemmas.)
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base Nominal2_Atoms
@@ -10,6 +11,14 @@
      ("nominal_permeq.ML")
 begin
 
+lemma r: "x = x"
+apply(auto)
+done
+
+ML {*
+  prop_of @{thm r}
+*}
+
 section {* Logical Operators *}
 
 lemma eq_eqvt:
diff -r 08e4d3cbcf8c -r 894930834ca8 Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Sun Apr 11 22:48:49 2010 +0200
@@ -71,7 +71,6 @@
   Conv.no_conv ctrm
 end
 
-
 (* conversion for applications: 
    only applies the conversion, if the head of the
    application is not a "bad head" *)
@@ -132,8 +131,8 @@
     then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
     else Conv.first_conv
 
-  val pre_thms = (map safe_mk_equiv user_thms) @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt)
-  val post_thms = @{thms permute_pure[THEN eq_reflection]}
+  val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
+  val post_thms = map safe_mk_equiv @{thms permute_pure}
 in
   first_conv_wrapper
     [ More_Conv.rewrs_conv pre_thms,
diff -r 08e4d3cbcf8c -r 894930834ca8 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Sun Apr 11 22:48:49 2010 +0200
@@ -38,6 +38,8 @@
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
 struct
 
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 structure EqvtData = Generic_Data
 ( type T = thm Item_Net.T;
@@ -66,16 +68,16 @@
 fun add_raw_thm thm = 
 let
   val trm = prop_of thm
-  val _ = if is_equiv trm then () 
-    else raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 in
-  (EqvtRawData.map o Item_Net.update) thm
+  if is_equiv trm 
+  then (EqvtRawData.map o Item_Net.update) thm
+  else raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 end
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
-  | dest_perm t = raise TERM("dest_perm", [t])
+  | dest_perm t = raise TERM ("dest_perm", [t])
 
 fun mk_perm p trm =
 let
@@ -90,11 +92,12 @@
    rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
 
 (* transform equations into the "p o c = c"-form *)
-fun transform_eq ctxt thm lhs rhs = 
+fun transform_eq ctxt thm = 
 let
+  val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
   val (p, t) = dest_perm lhs
   val (c, args) = strip_comb t
-  val (c', args') = strip_comb rhs 
+  val (c', args') = strip_comb rhs
   val eargs = map Envir.eta_contract args 
   val eargs' = map Envir.eta_contract args'
   val p_str = fst (fst (dest_Var p))
@@ -113,15 +116,12 @@
 fun transform addel_fun thm context = 
 let
   val ctxt = Context.proof_of context
-  val trm = HOLogic.dest_Trueprop (prop_of thm)
 in
-  case trm of
-    Const (@{const_name "op ="}, _) $ lhs $ rhs =>
-      let 
-        val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
-      in
-        addel_fun thm' context
-      end
+  case (prop_of thm) of
+    @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) =>
+      addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
+  | @{const "==>"} $ _ $ _ => 
+      error ("not yet implemented")
   | _ => raise (error "only (op=) case implemented yet")
 end 
 
diff -r 08e4d3cbcf8c -r 894930834ca8 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Sun Apr 11 22:48:49 2010 +0200
@@ -107,7 +107,12 @@
 
 nominal_datatype ty =
   TVar string
-| TFun ty ty ("_ \<rightarrow> _")
+| TFun ty ty
+
+notation
+ TFun ("_ \<rightarrow> _") 
+
+declare ty.perm[eqvt]
 
 inductive
   valid :: "(name \<times> ty) list \<Rightarrow> bool"
@@ -128,7 +133,7 @@
 *}
 
 
-lemma
+lemma 
   assumes a: "valid Gamma" 
   shows "valid (p \<bullet> Gamma)"
 using a
@@ -137,6 +142,31 @@
 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
 done
 
+lemma
+  "(p \<bullet> valid) = valid"
+oops
+
+lemma temp[eqvt_raw]: 
+  "(p \<bullet> valid) \<equiv> valid"
+sorry
+
+inductive
+  typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
+where
+    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
+  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+  | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
+
+lemma
+  assumes a: "Gamma \<turnstile> t : T" 
+  shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
+using a
+apply(induct)
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+done
+
 declare permute_lam_raw.simps[eqvt]
 
 thm alpha_gen_real_eqvt[no_vars]
@@ -173,6 +203,30 @@
 apply(perm_simp permute_minus_cancel(2))
 oops
 
+thm alpha_lam_raw.intros[no_vars]
+
+inductive
+ alpha_lam_raw'
+where
+  "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
+| "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
+   alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
+| "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
+   alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
+
+lemma
+  assumes a: "alpha_lam_raw' t1 t2"
+  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
+using a
+apply(induct)
+apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *})
+apply(perm_strict_simp)
+apply(rule alpha_lam_raw'.intros)
+apply(simp add: alphas)
+apply(rule_tac p="- p" in permute_boolE)
+apply(perm_simp permute_minus_cancel(2))
+oops
 
 
 section {* size function *}