
diff -r 16896fd8eff5 -r 7c5bca978886 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Sat Jan 15 21:16:15 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Mon Jan 17 12:33:37 2011 +0000
@@ -9,86 +9,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l
 
-definition
- "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
-
-lemma supp_eqvt_at:
-  assumes asm: "eqvt_at f x"
-  and     fin: "finite (supp x)"
-  shows "supp (f x) \<subseteq> supp x"
-apply(rule supp_is_subset)
-unfolding supports_def
-unfolding fresh_def[symmetric]
-using asm
-apply(simp add: eqvt_at_def)
-apply(simp add: swap_fresh_fresh)
-apply(rule fin)
-done
-
-lemma finite_supp_eqvt_at:
-  assumes asm: "eqvt_at f x"
-  and     fin: "finite (supp x)"
-  shows "finite (supp (f x))"
-apply(rule finite_subset)
-apply(rule supp_eqvt_at[OF asm fin])
-apply(rule fin)
-done
-
-lemma fresh_eqvt_at:
-  assumes asm: "eqvt_at f x"
-  and     fin: "finite (supp x)"
-  and     fresh: "as \<sharp>* x"
-  shows "as \<sharp>* f x"
-using fresh
-unfolding fresh_star_def
-unfolding fresh_def
-using supp_eqvt_at[OF asm fin]
-by auto
-
-definition
- "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
-
-lemma eqvtI:
-  "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
-apply(auto simp add: eqvt_def)
-done
-
-lemma the_default_eqvt:
-  assumes unique: "\<exists>!x. P x"
-  shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))"
-  apply(rule THE_default1_equality [symmetric])
-  apply(rule_tac p="-p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel)
-  apply(rule unique)
-  apply(rule_tac p="-p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel)
-  apply(rule THE_defaultI'[OF unique])
-  done
-
-lemma fundef_ex1_eqvt:
-  fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes eqvt: "eqvt G"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
-  apply (simp only: f_def)
-  apply(subst the_default_eqvt)
-  apply (rule ex1)
-  apply(perm_simp)
-  using eqvt
-  apply(simp add: eqvt_def)
-  done
-
-lemma fundef_ex1_eqvt_at:
-  fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes eqvt: "eqvt G"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "eqvt_at f x"
-  unfolding eqvt_at_def
-  using assms
-  apply(auto intro: fundef_ex1_eqvt)
-  done
 
 ML {*
 
@@ -333,33 +253,6 @@
 *}
 
 ML {*
-fun pp_thm thm =
-  let
-    val hyps = Thm.hyps_of thm
-    val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of thm)
-  in
-      (@{make_string} thm) ^ "\n    hyps: " ^ (commas (map (Syntax.string_of_term @{context}) hyps))
-      ^ "    tpairs: " ^   (commas (map (Syntax.string_of_term @{context}) tpairs))
-  end
-*}
-
-
-ML {*
-fun eqvt_at_elim thy (eqvts:thm list) thm =
-  case (prop_of thm) of
-    Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ => 
-      let
-        val el_thm = Skip_Proof.make_thm thy t
-        val _ = tracing ("NEED TO PROVE  " ^ @{make_string} el_thm)
-        val _ = tracing ("HAVE\n" ^ cat_lines (map @{make_string} eqvts))
-      in
-        Thm.elim_implies el_thm thm 
-        |> eqvt_at_elim thy eqvts 
-      end
-  | _ => thm
-*}
-
-ML {*
 (* expects i <= j *)
 fun lookup_compat_thm i j cts =
   nth (nth cts (i - 1)) (j - i)
@@ -375,12 +268,10 @@
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts
-      val _ = tracing ("XXXX compat clause if:\n" ^ @{make_string} compat)
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.elim_implies (rev eqvtsj) (* HERE *)
-      (*|> eqvt_at_elim thy eqvtsj *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
       |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
@@ -388,12 +279,10 @@
     else
     let
       val compat = lookup_compat_thm i j cts
-      (* val _ = tracing ("XXXX compat clause else:\n" ^ @{make_string} compat) *)
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.elim_implies (rev eqvtsi)  (* HERE *)
-      (* |> eqvt_at_elim thy eqvtsi *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -462,10 +351,9 @@
 ML {*
 fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
   let
-    val _ = tracing "START"
-
     val Globals {h, y, x, fvar, ...} = globals
-    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ags = agsi, ...}, ...} = clausei
+    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, 
+      ags = agsi, ...}, ...} = clausei
     val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
 
     val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
@@ -480,8 +368,6 @@
     val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 
 
-    val _ = tracing "POINT B"
-
     val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
 
     val RLj_import = RLj
@@ -489,64 +375,38 @@
       |> fold Thm.elim_implies agsj'
       |> fold Thm.elim_implies Ghsj'
 
-    val _ = tracing "POINT C"
- 
     val eqvtsi = nth eqvts (i - 1)
       |> map (fold Thm.forall_elim cqsi)
       |> map (fold Thm.elim_implies [case_hyp])
       |> map (fold Thm.elim_implies agsi)
 
-    val _ = tracing "POINT D"
-
     val eqvtsj = nth eqvts (j - 1)
-      |> tap (fn thms => tracing ("O1:\n" ^ cat_lines (map @{make_string} thms)))
       |> map (fold Thm.forall_elim cqsj')
-      |> tap (fn thms => tracing ("O2:\n" ^ cat_lines (map @{make_string} thms)))
       |> map (fold Thm.elim_implies [case_hypj'])
-      |> tap (fn thms => tracing ("O3:\n" ^ cat_lines (map @{make_string} thms)))
       |> map (fold Thm.elim_implies agsj')
 
-    val _ = tracing ("eqvtsi:\n" ^ cat_lines (map @{make_string} eqvtsi))
-    val _ = tracing ("eqvtsj:\n" ^ cat_lines (map @{make_string} eqvtsj))
-    val _ = tracing ("case_hypi:\n" ^ @{make_string} case_hyp)
-    val _ = tracing ("case_hypj:\n" ^ @{make_string} case_hypj')
-
     val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj
-    
-    val _ = tracing ("compats:\n" ^ pp_thm compat) 
-    
 
-    fun pppp str = tap (fn thm => tracing (str ^ ": " ^ pp_thm thm))
-    fun ppp str = I
   in
     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
-    |> pppp "A"
     |> Thm.implies_elim RLj_import
       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
-    |> pppp "B"
     |> (fn it => trans OF [it, compat])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
-    |> pppp "C"
     |> (fn it => trans OF [y_eq_rhsj'h, it])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
-    |> pppp "D"
     |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
-    |> pppp "E"
     |> fold_rev (Thm.implies_intr o cprop_of) agsj'
       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
-    |> pppp "F"
     |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
-    |> pppp "G"
     |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
-    |> pppp "H"
     |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
-    |> pppp "I"
   end
 *}
 
 
 ML {*
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas eqvt_lemmas clausei =
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =
   let
     val Globals {x, y, ranT, fvar, ...} = globals
     val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
@@ -565,9 +425,7 @@
     val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
     val unique_clauses =
-      map2 (mk_uniqueness_clause thy globals compat_store eqvt_lemmas clausei) clauses rep_lemmas
-
-    val _ = tracing ("DONE unique clauses") 
+      map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems
 
     fun elim_implies_eta A AB =
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
@@ -605,9 +463,6 @@
 *}
 
 
-ML {* (ex1_implies_ex, ex1_implies_un) *}
-thm fundef_ex1_eqvt_at
-
 ML {*
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =
   let
@@ -627,13 +482,6 @@
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
 
-    (*
-    val _ = tracing ("ihyp_thm\n" ^ pp_thm ihyp_thm)
-    val _ = tracing ("ih_intro\n" ^ pp_thm ih_intro)
-    val _ = tracing ("ih_elim\n" ^ pp_thm ih_elim)
-    val _ = tracing ("ih_eqvt\n" ^ pp_thm ih_eqvt)
-    *)
-
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
 
@@ -666,10 +514,9 @@
 *}
 
 
-
 ML {*
 (* wrapper -- restores quantifiers in rule specifications *)
-fun inductive_def (binding as ((R, T), _)) intrs lthy =
+fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy =
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
@@ -689,8 +536,14 @@
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
-    val eqvt_thm' = (Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI}
+    val eqvt_thm' = 
+      if eqvt_flag = false then NONE
+      else 
+        let
+          val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
+        in
+          SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})
+        end
 
     val cert = cterm_of (ProofContext.theory_of lthy)
     fun requantify orig_intro thm =
@@ -730,7 +583,7 @@
 
     val G_intros = map2 mk_GIntro clauses RCss
   in
-    inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
+    inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy
   end
 *}
 
@@ -762,10 +615,10 @@
 
     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
-    val ((R, RIntro_thms, R_elim, _, R_eqvt), lthy) =
-      inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+    val ((R, RIntro_thms, R_elim, _, _), lthy) =
+      inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy
   in
-    ((R, Library.unflat R_intross RIntro_thms, R_elim, R_eqvt), lthy)
+    ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
   end
 
 
@@ -1145,39 +998,18 @@
     val trees = map build_tree clauses
     val RCss = map find_calls trees
 
-    val ((G, GIntro_thms, G_elim, G_induct, G_eqvt), lthy) =
+    val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) =
       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
-    (* 
-    val _ = tracing ("Graph - name: " ^ pp_thm G)
-    val _ = tracing ("Graph intros:\n" ^ cat_lines (map pp_thm GIntro_thms))
-    val _ = tracing ("Graph Equivariance " ^ pp_thm G_eqvt)
-    *)
-
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
-    (*
-    val _ = tracing ("f - name: " ^ pp_thm f)
-    val _ = tracing ("f_defthm:\n" ^ pp_thm f_defthm)
-    *)
-
     val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
     val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
 
-    (*
-    val _ = tracing ("recursive calls:\n" ^ cat_lines (map pp_thm RCss))
-    *)
-
-    val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) =
+    val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 
-    (*
-    val _ = tracing ("Relation - name: " ^ pp_thm R) 
-    val _ = tracing ("Relation intros:\n" ^ cat_lines (map pp_thm RIntro_thmss))
-    val _ = tracing ("Relation Equivariance " ^ pp_thm R_eqvt)
-    *)    
-
     val (_, lthy) =
       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 
@@ -1199,13 +1031,6 @@
 
     val compat_store = store_compat_thms n compat
 
-    (*
-    val _ = tracing ("globals:\n" ^ pp_thm globals)
-    val _ = tracing ("complete:\n" ^ pp_thm complete)
-    val _ = tracing ("compat:\n" ^ pp_thm compat)
-    val _ = tracing ("compat_store:\n" ^ pp_thm compat_store)
-    *)
-
     val (goalstate, values) = PROFILE "prove_stuff"
       (prove_stuff lthy globals G f R xclauses complete compat
          compat_store G_elim G_eqvt) f_defthm
@@ -1352,16 +1177,6 @@
       end
 
     val qglrs = map convert_eqs fqgars
-   
-    fun pp_f (f, args, precond, lhs, rhs) =
-      (tracing ("lhs: " ^ commas 
-         (map (fn t => Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), t))) lhs));
-       tracing ("rhs: " ^ Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), rhs))))
-
-    fun pp_q (args, precond, lhs, rhs) =
-      (tracing ("qlhs: " ^ Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), lhs)));
-       tracing ("qrhs: " ^ Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), rhs))))
-
   in
     Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST,
       parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
@@ -1642,11 +1457,6 @@
   end
 
 *}
-ML {*
-  Proof.theorem;
-  Proof.refine
-*}
-
 
 ML {*
 fun gen_function is_external prep default_constraint fixspec eqns config lthy =




