nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:3342a2d13d95
+:16896fd8eff5
 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
 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 =
 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 *)
+|> fold Thm.elim_implies (rev eqvtsi)  (* HERE *)
-(* |> eqvt_at_elim thy eqvts *)
+(* |> eqvt_at_elim thy eqvtsi *)
 |> 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" *)
 end
 *}
 ML {*
 fun mk_eqvt_lemma thy ih_eqvt clause =
 let
-val ClauseInfo {cdata=ClauseContext {cqs, case_hyp, ...}, RCs, ...} = clause
+val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
 local open Conv in
 val ih_conv = arg1_conv o arg_conv o arg_conv
 end
 (llRI RS ih_eqvt_case)
 |> fold_rev (Thm.implies_intr o cprop_of) CCas
 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
 in
 map prep_eqvt RCs
+|> map (fold_rev (Thm.implies_intr o cprop_of) ags)
 |> map (Thm.implies_intr (cprop_of case_hyp))
 |> map (fold_rev Thm.forall_intr cqs)
 |> map (Thm.close_derivation)
 end
 *}
 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, ...}, ...} = 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', ...} =
 mk_clause_context x ctxti cdescj
 (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
 val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
 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
 |> fold Thm.forall_elim cqsj'
 |> 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)  *)
+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' *)
-|> ppp "A"
+|> pppp "A"
 |> Thm.implies_elim RLj_import
 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
-|> ppp "B"
+|> pppp "B"
 |> (fn it => trans OF [it, compat])
 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
-|> ppp "C"
+|> 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 *)
-|> ppp "D"
+|> pppp "D"
 |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
-|> ppp "E"
+|> 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 *)
-|> ppp "F"
+|> pppp "F"
 |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
-|> ppp "G"
+|> pppp "G"
 |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
-|> ppp "H"
+|> pppp "H"
 |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
-|> ppp "I"
+|> pppp "I"
 end
 *}
 ML {*
 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 eqvt_lemmas clausei) clauses rep_lemmas
+val _ = tracing ("DONE 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
 apply(simp_all add: lam.distinct)[5]
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(erule conjE)+
-apply(subst (asm) Abs_eq_iff3)
+oops
-apply(erule exE)
 nominal_primrec
 depth :: "lam \<Rightarrow> nat"

changeset 2661	16896fd8eff5
parent 2660	3342a2d13d95
child 2662	7c5bca978886