nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:e9a2770660ef
+:d0f774d06e6e
 Var "name"
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l
 definition
-"eqvt x \<equiv> \<forall>p. p \<bullet> x = x"
+"eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
+definition
+"eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
 lemma eqvtI:
-"(\<And>p. p \<bullet> x \<equiv> x) \<Longrightarrow> eqvt x"
+"(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
 apply(auto simp add: eqvt_def)
 done
-term THE_default
 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])
 ML {*
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if ! trace then tracing (msg ()) else ()
 val boolT = HOLogic.boolT
 val mk_eq = HOLogic.mk_eq
 rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
 end
 *}
 ML {*
-fun mk_eqvt trm =
+fun mk_eqvt_at (f_trm, arg_trm) =
 let
-val ty = fastype_of trm
+val f_ty = fastype_of f_trm
-in
+val arg_ty = domain_type f_ty
-Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm
+in
+Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm
 |> HOLogic.mk_Trueprop
 end
+*}
+ML {*
+fun find_calls2 f t =
+let
+fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)
+| aux (Abs (_, _, t)) = aux t
+| aux _ = I
+in
+aux t []
+end
 *}
 ML {*
 (** building proof obligations *)
 let
 val _ = tracing ("domT: " ^ @{make_string} domT)
 val _ = tracing ("ranT: " ^ @{make_string} ranT)
 val _ = tracing ("fvar: " ^ @{make_string} fvar)
 val _ = tracing ("f: " ^ @{make_string} f)
-fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
 let
 val shift = incr_boundvars (length qs')
+val RCs_rhs  = find_calls2 fvar rhs
+val RCs_rhs' = find_calls2 fvar rhs'
 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')
-(*|> (curry Logic.mk_implies) (mk_eqvt fvar) *)
+|> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs)
-|> (curry Logic.mk_implies) @{term "Trueprop True"}  (* HERE *)
+|> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')
+(*|> (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
 in
 (thms1 :: store_compat_thms (n - 1) thms2)
 end
 *}
+ML {*
+fun eqvt_at_elim thm =
+let
+val _ = tracing ("term\n" ^ @{make_string} (prop_of thm))
+in
+case (prop_of thm) of
+Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ =>
+let
+val el_thm = Skip_Proof.make_thm @{theory} t
+in
+Thm.elim_implies el_thm thm
+|> eqvt_at_elim
+end
+| _ => thm
+end
+*}
 ML {*
 (* expects i <= j *)
 fun lookup_compat_thm i j cts =
 nth (nth cts (i - 1)) (j - i)
 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)) *)
+|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))
-|> Thm.elim_implies @{thm TrueI}
+(*|> Thm.elim_implies @{thm TrueI}*) (* THERE *)
+|> eqvt_at_elim
+|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))
 |> 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
 else
 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)) *)
+|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))
-|> Thm.elim_implies @{thm TrueI}
+(*|> Thm.elim_implies @{thm TrueI}*)
+|> eqvt_at_elim
+|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))
 |> 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
 end
 *}
-(* WASS *)
 ML {*
 (* Generates the replacement lemma in fully quantified form. *)
 fun mk_replacement_lemma thy h ih_elim clause =
 let
 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
 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
 val RCss = map find_calls trees
 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 ((f, (_, f_defthm)), lthy) =
 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
+(*
 val _ = tracing ("f - name: " ^ @{make_string} f)
 val _ = tracing ("f_defthm:\n" ^ @{make_string} 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 @{make_string} RCss))
 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 (_, lthy) =
 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 val newthy = ProofContext.theory_of lthy
 val complete =
 mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
 val compat =
 mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
 |> map (cert #> Thm.assume)
 val compat_store = store_compat_thms n compat
 (*
 fun define (fvar as (n, _)) caTs resultT i =
 let
 val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
 val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
-val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
+val f_exp = SumTree.mk_proj RST n' i'
+(Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
 val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
 val rew = (n, fold_rev lambda vars f_exp)
 in
 (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
 SumTree.mk_inj RST n' i' (replace_frees rews rhs)
 |> Envir.beta_norm)
 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}
 end
+*}
+ML {*
 fun define_projections fixes mutual fsum lthy =
 let
 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
 let
 val ((f, (_, f_defthm)), lthy') =
 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
-apply(simp_all add: lam.distinct)[3]
+apply(simp add: lam.eq_iff lam.distinct)
 apply(auto)[1]
+apply(simp add: lam.eq_iff lam.distinct)
 apply(auto)[1]
-apply(simp add: fresh_star_def)
+apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)[5]
+apply(simp_all add: lam.distinct)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 sorry
+(* this should not work *)
+nominal_primrec
+bnds :: "lam \<Rightarrow> name set"
+where
+"bnds (Var x) = {}"
+| "bnds (App t1 t2) = (bnds t1) \<union> (bnds t2)"
+| "bnds (Lam x t) = (bnds t) \<union> {x}"
+apply(rule_tac y="x" in lam.exhaust)
+apply(simp_all)[3]
+apply(simp_all only: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+sorry
 end

changeset 2653	d0f774d06e6e
parent 2652	e9a2770660ef
child 2654	0f0335d91456