# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268306784 -3600
# Node ID 947e5f772a9c02b10597f387848fd3a045765fa8
# Parent  6e856be26ac70a07c2a49167ca5e77c8e360e595
Lifting constants.

diff -r 6e856be26ac7 -r 947e5f772a9c Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 11:41:27 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 12:26:24 2010 +0100
@@ -271,7 +271,11 @@
 
 ML {* val restricted_nominal=ref 0 *}
 ML {* val cheat_alpha_eqvt = ref true *}
-ML {* val cheat_fv_eqvt = ref true *}
+ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *)
+ML {* val cheat_fv_rsp = ref true *}
+ML {* val cheat_const_rsp = ref true *}
+
+ML {* unsuffix "sdf" "aasdf" *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -306,8 +310,10 @@
   val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
+  val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
+  val fv_ts_nobn = List.take (fv_ts, length perms)
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
-  val alpha_ts_nobn = List.take (alpha_ts, length perms)
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_induct_loc = #induct alpha
   val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
@@ -351,22 +357,20 @@
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
   val (consts, const_defs) = split_list consts_defs;
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
-else
-let
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
-  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts
-    (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9;
-  val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10
-  val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms
-    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11;
-  val qfv_names = map (fn x => "fv_" ^ x) qty_names
+  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+    else fvbv_rsp_tac alpha_induct fv_def 1;
+  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_inj (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 qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
   val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
@@ -374,6 +378,11 @@
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
+in
+if !restricted_nominal = 0 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy13)
+else
+let
   val q_name = space_implode "_" qty_names;
   val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
@@ -486,7 +495,7 @@
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
        Free (x, _) => (NONE, env_lookup env x)
-     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), false), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) = 
diff -r 6e856be26ac7 -r 947e5f772a9c Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu Mar 11 11:41:27 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 12:26:24 2010 +0100
@@ -87,13 +87,18 @@
 *}
 
 ML {*
+  fun all_eqvts ctxt =
+    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
+  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+ML {*
 fun constr_rsp_tac inj rsp equivps =
 let
   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
 in
   REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
+  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 @
@@ -134,7 +139,7 @@
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
+  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
   fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
@@ -153,11 +158,6 @@
 apply (rule_tac x="pi \<bullet> pia" in exI)
 by auto
 
-ML {*
-  fun all_eqvts ctxt =
-    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
 
 ML {*
 fun mk_minimal_ss ctxt =
diff -r 6e856be26ac7 -r 947e5f772a9c Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 11 11:41:27 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 11 12:26:24 2010 +0100
@@ -28,7 +28,7 @@
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
-thm fv_lam_raw_fv_bp_raw.simps[no_vars]
+(*thm fv_lam_raw_fv_bp_raw.simps[no_vars]*)
 
 text {* example 2 *}
 
@@ -57,7 +57,7 @@
 
 
 thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars]
-thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
+(*thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]*)
 thm f_raw.simps
 (*thm trm'_pat'_induct
 thm trm'_pat'_perm
@@ -90,8 +90,8 @@
 text {* example type schemes *}
 
 nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
+  VarTS "name"
+| FunTS "t" "t"
 and  tyS =
   All xs::"name set" ty::"t" bind xs in ty