# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281841393 -28800
# Node ID 107c06267f33f5a69bb46a65e9c6e1ddf3571d82
# Parent  1e616069054666e5440c76919f4fe9da8fc000e5
simplified code

diff -r 1e6160690546 -r 107c06267f33 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Aug 15 11:03:13 2010 +0800
@@ -10,6 +10,8 @@
 
   val dest_listT: typ -> typ
 
+  val size_const: typ -> term 
+
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -73,13 +75,15 @@
 fun dest_listT (Type (@{type_name list}, [T])) = T
   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
 
-fun mk_minus p = @{term "uminus::perm => perm"} $ p;
+fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
 
-fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;
+fun mk_minus p = @{term "uminus::perm => perm"} $ p
 
-fun perm_ty ty = @{typ "perm"} --> ty --> ty; 
-fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm;
-fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm;
+fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
+
+fun perm_ty ty = @{typ "perm"} --> ty --> ty
+fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t]);
diff -r 1e6160690546 -r 107c06267f33 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sun Aug 15 11:03:13 2010 +0800
@@ -85,8 +85,7 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-thm alpha_sym_thms
-thm funs_rsp
+
 thm distinct
 
 term TvsNil
diff -r 1e6160690546 -r 107c06267f33 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 15 11:03:13 2010 +0800
@@ -318,20 +318,18 @@
   val all_raw_ty_names = map (fst o dest_Type) all_raw_tys
   
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names  
-  val inject_thms = flat (map #inject dtinfos);
-  val distinct_thms = flat (map #distinct dtinfos);
-  val constr_thms = inject_thms @ distinct_thms
-  val rel_dtinfos = List.take (dtinfos, (length dts)); 
-  val raw_constrs_distinct = (map #distinct rel_dtinfos); 
+  val inject_thms = flat (map #inject dtinfos)
+  val distinct_thms = flat (map #distinct dtinfos)
+  val constr_thms = inject_thms @ distinct_thms 
+  
   val raw_induct_thm = #induct dtinfo;
   val raw_induct_thms = #inducts dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
-  val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys
+  val raw_size_trms = map size_const all_raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop
   
-
   (* definitions of raw permutations *)
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
@@ -366,8 +364,8 @@
 
   (* definition of alpha-distinct lemmas *)
   val _ = warning "Distinct theorems";
-  val (alpha_distincts, alpha_bn_distincts) = 
-    mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
+  val alpha_distincts = 
+    mk_alpha_distincts lthy4 alpha_cases distinct_thms alpha_trms all_raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
   (* they have a funny shape for the simplifier *)
@@ -563,7 +561,7 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
-      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =
diff -r 1e6160690546 -r 107c06267f33 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sun Aug 15 11:03:13 2010 +0800
@@ -11,8 +11,8 @@
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
 
-  val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> 
-    term list -> term list -> bn_info -> thm list * thm list
+  val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
+    term list -> typ list -> thm list
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> (thm list * thm list)
@@ -270,42 +270,41 @@
 
 (* transforms the distinctness theorems of the constructors 
    to "not-alphas" of the constructors *)
-fun mk_alpha_distinct_goal alpha neq =
+fun mk_distinct_goal ty_trm_assoc neq =
 let
   val (lhs, rhs) = 
     neq
     |> HOLogic.dest_Trueprop
     |> HOLogic.dest_not
     |> HOLogic.dest_eq
+  val ty = fastype_of lhs
 in
-  alpha $ lhs $ rhs
+  (lookup ty_trm_assoc ty) $ lhs $ rhs
   |> HOLogic.mk_not
   |> HOLogic.mk_Trueprop
 end
 
-fun distinct_tac cases distinct_thms =
-  rtac notI THEN' eresolve_tac cases 
+fun distinct_tac cases_thms distinct_thms =
+  rtac notI THEN' eresolve_tac cases_thms 
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
-fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
+
+fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
 let
-  val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
-  val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
-  val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
-in
-  Variable.export ctxt' ctxt nrels
-end
+  val ty_trm_assoc = alpha_tys ~~ alpha_trms
 
-fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
-let
-  val alpha_distincts = 
-    map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
-  val distinc_thms = map 
-  val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
-  val alpha_bn_distincts =  
-    map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms)
+  fun mk_alpha_distinct distinct_trm =
+  let
+    val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt
+    val goal = mk_distinct_goal ty_trm_assoc trm'
+  in
+    Goal.prove ctxt' [] [] goal 
+      (K (distinct_tac cases_thms distinct_thms 1))
+    |> singleton (Variable.export ctxt' ctxt)
+  end
+    
 in
-  (flat alpha_distincts, flat alpha_bn_distincts)
+  map (mk_alpha_distinct o prop_of) distinct_thms
 end
 
 
@@ -692,7 +691,7 @@
 end
 
 
-(* transformation of the natural rsp-lemmas into the standard form *)
+(* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma
   "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}