# HG changeset patch # User Christian Urban # Date 1285136388 -28800 # Node ID 3a5ebb2fcdbf9497bcf78427ca05f40e3d347185 # Parent ac7dff1194e89a099f3156be9f469e4082c1905a made supp proofs more robust by not using the standard induction; renamed some example files diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Mon Sep 20 21:52:45 2010 +0800 +++ b/Nominal/Ex/CoreHaskell.thy Wed Sep 22 14:19:48 2010 +0800 @@ -8,8 +8,6 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 31]] - nominal_datatype core_haskell: tkind = KStar @@ -97,6 +95,7 @@ thm core_haskell.eq_iff thm core_haskell.fv_bn_eqvt thm core_haskell.size_eqvt +thm core_haskell.supp (* lemma fresh_star_minus_perm: "as \* - p = as \* (p :: perm)" diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/ExPS7.thy --- a/Nominal/Ex/ExPS7.thy Mon Sep 20 21:52:45 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -theory ExPS7 -imports "../Nominal2" -begin - -(* example 7 from Peter Sewell's bestiary *) - -atom_decl name - -declare [[STEPS = 31]] - -nominal_datatype exp = - Var name -| Unit -| Pair exp exp -| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e -and lrb = - Assign name exp -and lrbs = - Single lrb -| More lrb lrbs -binder - b :: "lrb \ atom set" and - bs :: "lrbs \ atom set" -where - "b (Assign x e) = {atom x}" -| "bs (Single a) = b a" -| "bs (More a as) = (b a) \ (bs as)" - - - -end - - - diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Mon Sep 20 21:52:45 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -theory ExPS8 -imports "../Nominal2" -begin - -(* example 8 from Peter Sewell's bestiary *) - -atom_decl name - -declare [[STEPS = 31]] - -nominal_datatype fun_pats: exp = - EVar name -| EUnit -| EPair exp exp -| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e -and fnclause = - K x::name p::pat f::exp bind (set) "b_pat p" in f -and fnclauses = - S fnclause -| ORs fnclause fnclauses -and lrb = - Clause fnclauses -and lrbs = - Single lrb -| More lrb lrbs -and pat = - PVar name -| PUnit -| PPair pat pat -binder - b_lrbs :: "lrbs \ atom set" and - b_pat :: "pat \ atom set" and - b_fnclauses :: "fnclauses \ atom set" and - b_fnclause :: "fnclause \ atom set" and - b_lrb :: "lrb \ atom set" -where - "b_lrbs (Single l) = b_lrb l" -| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" -| "b_pat (PVar x) = {atom x}" -| "b_pat (PUnit) = {}" -| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" -| "b_fnclauses (S fc) = (b_fnclause fc)" -| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" -| "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 - -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" -thm fun_pats.inducts -apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] - fun_pats.inducts(2)[where ?fnclause="y"] - fun_pats.inducts(3)[where ?fnclauses="xb"] - fun_pats.inducts(4)[where ?lrb="xc"] - fun_pats.inducts(5)[where ?lrbs="xd"] - fun_pats.inducts(6)[where ?pat="xe"]) -thm fun_pats.inducts -oops - -end - - - diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/Modules.thy --- a/Nominal/Ex/Modules.thy Mon Sep 20 21:52:45 2010 +0800 +++ b/Nominal/Ex/Modules.thy Wed Sep 22 14:19:48 2010 +0800 @@ -2,14 +2,14 @@ imports "../Nominal2" begin -(* example from Leroy'96 about modules; - see OTT example by Owens *) +(* + example from Leroy'96 about modules + + see OTT example by Owens +*) atom_decl name -declare [[STEPS = 31]] - - nominal_datatype modules: mexp = Acc "path" @@ -72,7 +72,7 @@ thm modules.eq_iff thm modules.fv_bn_eqvt thm modules.size_eqvt - +thm modules.supp end diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/Multi_Recs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/Multi_Recs.thy Wed Sep 22 14:19:48 2010 +0800 @@ -0,0 +1,49 @@ +theory Multi_Recs +imports "../Nominal2" +begin + +(* + multiple recursive binders + + example 7 from Peter Sewell's bestiary + +*) + +atom_decl name + +nominal_datatype multi_recs: exp = + Var name +| Unit +| Pair exp exp +| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e +and lrb = + Assign name exp +and lrbs = + Single lrb +| More lrb lrbs +binder + b :: "lrb \ atom set" and + bs :: "lrbs \ atom set" +where + "b (Assign x e) = {atom x}" +| "bs (Single a) = b a" +| "bs (More a as) = (b a) \ (bs as)" + +thm multi_recs.distinct +thm multi_recs.induct +thm multi_recs.inducts +thm multi_recs.exhaust +thm multi_recs.fv_defs +thm multi_recs.bn_defs +thm multi_recs.perm_simps +thm multi_recs.eq_iff +thm multi_recs.fv_bn_eqvt +thm multi_recs.size_eqvt +thm multi_recs.supports +thm multi_recs.fsupp +thm multi_recs.supp + +end + + + diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/Multi_Recs2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/Multi_Recs2.thy Wed Sep 22 14:19:48 2010 +0800 @@ -0,0 +1,70 @@ +theory Multi_Recs2 +imports "../Nominal2" +begin + +(* + multiple recursive binders - multiple letrecs with multiple + clauses for each functions + + example 8 from Peter Sewell's bestiary (originally due + to James Cheney) + +*) + +atom_decl name + +nominal_datatype fun_recs: exp = + Var name +| Unit +| Pair exp exp +| LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e +and fnclause = + K x::name p::pat f::exp bind (set) "b_pat p" in f +and fnclauses = + S fnclause +| ORs fnclause fnclauses +and lrb = + Clause fnclauses +and lrbs = + Single lrb +| More lrb lrbs +and pat = + PVar name +| PUnit +| PPair pat pat +binder + b_lrbs :: "lrbs \ atom set" and + b_pat :: "pat \ atom set" and + b_fnclauses :: "fnclauses \ atom set" and + b_fnclause :: "fnclause \ atom set" and + b_lrb :: "lrb \ atom set" +where + "b_lrbs (Single l) = b_lrb l" +| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" +| "b_pat (PVar x) = {atom x}" +| "b_pat (PUnit) = {}" +| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" +| "b_fnclauses (S fc) = (b_fnclause fc)" +| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" +| "b_lrb (Clause fcs) = (b_fnclauses fcs)" +| "b_fnclause (K x pat exp) = {atom x}" + +thm fun_recs.distinct +thm fun_recs.induct +thm fun_recs.inducts +thm fun_recs.exhaust +thm fun_recs.fv_defs +thm fun_recs.bn_defs +thm fun_recs.perm_simps +thm fun_recs.eq_iff +thm fun_recs.fv_bn_eqvt +thm fun_recs.size_eqvt +thm fun_recs.supports +thm fun_recs.fsupp +thm fun_recs.supp + + +end + + + diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Sep 20 21:52:45 2010 +0800 +++ b/Nominal/Nominal2.thy Wed Sep 22 14:19:48 2010 +0800 @@ -563,8 +563,8 @@ 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 + then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs + qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC else [] diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/ROOT.ML --- a/Nominal/ROOT.ML Mon Sep 20 21:52:45 2010 +0800 +++ b/Nominal/ROOT.ML Wed Sep 22 14:19:48 2010 +0800 @@ -3,10 +3,11 @@ no_document use_thys ["Ex/Classical", "Ex/CoreHaskell", + Ex/Datatypes", "Ex/Ex1", "Ex/ExPS3", - "Ex/ExPS7", - "Ex/ExPS8", + "Ex/Multi_Recs", + "Ex/Multi_Recs2", "Ex/LF", "Ex/Lambda", "Ex/Let", diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Mon Sep 20 21:52:45 2010 +0800 +++ b/Nominal/nominal_dt_supp.ML Wed Sep 22 14:19:48 2010 +0800 @@ -13,8 +13,8 @@ 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 + val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> + thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list end structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = @@ -104,27 +104,17 @@ (* proves that fv and fv_bn equals supp *) -fun mk_fvs_goals ty_arg_map fv = +fun gen_mk_goals fv supp = let - val arg = fastype_of fv + val arg_ty = + fastype_of fv |> domain_type - |> lookup ty_arg_map in - (fv $ arg, mk_supp arg) - |> HOLogic.mk_eq - |> HOLogic.mk_Trueprop + (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x)) 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 mk_fvs_goals fv = gen_mk_goals fv mk_supp +fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) fun add_ss thms = HOL_basic_ss addsimps thms @@ -144,15 +134,14 @@ | 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 +fun mk_bn_supp_abs_tac trm = + trm |> fastype_of + |> body_type |> (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])) + | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} @@ -160,32 +149,49 @@ 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 = +fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps + fv_bn_eqvts qinduct 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 fvs + val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns + + - 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 tac ctxt = + SUBGOAL (fn (goal, i) => + let + val (fv_fun, arg) = + goal |> Envir.eta_contract + |> Logic.strip_assums_concl + |> HOLogic.dest_Trueprop + |> fst o HOLogic.dest_eq + |> dest_comb + val supp_abs_tac = + case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of + SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) + | NONE => mk_bn_supp_abs_tac fv_fun + in + EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), + TRY o supp_abs_tac, + TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), + TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], + TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), + TRY o asm_full_simp_tac (add_ss thms3), + TRY o simp_tac (add_ss thms2), + TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i + end) + in + induct_prove qtys (goals1 @ goals2) qinduct tac ctxt + end - fun fv_tac ctxt bclauses = +(* + fun fv_tac bclauses ctxt = 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)), @@ -207,7 +213,12 @@ (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) ]) - fun bn_tac ctxt bn_simp = + fun fv_tacs ctxt = map (fv_tac ctxt) bclausess + (*fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps*) +*) + +(* + 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)), @@ -227,18 +238,7 @@ 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 *) -