equal
deleted
inserted
replaced
2863 | "NEGn (C IMP D) X = AXIOMSn (C IMP D) \<union> BINDINGn (C IMP D) X |
2863 | "NEGn (C IMP D) X = AXIOMSn (C IMP D) \<union> BINDINGn (C IMP D) X |
2864 \<union> IMPLEFT (C IMP D) (NEGc C (lfp (NEGn C \<circ> NEGc C))) (lfp (NEGn D \<circ> NEGc D))" |
2864 \<union> IMPLEFT (C IMP D) (NEGc C (lfp (NEGn C \<circ> NEGc C))) (lfp (NEGn D \<circ> NEGc D))" |
2865 using ty_cases sum_cases |
2865 using ty_cases sum_cases |
2866 apply(auto simp add: ty.inject) |
2866 apply(auto simp add: ty.inject) |
2867 apply(drule_tac x="x" in meta_spec) |
2867 apply(drule_tac x="x" in meta_spec) |
2868 apply(auto simp add: ty.inject) |
2868 apply(fastforce simp add: ty.inject) |
2869 apply(rotate_tac 10) |
|
2870 apply(drule_tac x="a" in meta_spec) |
|
2871 apply(auto simp add: ty.inject) |
|
2872 apply(rotate_tac 10) |
|
2873 apply(drule_tac x="a" in meta_spec) |
|
2874 apply(auto simp add: ty.inject) |
|
2875 done |
2869 done |
2876 |
2870 |
2877 termination |
2871 termination |
2878 apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))") |
2872 apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))") |
2879 apply(simp_all) |
2873 apply(simp_all) |