nominal2: comparison Nominal/Ex/Typing.thy

equal deleted inserted replaced

-:0865caafbfe6
+:3890483c674f
 | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
 | real_head_of t = head_of t
 *}
 ML {*
 fun mk_vc_compat (avoid, avoid_trm) prems concl_args params =
 let
-fun aux arg = arg
+val vc_goal = concl_args
+|> HOLogic.mk_tuple
 |> mk_fresh_star avoid_trm
 |> HOLogic.mk_Trueprop
 |> (curry Logic.list_implies) prems
 |> (curry list_all_free) params
 in
-if null avoid then [] else map aux concl_args
+if null avoid then [] else [vc_goal]
 end
 *}
 ML {*
 fun map_term prop f trm =
 in
 EVERY1 [rtac prem', RANGE (map (SUBGOAL o select) prems) ]
 end) ctxt
 *}
-ML {*
-fun binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trms ctxt =
+ML {*
+fun fresh_thm ctxt fresh_thms p c prms avoid_trm =
+let
+val conj1 =
+mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c
+val conj2 =
+mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) prms))) (Bound 0)
+val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2))
+|> HOLogic.mk_Trueprop
+val _ = tracing ("fresh goal: " ^ Syntax.string_of_term ctxt fresh_goal)
+in
+Goal.prove ctxt [] [] fresh_goal
+(K (HEADGOAL (rtac @{thm at_set_avoiding2})))
+end
+*}
+ML {*
+fun binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt =
 Subgoal.FOCUS (fn {context, params, ...} =>
 let
 val thy = ProofContext.theory_of context
-val (prms, p, _) = split_last2 (map snd params)
+val (prms, p, c) = split_last2 (map snd params)
-val prm_tys = map (fastype_of o term_of) prms
+val prm_trms = map term_of prms
+val prm_tys = map fastype_of prm_trms
 val cperms = map (cterm_of thy o perm_const) prm_tys
 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms
 val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem
+val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm
+val fthm = fresh_thm context fresh_thms (term_of p) (term_of c) (map term_of prms) avoid_trm'
 in
 Skip_Proof.cheat_tac thy
 (* EVERY1 [rtac prem'] *)
 end) ctxt
 *}
 ML {*
-fun case_tac ctxt fresh_thms Ps avoid avoid_trm intr_cvars prem =
+fun case_tac ctxt fresh_thms Ps (avoid, avoid_trm) intr_cvars param_trms prem =
 let
 val tac1 = non_binder_tac prem intr_cvars Ps ctxt
-val tac2 = binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trm ctxt
+val tac2 = binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt
 in
 EVERY' [ rtac @{thm allI}, rtac @{thm allI}, eqvt_stac ctxt,
 if null avoid then tac1 else tac2 ]
 end
 *}
 ML {*
-fun tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars {prems, context} =
+fun prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms {prems, context} =
 let
-val cases_tac = map4 (case_tac context fresh_thms Ps) avoids avoid_trms intr_cvars prems
+val cases_tac = map4 (case_tac context fresh_thms Ps) (avoids ~~avoid_trms) intr_cvars param_trms prems
 in
 EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]
 end
 *}
 ML {*
-val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (\<And>c. Q ==> P (0::perm) c)" by simp}
+val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}
 *}
 ML {*
 fun prove_strong_inductive rule_names avoids raw_induct intrs ctxt =
 let
 val param_trms = (map o map) Free params
 val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs
 val intr_vars = (map o map) fst intr_vars_tys
 val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms
 val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys
 val (intr_prems, intr_concls) = intrs
 |> map prop_of
 |> map2 subst_Vars intr_vars_substs
 |> map Logic.strip_horn
 |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms)
 fun after_qed ctxt_outside fresh_thms ctxt =
 let
 val thms = Goal.prove ctxt [] ind_prems' ind_concl'
-(tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars)
+(prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms)
 |> singleton (ProofContext.export ctxt ctxt_outside)
 |> Datatype_Aux.split_conj_thm
 |> map (fn thm => thm RS normalise)
 |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify}))
 |> map (Drule.rotate_prems (length ind_prems'))
 equivariance typing
 nominal_inductive typing
 avoids t_Lam: "x"
+(* | t_Var: "x" *)
 apply -
 apply(simp_all add: fresh_star_def ty_fresh lam.fresh)?
 done
 apply(simp add: supp_Pair fresh_star_Un)
 apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)
 apply(simp only: permute_plus)
 apply(rule supp_perm_eq)
 apply(simp add: supp_Pair fresh_star_Un)
+(* apply(perm_simp) *)
 apply(simp (no_asm) only: eqvts)
 apply(rule a3)
 apply(simp only: eqvts permute_plus)
 apply(rule_tac p="- (q + p)" in permute_boolE)
 apply(perm_strict_simp add: permute_minus_cancel)
 apply(rule_tac p="- (q + p)" in permute_boolE)
 apply(perm_strict_simp add: permute_minus_cancel)
 apply(assumption)
 apply(perm_strict_simp)
 apply(simp only:)
+thm at_set_avoiding2
 apply(rule at_set_avoiding2)
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(rule_tac p="-p" in permute_boolE)

changeset 2637	3890483c674f
parent 2636	0865caafbfe6
child 2638	e1e2ca92760b