
diff -r d5713db7e146 -r dd7490fdd998 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Dec 19 07:50:37 2010 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 21 10:28:08 2010 +0000
@@ -116,7 +116,8 @@
 
 ML {*
 (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *)
-fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) =
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
+  (bclause as (BC (bmode, binders, bodies))) =
   case binders of
     [] => [] 
   | _ =>
@@ -133,37 +134,85 @@
 
         val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty]))
         val abs_lhs = abs $ binder_trm $ body_trm
-        val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0
-        val goal = HOLogic.mk_eq (abs_lhs, abs_rhs)
-          |> (fn t => HOLogic.mk_exists ("y", body_ty, t))
+        val abs_rhs = abs $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
+        val abs_rhs' = abs $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
+        val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
+        val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs')
+        val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
+
+        val goal = HOLogic.mk_conj (abs_eq, eq)
+          |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
           |> HOLogic.mk_Trueprop  
+
+        val goal' = HOLogic.mk_conj (abs_eq', eq)
+          |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
+          |> HOLogic.mk_Trueprop   
  
         val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
           @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
-          fresh_star_set} @ @{thms finite.intros finite_fset}  
+          fresh_star_set} @ @{thms finite.intros finite_fset}
      in
-       [Goal.prove ctxt [] [] goal
-          (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
-              THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] 
+       if is_recursive_binder bclause
+       then
+         (tracing "recursive";
+         [ Goal.prove ctxt [] [] goal'
+             (K (HEADGOAL (resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+                 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))
+           |> Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
+         ])
+       else
+         (tracing "non-recursive";
+         [ Goal.prove ctxt [] [] goal
+             (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
+                 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))
+           |> Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []
+         ]) 
      end
 *}
 
-
-(* FIXME: use pure cterm functions *)
 ML {*
-fun mk_cperm ctxt p ctrm =
-  mk_perm (term_of p) (term_of ctrm)
-  |> cterm_of (ProofContext.theory_of ctxt)
+fun conj_tac tac i =
+  let
+     fun select (t, i) =
+       case t of
+         @{term "Trueprop"} $ t' => select (t', i)
+       | @{term "op \<and>"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i
+       | _ => tac i
+  in
+    SUBGOAL select i
+  end
 *}
 
+ML {*
+fun is_abs_eq thm =
+  let
+    fun is_abs trm =
+      case (head_of trm) of
+        Const (@{const_name "Abs_set"}, _) => true
+      | Const (@{const_name "Abs_lst"}, _) => true
+      | Const (@{const_name "Abs_res"}, _) => true
+      | _ => false
+  in 
+    thm |> prop_of 
+        |> HOLogic.dest_Trueprop
+        |> HOLogic.dest_eq
+        |> fst
+        |> is_abs
+  end
+*}
+
+lemma setify:
+  shows "xs = ys \<Longrightarrow> set xs = set ys" 
+  by simp
 
 ML {*
-fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm =
+fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
+  (prems, bclausess) qexhaust_thm =
   let
     fun aux_tac prem bclauses =
       case (get_all_binders bclauses) of
         [] => EVERY' [rtac prem, atac]
-      | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} =>  
+      | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>  
           let
             val parms = map (term_of o snd) params
             val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
@@ -172,36 +221,76 @@
             val (([(_, fperm)], fprops), ctxt') = Obtain.result
               (K (EVERY1 [etac exE, 
                           full_simp_tac (HOL_basic_ss addsimps ss), 
-                          REPEAT o (etac conjE)])) [fthm] ctxt 
+                          REPEAT o (etac @{thm conjE})])) [fthm] ctxt 
   
-            val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses)
+            val abs_eq_thms = flat 
+             (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
+
+            val ((_, eqs), ctxt'') = Obtain.result
+              (K (EVERY1 
+                   [ REPEAT o (etac @{thm exE}), 
+                     REPEAT o (etac @{thm conjE}),
+                     REPEAT o (dtac @{thm setify}),
+                     full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' 
+
+            val (abs_eqs, peqs) = split_filter is_abs_eq eqs
+
+            val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
+            val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
 
-            val _ = tracing ("test")
-            (*
-            val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops))
-            *)    
-            (* 
-            val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs))
-            *)
+            val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem)
+            val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems))
+            val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'))
+            val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops''))
+            val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs))
+            val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs))
+              
+ 
+            val tac1 = EVERY'
+              [ simp_tac (HOL_basic_ss addsimps peqs),
+                rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
+                K (print_tac "before solving freshness"), 
+                conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ] 
+
+            val tac2 = EVERY' 
+              [ rtac (@{thm ssubst} OF prems),
+                rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
+                K (print_tac "before substituting"),
+                rewrite_goal_tac (map safe_mk_equiv abs_eqs),
+                K (print_tac "after substituting"),
+                conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)),
+                K (print_tac "end") 
+              ] 
+
+            val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
+              (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *)
+                       EVERY 
+                        [ rtac prem 1,
+                          print_tac "after applying prem",
+                          RANGE [SOLVED' tac1, SOLVED' tac2] 1,
+                          print_tac "final" ] )
+              |> singleton (ProofContext.export ctxt'' ctxt)  
+
+            val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm)
           in
-            (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*)
-            Skip_Proof.cheat_tac (ProofContext.theory_of ctxt')
+            rtac side_thm 1 
           end) ctxt
   in
-    rtac thm THEN' RANGE (map2 aux_tac prems bclausess)
+    rtac qexhaust_thm THEN' RANGE (map2 aux_tac prems bclausess)
   end
 *}
 
 
 ML {*
-fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms =
+fun prove_strong_exhausts lthy exhausts qtrms bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns 
+  perm_bn_alphas =
   let
-    val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy 
+    val ((_, exhausts'), lthy') = Variable.import true exhausts lthy 
 
     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c = Free (c, TFree (a, @{sort fs}))
 
-    val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *)
+    val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *)
       |> map prop_of
       |> map Logic.strip_horn
       |> split_list
@@ -215,7 +304,8 @@
            val prems' = partitions prems (map length bclausesss)
         in
           EVERY1 [Goal.conjunction_tac,
-            RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')]
+            RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) 
+                      (prems' ~~ bclausesss) exhausts')]
         end)
   end
 *}
@@ -582,7 +672,7 @@
   (* defining of quotient term-constructors, binding functions, free vars functions *)
   val _ = warning "Defining the quotient constants"
   val qconstrs_descrs =
-    map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs
+    (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs
 
   val qbns_descr =
     map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
@@ -734,7 +824,9 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
-  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms
+  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms qeq_iffs'
+    qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
+
 
   (* noting the theorems *)  
 
@@ -917,7 +1009,7 @@
     bcs @ (flat (map_range (add bcs) n))
   end
 in
-  map2 (map2 complt) args bclauses
+  (map2 o map2) complt args bclauses
 end
 *}
 




