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