theory False

imports "~/Well_Order_Extension"

begin

definition
  "int_less = {(x, (y :: int)). x < y}"

text {* If the less-than relation on integers is a subset of a partial
relation, then it is the partial relation. *}
lemma int_less_subset:
  "\<lbrakk> int_less <= r; Partial_order r \<rbrakk> \<Longrightarrow> (r - Id) = int_less"
  apply (simp add: partial_order_on_def preorder_on_def)
  apply (safe, simp_all add: int_less_def)
   apply (rule ccontr)
   apply (subgoal_tac "b < a")
    apply (erule notE, erule(1) antisymD)
    apply auto[1]
   apply simp
  apply auto[1]
  done

lemma field_id: "Field Id = UNIV"
  by (auto simp: Field_def)

lemma Partial_order_int_less: "Partial_order (int_less Un Id)"
  apply (simp add: partial_order_on_def preorder_on_def refl_on_def
                   field_id)
  apply (auto simp: int_less_def intro!: transI antisymI)
  done

lemma not_wf_int_less:
  "\<not> wf int_less"
  apply clarsimp
  apply (drule_tac P="\<lambda>x. x > 0" and a=0 in wf_induct)
   apply (drule_tac x="x - 1" in spec)
   apply (simp add: int_less_def)
  apply simp
  done

lemma False: "False"
  using well_ordering_extension[OF Partial_order_int_less]
  apply clarsimp
  apply (drule int_less_subset)
   apply (simp add: well_order_on_def linear_order_on_def)
  apply (simp add: well_order_on_def not_wf_int_less)
  done

end