Nominal/Ex/ExPS8.thy
changeset 2475 486d4647bb37
parent 2454 9ffee4eb1ae1
child 2477 2f289c1f6cf1
--- 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) \<and>
+   (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
+   (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and>
+   (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and>
+   (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and>
+   (fv_pat xe = supp xe \<and> 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