Nominal/Ex/Ex3.thy
changeset 2034 837b889fcf59
parent 2028 15c5a2926622
child 2082 0854af516f14
equal deleted inserted replaced
2033:74bd7bfb484b 2034:837b889fcf59
     1 theory Ex3
     1 theory Ex3
     2 imports "../Parser"
     2 imports "../NewParser"
     3 begin
     3 begin
     4 
     4 
     5 (* Example 3, identical to example 1 from Terms.thy *)
     5 (* Example 3, identical to example 1 from Terms.thy *)
     6 
     6 
     7 atom_decl name
     7 atom_decl name
     8 
     8 
     9 ML {* val _ = recursive := false  *}
     9 nominal_datatype trm =
    10 nominal_datatype trm0 =
    10   Var "name"
    11   Var0 "name"
    11 | App "trm" "trm"
    12 | App0 "trm0" "trm0"
    12 | Lam x::"name" t::"trm"        bind_set x in t
    13 | Lam0 x::"name" t::"trm0"          bind x in t
    13 | Let p::"pat" "trm" t::"trm"   bind_set "f p" in t
    14 | Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
    14 and pat =
    15 and pat0 =
    15   PN
    16   PN0
    16 | PS "name"
    17 | PS0 "name"
    17 | PD "pat" "pat"
    18 | PD0 "pat0" "pat0"
       
    19 binder
    18 binder
    20   f0::"pat0 \<Rightarrow> atom set"
    19   f::"pat \<Rightarrow> atom set"
    21 where
    20 where
    22   "f0 PN0 = {}"
    21   "f PN = {}"
    23 | "f0 (PS0 x) = {atom x}"
    22 | "f (PS x) = {atom x}"
    24 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
    23 | "f (PD p1 p2) = (f p1) \<union> (f p2)"
    25 
    24 
    26 thm trm0_pat0.fv
    25 thm trm_pat.fv
    27 thm trm0_pat0.eq_iff
    26 thm trm_pat.eq_iff
    28 thm trm0_pat0.bn
    27 thm trm_pat.bn
    29 thm trm0_pat0.perm
    28 thm trm_pat.perm
    30 thm trm0_pat0.induct
    29 thm trm_pat.induct
    31 thm trm0_pat0.distinct
    30 thm trm_pat.distinct
    32 thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
    31 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
    33 
    32 
    34 end
    33 end
    35 
    34 
    36 
    35 
    37 
    36