# HG changeset patch # User Christian Urban # Date 1284081460 -28800 # Node ID 486d4647bb371938d0d35a9948666af346f22573 # Parent 6e37bfb624748d8b8a804a1adee28fb676975311 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) diff -r 6e37bfb62474 -r 486d4647bb37 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal-General/Nominal2_Base.thy Fri Sep 10 09:17:40 2010 +0800 @@ -848,6 +848,18 @@ qed qed +section {* Support w.r.t. relations *} + +text {* + This definition is used for unquotient types, where + alpha-equivalence does not coincide with equality. +*} + +definition + "supp_rel R x = {a. infinite {b. \(R ((a \ b) \ x) x)}}" + + + section {* Finitely-supported types *} class fs = pt + diff -r 6e37bfb62474 -r 486d4647bb37 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal-General/nominal_library.ML Fri Sep 10 09:17:40 2010 +0800 @@ -33,6 +33,11 @@ val mk_supp_ty: typ -> term -> term val mk_supp: term -> term + val supp_rel_ty: typ -> typ + val supp_rel_const: typ -> term + val mk_supp_rel_ty: typ -> term -> term -> term + val mk_supp_rel: term -> term -> term + val supports_const: typ -> term val mk_supports_ty: typ -> term -> term -> term val mk_supports: term -> term -> term @@ -124,8 +129,13 @@ fun supp_ty ty = ty --> @{typ "atom set"}; fun supp_const ty = Const (@{const_name supp}, supp_ty ty) -fun mk_supp_ty ty t = supp_const ty $ t; -fun mk_supp t = mk_supp_ty (fastype_of t) t; +fun mk_supp_ty ty t = supp_const ty $ t +fun mk_supp t = mk_supp_ty (fastype_of t) t + +fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"}; +fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty) +fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t +fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Abs.thy --- a/Nominal/Abs.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/Abs.thy Fri Sep 10 09:17:40 2010 +0800 @@ -6,11 +6,6 @@ "Quotient_Product" begin -section {* Support w.r.t. relations *} - -definition - "supp_rel R x = {a. infinite {b. \(R ((a \ b) \ x) x)}}" - section {* Abstractions *} diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Ex/Ex1.thy --- a/Nominal/Ex/Ex1.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/Ex/Ex1.thy Fri Sep 10 09:17:40 2010 +0800 @@ -18,8 +18,19 @@ "bv (Bar0 x) = {}" | "bv (Bar1 v x b) = {atom v}" - -thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars] +thm foo_bar.distinct +thm foo_bar.induct +thm foo_bar.inducts +thm foo_bar.exhaust +thm foo_bar.fv_defs +thm foo_bar.bn_defs +thm foo_bar.perm_simps +thm foo_bar.eq_iff +thm foo_bar.fv_bn_eqvt +thm foo_bar.size_eqvt +thm foo_bar.supports +thm foo_bar.fsupp +thm foo_bar.supp lemma "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/Ex/ExPS8.thy Fri Sep 10 09:17:40 2010 +0800 @@ -6,11 +6,11 @@ atom_decl name -declare [[STEPS = 100]] +declare [[STEPS = 31]] -nominal_datatype exp = +nominal_datatype fun_pats: exp = EVar name -| EUnit +| EUnit | EPair exp exp | ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e and fnclause = @@ -44,6 +44,57 @@ | "b_lrb (Clause fcs) = (b_fnclauses fcs)" | "b_fnclause (K x pat exp) = {atom x}" +thm fun_pats.distinct +thm fun_pats.induct +thm fun_pats.inducts +thm fun_pats.exhaust +thm fun_pats.fv_defs +thm fun_pats.bn_defs +thm fun_pats.perm_simps +thm fun_pats.eq_iff +thm fun_pats.fv_bn_eqvt +thm fun_pats.size_eqvt +thm fun_pats.supports +thm fun_pats.fsupp +thm fun_pats.supp + + +ML {* +fun add_ss thms = + HOL_basic_ss addsimps thms + +fun symmetric thms = + map (fn thm => thm RS @{thm sym}) thms +*} + +lemma + "(fv_exp x = supp x) \ + (fv_fnclause xa = supp xa \ fv_b_lrb xa = supp_rel alpha_b_lrb xa) \ + (fv_fnclauses xb = supp xb \ fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \ + (fv_lrb xc = supp xc \ fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \ + (fv_lrbs xd = supp xd \ fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \ + (fv_pat xe = supp xe \ fv_b_pat xe = supp_rel alpha_b_pat xe)" +apply(rule fun_pats.induct) +apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*}) +thm fun_pats.inducts +oops + + +lemma + "fv_exp x = supp x" and + "fv_fnclause y = supp y" and + "fv_fnclauses xb = supp xb" and + "fv_lrb xc = supp xc" and + "fv_lrbs xd = supp xd" and + "fv_pat xe = supp xe" and + "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and + "fv_b_pat xe = supp_rel alpha_b_pat xe" and + "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and + "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and + "fv_b_lrb y = supp_rel alpha_b_lrb y" +apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts) +thm fun_pats.inducts +oops end diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Ex/LetFun.thy --- a/Nominal/Ex/LetFun.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/Ex/LetFun.thy Fri Sep 10 09:17:40 2010 +0800 @@ -4,8 +4,11 @@ atom_decl name -(* x is bound in both e1 and e2 - names in p are bound only in e1 *) +(* x is bound in both e1 and e2; + bp-names in p are bound only in e1 +*) + +declare [[STEPS = 100]] nominal_datatype exp = Var name @@ -22,4 +25,19 @@ | "bp (PUnit) = []" | "bp (PPair p1 p2) = bp p1 @ bp p2" +thm exp_pat.distinct +thm exp_pat.induct +thm exp_pat.inducts +thm exp_pat.exhaust +thm exp_pat.fv_defs +thm exp_pat.bn_defs +thm exp_pat.perm_simps +thm exp_pat.eq_iff +thm exp_pat.fv_bn_eqvt +thm exp_pat.size_eqvt +thm exp_pat.supports +thm exp_pat.fsupp +thm exp_pat.supp + + end \ No newline at end of file diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Fri Sep 10 09:17:40 2010 +0800 @@ -6,14 +6,14 @@ declare [[STEPS = 100]] -nominal_datatype single_let: trm = +nominal_datatype single_let: trm = Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind x in t | Let a::"assg" t::"trm" bind "bn a" in t | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 | Bar x::"name" y::"name" t::"trm" bind y x in t x y -| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 +| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2 and assg = As "name" x::"name" t::"trm" bind x in t binder @@ -34,6 +34,7 @@ thm single_let.size_eqvt thm single_let.supports thm single_let.fsupp +thm single_let.supp lemma test2: assumes "fv_trm t = supp t" @@ -44,26 +45,25 @@ apply(rule assms) done - lemma supp_fv: - "fv_trm t = supp t" "fv_assg as = supp as" "fv_bn as = supp_rel alpha_bn as" -apply(induct t and as rule: single_let.inducts) + "fv_trm x = supp x" + "fv_assg xa = supp xa" + "fv_bn xa = supp_rel alpha_bn xa" +apply(induct rule: single_let.inducts) -- " 0A " apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric])? apply(simp (no_asm) only: supp_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) -- " 0B" apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric])? apply(simp (no_asm) only: supp_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) --" 1 " apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric]) +apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *}) apply(simp (no_asm) only: supp_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) @@ -72,7 +72,7 @@ apply(simp only:) -- " 2 " apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric]) +apply(subst supp_abs(3)[symmetric]) apply(simp (no_asm) only: supp_def supp_rel_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) @@ -82,7 +82,7 @@ apply(simp only:) -- " 3 " apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(1)[symmetric]) +apply(subst supp_abs(1)[symmetric]) apply(simp (no_asm) only: supp_def supp_rel_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) @@ -91,7 +91,7 @@ apply(simp only: supp_Pair Un_assoc conj_assoc) -- " Bar " apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric]) +apply(subst supp_abs(3)[symmetric]) apply(simp (no_asm) only: supp_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) @@ -100,7 +100,8 @@ apply(simp only: supp_Pair Un_assoc conj_assoc) -- " Baz " apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric]) +apply(subst supp_abs(1)[symmetric]) +apply(subst supp_abs(1)[symmetric]) apply(simp (no_asm) only: supp_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) @@ -110,7 +111,7 @@ apply(simp only: supp_Pair Un_assoc conj_assoc) -- "last" apply(simp only: single_let.fv_defs supp_Pair[symmetric]) -apply(simp only: supp_abs(3)[symmetric]) +apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *}) apply(simp (no_asm) only: supp_def supp_rel_def) apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/Nominal2.thy Fri Sep 10 09:17:40 2010 +0800 @@ -249,7 +249,6 @@ end *} - ML {* (* for testing porposes - to exit the procedure early *) exception TEST of Proof.context @@ -259,6 +258,7 @@ fun get_STEPS ctxt = Config.get ctxt STEPS *} + setup STEPS_setup ML {* @@ -333,9 +333,8 @@ mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys (* definition of alpha_eq_iff lemmas *) - (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*) val _ = warning "Eq-iff theorems"; - val (alpha_eq_iff_simps, alpha_eq_iff) = + val alpha_eq_iff = if get_STEPS lthy > 5 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases else raise TEST lthy4 @@ -542,6 +541,7 @@ val qinducts = Project_Rule.projections lthyA qinduct (* supports lemmas *) + val _ = warning "Proving Supports Lemmas and fs-Instances" val qsupports_thms = if get_STEPS lthy > 28 then prove_supports lthyB qperm_simps qtrms @@ -559,6 +559,15 @@ then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB else raise TEST lthyB + (* fv - supp equality *) + val _ = warning "Proving Equality between fv and supp" + val qfv_supp_thms = + if get_STEPS lthy > 31 + then prove_fv_supp qtys qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs + qperm_simps qfv_qbn_eqvts qinducts (flat raw_bclauses) lthyC + else [] + + (* noting the theorems *) (* generating the prefix for the theorem names *) @@ -575,15 +584,17 @@ ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) - ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) + ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) + ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms) in (0, lthy9') end handle TEST ctxt => (0, ctxt) *} + section {* Preparing and parsing of the specification *} ML {* diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Fri Sep 10 09:17:40 2010 +0800 @@ -14,7 +14,7 @@ term list -> typ list -> thm list val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> - thm list -> (thm list * thm list) + thm list -> thm list val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list @@ -315,11 +315,12 @@ (** produces the alpha_eq_iff simplification rules **) -(* in case a theorem is of the form (C.. = C..), it will be - rewritten to ((C.. = C..) = True) *) +(* in case a theorem is of the form (Rel Const Const), it will be + rewritten to ((Rel Const = Const) = True) +*) fun mk_simp_rule thm = case (prop_of thm) of - @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm] + @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} | _ => thm fun alpha_eq_iff_tac dist_inj intros elims = @@ -347,7 +348,7 @@ val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms - |> `(map mk_simp_rule) + |> map mk_simp_rule end diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/nominal_dt_quot.ML Fri Sep 10 09:17:40 2010 +0800 @@ -20,11 +20,13 @@ (string * term * mixfix) list -> local_theory -> local_theory val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context + end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = struct + (* defines the quotient types *) fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = let @@ -86,7 +88,7 @@ end -(* lifts a theorem and cleans all "_raw" instances +(* lifts a theorem and cleans all "_raw" parts from variable names *) local @@ -126,6 +128,5 @@ #> unraw_vars_thm #> Drule.zero_var_indexes) thms, ctxt) - end (* structure *) diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/nominal_dt_supp.ML Fri Sep 10 09:17:40 2010 +0800 @@ -12,44 +12,48 @@ val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory + + val prove_fv_supp: typ list -> term list -> term list -> term list -> thm list -> thm list -> + thm list -> thm list -> thm list -> thm list -> bclause list list -> Proof.context -> thm list end structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = struct +fun lookup xs x = the (AList.lookup (op=) xs x) (* supports lemmas for constructors *) fun mk_supports_goal ctxt qtrm = -let - val vs = fresh_args ctxt qtrm - val rhs = list_comb (qtrm, vs) - val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} - |> mk_supp -in - mk_supports lhs rhs - |> HOLogic.mk_Trueprop -end + let + val vs = fresh_args ctxt qtrm + val rhs = list_comb (qtrm, vs) + val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} + |> mk_supp + in + mk_supports lhs rhs + |> HOLogic.mk_Trueprop + end fun supports_tac ctxt perm_simps = -let - val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} - val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} -in - EVERY' [ simp_tac ss1, - Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], - simp_tac ss2 ] -end + let + val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} + val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} + in + EVERY' [ simp_tac ss1, + Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], + simp_tac ss2 ] + end fun prove_supports_single ctxt perm_simps qtrm = -let - val goal = mk_supports_goal ctxt qtrm - val ctxt' = Variable.auto_fixes goal ctxt -in - Goal.prove ctxt' [] [] goal - (K (HEADGOAL (supports_tac ctxt perm_simps))) - |> singleton (ProofContext.export ctxt' ctxt) -end + let + val goal = mk_supports_goal ctxt qtrm + val ctxt' = Variable.auto_fixes goal ctxt + in + Goal.prove ctxt' [] [] goal + (K (HEADGOAL (supports_tac ctxt perm_simps))) + |> singleton (ProofContext.export ctxt' ctxt) + end fun prove_supports ctxt perm_simps qtrms = map (prove_supports_single ctxt perm_simps) qtrms @@ -58,44 +62,182 @@ (* finite supp lemmas for qtypes *) fun prove_fsupp ctxt qtys qinduct qsupports_thms = -let - val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt - val goals = vs ~~ qtys - |> map Free - |> map (mk_finite o mk_supp) - |> foldr1 (HOLogic.mk_conj) - |> HOLogic.mk_Trueprop + let + val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt + val goals = vs ~~ qtys + |> map Free + |> map (mk_finite o mk_supp) + |> foldr1 (HOLogic.mk_conj) + |> HOLogic.mk_Trueprop - val tac = - EVERY' [ rtac @{thm supports_finite}, - resolve_tac qsupports_thms, - asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] -in - Goal.prove ctxt' [] [] goals - (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) - |> singleton (ProofContext.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm - |> map zero_var_indexes -end + val tac = + EVERY' [ rtac @{thm supports_finite}, + resolve_tac qsupports_thms, + asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] + in + Goal.prove ctxt' [] [] goals + (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm + |> map zero_var_indexes + end (* finite supp instances *) fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = -let - val lthy1 = - lthy - |> Local_Theory.exit_global - |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) + let + val lthy1 = + lthy + |> Local_Theory.exit_global + |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) - fun tac _ = - Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac qfsupp_thms)) -in - lthy1 - |> Class.prove_instantiation_exit tac - |> Named_Target.theory_init -end + fun tac _ = + Class.intro_classes_tac [] THEN + (ALLGOALS (resolve_tac qfsupp_thms)) + in + lthy1 + |> Class.prove_instantiation_exit tac + |> Named_Target.theory_init + end + + +(* proves that fv and fv_bn equals supp *) + +fun mk_fvs_goals ty_arg_map fv = + let + val arg = fastype_of fv + |> domain_type + |> lookup ty_arg_map + in + (fv $ arg, mk_supp arg) + |> HOLogic.mk_eq + |> HOLogic.mk_Trueprop + end + +fun mk_fv_bns_goals ty_arg_map fv_bn alpha_bn = + let + val arg = fastype_of fv_bn + |> domain_type + |> lookup ty_arg_map + in + (fv_bn $ arg, mk_supp_rel alpha_bn arg) + |> HOLogic.mk_eq + |> HOLogic.mk_Trueprop + end + +fun add_ss thms = + HOL_basic_ss addsimps thms + +fun symmetric thms = + map (fn thm => thm RS @{thm sym}) thms + +val supp_abs_set = @{thms supp_abs(1)[symmetric]} +val supp_abs_res = @{thms supp_abs(2)[symmetric]} +val supp_abs_lst = @{thms supp_abs(3)[symmetric]} + +fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set + | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res + | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst + +fun mk_supp_abs_tac ctxt [] = [] + | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs + | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs + +fun mk_bn_supp_abs_tac thm = + (prop_of thm) + |> HOLogic.dest_Trueprop + |> snd o HOLogic.dest_eq + |> fastype_of + |> (fn ty => case ty of + @{typ "atom set"} => simp_tac (add_ss supp_abs_set) + | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst) + | _ => raise TERM ("mk_bn_supp_abs_tac", [prop_of thm])) + + +val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} +val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} +val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def + prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} + +fun ind_tac ctxt qinducts = + let + fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st) + in + DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) [])) + end + +fun p_tac msg i = + if false then print_tac ("ptest: " ^ msg) else all_tac + +fun q_tac msg i = + if true then print_tac ("qtest: " ^ msg) else all_tac + +fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps + fv_bn_eqvts qinducts bclausess ctxt = + let + val (arg_names, ctxt') = + Variable.variant_fixes (replicate (length qtys) "x") ctxt + val args = map2 (curry Free) arg_names qtys + val ty_arg_map = qtys ~~ args + val ind_args = map SOME arg_names + + val goals1 = map (mk_fvs_goals ty_arg_map) fvs + val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns + + fun fv_tac ctxt bclauses = + SOLVED' (EVERY' [ + (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), + TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), + p_tac "A", + TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), + p_tac "B", + TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), + p_tac "C", + TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], + p_tac "D", + TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), + p_tac "E", + TRY o asm_full_simp_tac (add_ss thms3), + p_tac "F", + TRY o simp_tac (add_ss thms2), + p_tac "G", + TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), + p_tac "H", + (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) + ]) + + fun bn_tac ctxt bn_simp = + SOLVED' (EVERY' [ + (fn i => print_tac ("BN Goal: " ^ string_of_int i)), + TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), + q_tac "A", + TRY o mk_bn_supp_abs_tac bn_simp, + q_tac "B", + TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), + q_tac "C", + TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], + q_tac "D", + TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), + q_tac "E", + TRY o asm_full_simp_tac (add_ss thms3), + q_tac "F", + TRY o simp_tac (add_ss thms2), + q_tac "G", + TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), + (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i)) + ]) + + fun fv_tacs ctxt = map (fv_tac ctxt) bclausess + fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps + + in + Goal.prove_multi ctxt' [] [] (goals1 @ goals2) + (fn {context as ctxt, ...} => HEADGOAL + (ind_tac ctxt qinducts THEN' RANGE (fv_tacs ctxt @ bn_tacs ctxt))) + |> ProofContext.export ctxt' ctxt + end + end (* structure *)