nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:e5fa8de0e4bd
+:4aa72a88b2c1
 lemma eqvtI:
 "(\<And>p. p \<bullet> x \<equiv> x) \<Longrightarrow> eqvt x"
 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 (p \<bullet> 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
 ML {*
 val trace = Unsynchronized.ref false
 qglr : ((string * typ) list * term list * term * term),
 cdata : clause_context,
 tree: Function_Ctx_Tree.ctx_tree,
 lGI: thm,
 RCs: rec_call_info list}
+*}
+thm accp_induct_rule
+ML {*
 (* Theory dependencies. *)
 val acc_induct_rule = @{thm accp_induct_rule}
 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
 val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
 in
 Logic.mk_implies
 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-(* HERE |> (curry Logic.mk_implies) (mk_eqvt fvar) *)
+(*|> (curry Logic.mk_implies) (mk_eqvt fvar) *)
-|> (curry Logic.mk_implies) @{term "Trueprop True"}
+|> (curry Logic.mk_implies) @{term "Trueprop True"}  (* HERE *)
 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
 |> curry abstract_over fvar
 |> curry subst_bound f
 end
 in
 let
 val compat = lookup_compat_thm j i cts
 in
 compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+(*|> tap (fn th => tracing ("NEED TO PROVE" ^ @{make_string} th)) *)
 |> Thm.elim_implies @{thm TrueI}
 |> 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" *)
 end
 let
 val compat = lookup_compat_thm i j cts
 in
 compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+(* |> tap (fn th => tracing ("NEED TO PROVE" ^ @{make_string} th)) *)
 |> Thm.elim_implies @{thm TrueI}
 |> fold Thm.elim_implies agsi
 |> fold Thm.elim_implies agsj
 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
 val P = cterm_of thy (mk_eq (y, rhsC))
 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 clausei) clauses rep_lemmas
+val _ = tracing ("unique_clauses\n" ^ cat_lines (map @{make_string} unique_clauses))
 fun elim_implies_eta A AB =
 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
 val uniqueness = G_cases
 |> Thm.forall_elim (cterm_of thy lhs)
 in
 (exactly_one, function_value)
 end
 *}
+(* AAA *)
 ML {*
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
 let
 val Globals {h, domT, ranT, x, ...} = globals
 val thy = ProofContext.theory_of ctxt
 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
 |> instantiate' [] [NONE, SOME (cterm_of thy h)]
+val _ = tracing ("ihyp\n" ^ @{make_string} ihyp)
+val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm)
+val _ = tracing ("ih_intro\n" ^ @{make_string} ih_intro)
+val _ = tracing ("ih_elim\n" ^ @{make_string} ih_elim)
 val _ = trace_msg (K "Proving Replacement lemmas...")
 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+val _ = tracing (cat_lines (map @{make_string} repLemmas))
 val _ = trace_msg (K "Proving cases for unique existence...")
 val (ex1s, values) =
 split_list (map (mk_uniqueness_case thy globals G f
 ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+val _ = tracing ("ex1s\n" ^ cat_lines (map @{make_string} ex1s))
+val _ = tracing ("values\n" ^ cat_lines (map @{make_string} values))
 val _ = trace_msg (K "Proving: Graph is a function")
 val graph_is_function = complete
 |> Thm.forall_elim_vars 0
 |> fold (curry op COMP) ex1s
 in
 (goalstate, values)
 end
 *}
-ML {*
-Inductive.add_inductive_i;
-Local_Theory.conceal
-*}
 ML {*
 (* wrapper -- restores quantifiers in rule specifications *)
 fun inductive_def (binding as ((R, T), _)) intrs lthy =
 let
 val ((G, GIntro_thms, G_elim, G_induct, G_eqvt), lthy) =
 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 val _ = tracing ("Graph - name: " ^ @{make_string} G)
 val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms))
-val _ = tracing ("Graph Equivariance" ^ @{make_string} G_eqvt)
+val _ = tracing ("Graph Equivariance " ^ @{make_string} G_eqvt)
 val ((f, (_, f_defthm)), lthy) =
 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) =
 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 val _ = tracing ("Relation - name: " ^ @{make_string} R)
 val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss))
-val _ = tracing ("Relation Equivariance" ^ @{make_string} R_eqvt)
+val _ = tracing ("Relation Equivariance " ^ @{make_string} R_eqvt)
 val (_, lthy) =
 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 val newthy = ProofContext.theory_of lthy
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 sorry
+thm depth.psimps
 nominal_primrec
 frees :: "lam \<Rightarrow> name set"
 where
 "frees (Var x) = {x}"

changeset 2651	4aa72a88b2c1
parent 2650	e5fa8de0e4bd
child 2652	e9a2770660ef