Nominal/Test.thy
changeset 1329 8502c2ff3be5
parent 1327 670701b19e8e
parent 1326 4bc9278a808d
child 1330 88d2d4beb9e0
equal deleted inserted replaced
1328:531dcebbf483 1329:8502c2ff3be5
    11 | WP "weird" "weird"
    11 | WP "weird" "weird"
    12 
    12 
    13 thm permute_weird_raw.simps[no_vars]
    13 thm permute_weird_raw.simps[no_vars]
    14 thm alpha_weird_raw.intros[no_vars]
    14 thm alpha_weird_raw.intros[no_vars]
    15 thm fv_weird_raw.simps[no_vars]
    15 thm fv_weird_raw.simps[no_vars]
    16 
    16 (* Potential problem: Is it correct that in the fv-function 
    17 abbreviation "fv_weird \<equiv> fv_weird_raw"
    17 the first two terms are created? Should be ommitted. Also
    18 abbreviation "alpha_weird \<equiv> alpha_weird_raw"
    18 something wrong with the permutations. *)
    19 
    19 
    20 (*
    20 lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)"
       
    21 apply (erule alpha_weird_raw.induct)
       
    22 defer
       
    23 apply (simp add: alpha_weird_raw.intros)
       
    24 apply (simp add: alpha_weird_raw.intros)
       
    25 apply (simp only: permute_weird_raw.simps)
       
    26 apply (rule alpha_weird_raw.intros)
       
    27 apply (erule exi[of _ _ "p"])
       
    28 apply (erule exi[of _ _ "p"])
       
    29 apply (erule exi[of _ _ "p"])
       
    30 apply (erule exi[of _ _ "p"])
       
    31 apply (erule conjE)+
       
    32 apply (rule conjI)
       
    33 apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
       
    34 apply (simp add: eqvts)
       
    35 apply (simp add: eqvts)
       
    36 apply (rule conjI)
       
    37 defer
       
    38 apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
       
    39 apply (simp add: eqvts)
       
    40 apply (simp add: eqvts)
       
    41 apply (rule conjI)
       
    42 defer
       
    43 apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt)
       
    44 apply(simp add: alpha_gen.simps)
       
    45 apply(erule conjE)+
       
    46   apply(rule conjI)
       
    47   apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
       
    48 apply (simp add: eqvts)
       
    49   apply(rule conjI)
       
    50   apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
       
    51 apply (simp add: eqvts add_perm_eqvt)
       
    52 apply (simp add: permute_eqvt[symmetric])
       
    53 done
       
    54 
       
    55 primrec 
       
    56   fv_weird
       
    57 where
       
    58   "fv_weird (WBind_raw x y p1 p2 p3) = 
       
    59     (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})"
       
    60 | "fv_weird (WV_raw x) = {atom x}"
       
    61 | "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)"
       
    62 
    21 inductive
    63 inductive
    22   alpha_weird
    64   alpha_weird
    23 where
    65 where
    24   "\<exists>p1 p2.  
    66   "\<exists>p1 p2.  
    25   ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and>
    67   ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and>
    27   ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and>
    69   ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and>
    28   supp p1 \<inter> supp p2 = {} \<Longrightarrow>
    70   supp p1 \<inter> supp p2 = {} \<Longrightarrow>
    29   alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)"
    71   alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)"
    30 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)"
    72 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)"
    31 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)"
    73 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)"
    32 *)
    74 
    33 
    75 (*
    34 abbreviation "WBind \<equiv> WBind_raw"
    76 abbreviation "WBind \<equiv> WBind_raw"
    35 abbreviation "WP \<equiv> WP_raw" 
    77 abbreviation "WP \<equiv> WP_raw"
    36 abbreviation "WV \<equiv> WV_raw" 
    78 abbreviation "WV \<equiv> WV_raw"
    37 
    79 
    38 lemma test:
    80 lemma test:
    39   assumes a: "distinct [x, y, z]"
    81   assumes a: "distinct [x, y, z]"
    40   shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
    82   shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
    41                      (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
    83                      (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
    42 apply(rule_tac alpha_weird_raw.intros)
    84 apply(rule_tac alpha_weird.intros)
    43 unfolding alpha_gen
    85 unfolding alpha_gen
    44 using a
    86 using a
    45 apply(simp)
    87 apply(simp)
    46 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
    88 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
    47 apply(rule conjI)
    89 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
       
    90 apply(simp add: fresh_star_def)
    48 apply(simp add: flip_def)
    91 apply(simp add: flip_def)
    49 apply(simp add: fresh_star_def)
    92 apply(auto)
    50 defer
    93 prefer 2
    51 apply(rule conjI)
    94 apply(rule alpha_weird.intros)
       
    95 apply(simp add: alpha_weird.intros(2))
       
    96 prefer 2
       
    97 apply(rule alpha_weird.intros)
       
    98 apply(simp add: alpha_weird.intros(2))
    52 apply(simp)
    99 apply(simp)
    53 apply(rule alpha_weird_raw.intros)
   100 apply(rule alpha_weird.intros)
    54 apply(simp add: alpha_weird_raw.intros(2))
       
    55 apply(simp add: fresh_star_def)
       
    56 apply(rule conjI)
       
    57 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
       
    58 apply(rule_tac x="0" in exI)
       
    59 apply(simp)
   101 apply(simp)
    60 apply(rule alpha_weird_raw.intros)
   102 apply(simp add: alpha_gen)
    61 apply(simp add: alpha_weird_raw.intros(2))
   103 using a
    62 apply(rule conjI)
       
    63 apply(auto)[1]
       
    64 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
       
    65 apply(rule conjI)
       
    66 apply(simp add: flip_def)
       
    67 apply(auto)[1]
       
    68 defer
       
    69 apply(simp)
   104 apply(simp)
    70 apply(rule alpha_weird_raw.intros)
   105 *)
    71 apply(simp add: alpha_weird_raw.intros(2))
       
    72 apply(simp add: fresh_perm)
       
    73 defer
       
    74 apply(simp add: fresh_perm)
       
    75 apply(simp add: atom_eqvt)
       
    76 unfolding flip_def[symmetric]
       
    77 apply(simp)
       
    78 done
       
    79 
       
    80 
       
    81 
   106 
    82 text {* example 1 *}
   107 text {* example 1 *}
    83 
   108 
    84 (* ML {* set show_hyps *} *)
   109 (* ML {* set show_hyps *} *)
    85 
   110 
   217   "bv3 ANil = {}"
   242   "bv3 ANil = {}"
   218 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
   243 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
   219 
   244 
   220 (* example 4 from Terms.thy *)
   245 (* example 4 from Terms.thy *)
   221 
   246 
   222 (* fv_eqvt does not work, we need to repaire defined permute functions...
   247 (* fv_eqvt does not work, we need to repaire defined permute functions
   223 nominal_datatype trm4 =
   248    defined fv and defined alpha... *)
       
   249 (*nominal_datatype trm4 =
   224   Vr4 "name"
   250   Vr4 "name"
   225 | Ap4 "trm4" "trm4 list"
   251 | Ap4 "trm4" "trm4 list"
   226 | Lm4 x::"name" t::"trm4"  bind x in t
   252 | Lm4 x::"name" t::"trm4"  bind x in t
   227 
   253 
   228 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
   254 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
   229 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
   255 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)
   230 
   256 
   231 (* example 5 from Terms.thy *)
   257 (* example 5 from Terms.thy *)
   232 
   258 
   233 nominal_datatype trm5 =
   259 nominal_datatype trm5 =
   234   Vr5 "name"
   260   Vr5 "name"