# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269073648 -3600
# Node ID c3dca6e600c865f2f6f2a6a9c75b31921d18deaf
# Parent  604c4cffc5b9b1d7b45c269db56ec2b9ff89c4e5
Use 'alpha_bn_refl' to get rid of one of the sorrys.

diff -r 604c4cffc5b9 -r c3dca6e600c8 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Sat Mar 20 08:56:07 2010 +0100
+++ b/Nominal/LFex.thy	Sat Mar 20 09:27:28 2010 +0100
@@ -6,7 +6,7 @@
 atom_decl ident
 
 ML {* val _ = cheat_fv_rsp := false *}
-ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_alpha_bn_rsp := false *}
 ML {* val _ = cheat_equivp := false *}
 
 nominal_datatype kind =
diff -r 604c4cffc5b9 -r c3dca6e600c8 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Sat Mar 20 08:56:07 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 20 09:27:28 2010 +0100
@@ -267,7 +267,7 @@
 
 (* These 2 are critical, we don't know how to do it in term5 *)
 ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
-ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
 
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
@@ -363,10 +363,13 @@
   val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-  fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-    else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
-  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
+  val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;
+  fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1
+  fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x
+  val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    const_rsp_tac) raw_consts lthy11
+  val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    alpha_bn_rsp_tac) alpha_ts_bn lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
diff -r 604c4cffc5b9 -r c3dca6e600c8 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Sat Mar 20 08:56:07 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 20 09:27:28 2010 +0100
@@ -95,18 +95,15 @@
 *}
 
 ML {*
-fun constr_rsp_tac inj rsp equivps =
-let
-  val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
-in
+fun constr_rsp_tac inj rsp =
   REPEAT o rtac impI THEN'
   simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
-   rtac @{thm exI[of _ "0 :: perm"]} THEN'
-   asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+   REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
+   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+   asm_full_simp_tac (HOL_ss addsimps (rsp @
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
-end
 *}
 
 (* Testing code
diff -r 604c4cffc5b9 -r c3dca6e600c8 Nominal/TySch.thy
--- a/Nominal/TySch.thy	Sat Mar 20 08:56:07 2010 +0100
+++ b/Nominal/TySch.thy	Sat Mar 20 09:27:28 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 
 ML {* val _ = cheat_fv_rsp := false *}
-ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_alpha_bn_rsp := false *}
 ML {* val _ = cheat_equivp := false *}
 
 nominal_datatype t =
diff -r 604c4cffc5b9 -r c3dca6e600c8 TODO
--- a/TODO	Sat Mar 20 08:56:07 2010 +0100
+++ b/TODO	Sat Mar 20 09:27:28 2010 +0100
@@ -24,10 +24,10 @@
 
 - strong induction rules
 
-- show support equations
+- check support equations for more bindings per constructor
 
 - automate the proofs that are currently proved with sorry:
-  alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
+  alpha_equivp, fv_rsp, alpha_bn_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these