Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Foo2.thy
changeset 2609 666ffc8a92a9
parent 2608 86e3b39c2a60
child 2611 3d101f2f817c
equal deleted inserted replaced
2608:86e3b39c2a60 2609:666ffc8a92a9 
    22   bn::"assg \<Rightarrow> atom list"
 
    22   bn::"assg \<Rightarrow> atom list"
 
    23 where
 
    23 where
 
    24  "bn (As x y t a) = [atom x] @ bn a"
 
    24  "bn (As x y t a) = [atom x] @ bn a"
 
    25 | "bn (As_Nil) = []"
 
    25 | "bn (As_Nil) = []"
 
    26 
    26 
    27 thm foo.exhaust
 
       
    28 
       
    29 ML {* 
       
    30   Variable.import;
 
       
    31   Variable.import true @{thms foo.exhaust} @{context}
 
       
    32 *}
 
       
    33 
    27 
    34 thm foo.bn_defs
 
    28 thm foo.bn_defs
 
    35 thm foo.permute_bn
 
    29 thm foo.permute_bn
 
    36 thm foo.perm_bn_alpha
 
    30 thm foo.perm_bn_alpha
 
    37 thm foo.perm_bn_simps
 
    31 thm foo.perm_bn_simps
 
    51 thm foo.supports
 
    45 thm foo.supports
 
    52 thm foo.fsupp
 
    46 thm foo.fsupp
 
    53 thm foo.supp
 
    47 thm foo.supp
 
    54 thm foo.fresh
 
    48 thm foo.fresh
 
    55 
    49 
       
    50 (*
 
       
    51 lemma ex_prop:
 
       
    52   shows "\<exists>n::nat. Suc n = n"
 
       
    53 sorry
 
       
    54 
       
    55 lemma test:
 
       
    56   shows "True"
 
       
    57 apply -
 
       
    58 ML_prf {*
 
       
    59   val (x, ctxt') = Obtain.result (K (
 
       
    60   EVERY [print_tac "test", 
       
    61          etac exE 1,
 
       
    62          print_tac "end"])) 
       
    63   @{thms ex_prop} @{context};
 
       
    64   ProofContext.verbose := true;
 
       
    65   ProofContext.pretty_context ctxt'
 
       
    66   |> Pretty.block
 
       
    67   |> Pretty.writeln
 
       
    68 *}
 
       
    69 *)
 
    56 
    70 
    57 
    71 
    58 text {* *}
 
    72 text {* *}
 
    59 
    73 
    60 
    74 
   101   and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
 
   115   and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
 
   102   and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
   116   and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
   103   and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
 
   117   and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
 
   104   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
 
   118   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
 
   105   shows "P"
 
   119   shows "P"
 
   106 apply(rule_tac y="y" in foo.exhaust(1))
 
   120 apply(rule_tac foo.exhaust(1))
 
   107 apply(rule assms(1))
 
   121 apply(rule assms(1))
 
   108 apply(rule exI)+
 
   122 apply(rule exI)+
 
   109 apply(assumption)
 
   123 apply(assumption)
 
   110 apply(rule assms(2))
 
   124 apply(rule assms(2))
 
   111 apply(rule exI)+
 
   125 apply(rule exI)+
 
   112 apply(assumption)
 
   126 apply(assumption)
 
   113 (* lam case *)
 
   127 (* lam case *)
 
   114 (*
 
   128 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
 
   115 apply(rule Let1_rename)
 
       
   116 apply(rule assms(3))
 
       
   117 apply(assumption)
 
       
   118 apply(simp)
 
       
   119 *)
 
       
   120 
       
   121 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 
       
   122 apply(erule exE)
 
   129 apply(erule exE)
 
   123 apply(insert Abs_rename_list)[1]
 
   130 apply(insert Abs_rename_list)[1]
 
   124 apply(drule_tac x="p" in meta_spec)
 
   131 apply(drule_tac x="p" in meta_spec)
 
   125 apply(drule_tac x="[atom name]" in meta_spec)
 
   132 apply(drule_tac x="[atom name]" in meta_spec)
 
   126 apply(drule_tac x="trm" in meta_spec)
 
   133 apply(drule_tac x="trm" in meta_spec)
 
   127 apply(simp only: fresh_star_Pair set.simps)
 
   134 apply(simp only: fresh_star_Pair set.simps)
 
   128 apply(drule meta_mp)
 
   135 apply(drule meta_mp)
 
   129 apply(simp)
 
   136 apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base)
 
   130 apply(erule exE)
 
   137 apply(erule exE)
 
   131 apply(rule assms(3))
 
   138 apply(rule assms(3))
 
   132 apply(perm_simp)
 
   139 apply(perm_simp)
 
   133 apply(erule conjE)+
 
   140 apply(erule conjE)+
 
   134 apply(assumption)
 
   141 apply(assumption)
nominal2