Re: [isabelle] locales, including documentation & possible programming bugs



Brian, I read ref.pdf p 30--32 on misfixes, but I could not figure out
how to write (in my code below) 
C a b c d as a b \<equiv> c d.  
I seem to have a priority problem.  I'm using the priority stuff 
ps = [99,99,99,99] and p = 70, and I've tried lots of others.

My "\<forall> a b . a b \<equiv> b a" gets me the error, a
do-not-enter on locale, and when I click on locale, I see in the
output window
Ambiguous input.  2 types are correct:
(\<forall> (a b) . (a b \<equiv> b a))
((\<forall> (a b) . (a b)) \<equiv> (b a))
If I change that to "a b \<equiv> b a", and then I get no error, but
the output window reads
Ambiguous input produces 2 parse trees: [which seem to be]
(C a b b a)
(C a b) (C b a)
Fortunately, only one is correct, 
but you may still want to disambiguate your grammar or input.
There's more of the same for every \<equiv> expression in my axioms.

II tried to write a simple proof following p 40--42 of isar-ref.pdf,
but it didn't work. I get do-not-enter signs on every line of the
proof.  The following commented proof is no better.

----- Tarski2.thy Tarski2

theory Tarski2
imports Complex_Main 
begin
locale tarskifirst7 =
 fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("_ _  \<equiv> _ _" [99,99,99,99] 70)
 fixes B :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
(*
  assumes A1: "\<forall> a b . a b \<equiv> b a"
*)
  assumes A1: "a b \<equiv> b a"
   and A2: "a b \<equiv> p q \<and> a b \<equiv> r s --> p q \<equiv> r s"
   and A3: "a b \<equiv> c c ==> a = b"
   and A4: "\<exists> x. B q a x \<and> a x \<equiv> b c"
   and A5: "a \<noteq> b \<and> B a b x \<and> B a' b' x' \<and> b x \<equiv> b' x' \<and> 
              a b \<equiv> a' b' \<and> a c \<equiv> a' c' \<and> b c \<equiv> b' c' --> c x \<equiv> c' x'"
   and A6: "B a b a ==> a = b"
   and A7: "B a p c \<and> B b q c ==> (\<exists> x. B p x b \<and> B q x a)"


context tarskifirst7
begin


theorem EquivReflexive: "a b \<equiv> a b"

   proof -
     have "b a \<equiv> a b" by (rule A1)
     have "b a \<equiv> a b" by (rule A1)
     thus "a b \<equiv> a b" by (rule A2)
     qed
   end

(*
   proof -
     have "b a \<equiv> a b" by (rule A1 [symmetric])
     have "b a \<equiv> a b" by (rule A1 [symmetric])
     also have "a b \<equiv> a b" by (rule A2 [symmetric])
     finally show "a b \<equiv> a b"
     qed
   end
*)



(* end *)
(*
 lemma A1: "C a b b a"
  by (simp add: A1)
 

lemma A2: "C a b p q \<and> C a b r s ==> C p q r s"
  by (simp add: A2)



lemma A3 : a b \<equiv> c c =\<Rightarrow> a = b
  by (simp add: A3)

theorem th2-1: a b \<equiv> a b
proof −
  from A2 [of b a a b a b] and A1 [of b a] show ?thesis by simp
qed

theorem th2-2: a b \<equiv> c d =\<Rightarrow> c d \<equiv> a b
proof −
  assume a b \<equiv> c d
  with A2 [of a b c d a b] and th2-1 [of a b] show ?thesis by simp
qed

theorem th2-3: [[a b \<equiv> c d; c d \<equiv> e f ]] =\<Rightarrow> a b \<equiv> e f
proof −
  assume a b \<equiv> c d
  with th2-2 [of a b c d] have c d \<equiv> a b by simp
  assume c d \<equiv> e f
  with A2 [of c d a b e f ] and c d \<equiv> a b show ?thesis by simp
qed

theorem th2-4: a b \<equiv> c d =\<Rightarrow> b a \<equiv> c d
proof −
  assume a b \<equiv> c d
  with th2-3 [of b a a b c d] and A1 [of b a] show ?thesis by simp
qed

theorem th2-5: a b \<equiv> c d =\<Rightarrow> a b \<equiv> d c
proof −
  assume a b \<equiv> c d
  with th2-3 [of a b c d d c] and A1 [of c d] show ?thesis by simp
qed

definition is-segment :: 'p set \<Rightarrow> bool where
is-segment X \<exists> x y. X = {x, y}
definition segments :: p set set where
segments = {X. is-segment X}
definition SC :: p set \<Rightarrow> p set \<Rightarrow> bool where
SC X Y \<exists> w x y z. X = {w, x} \<and> Y = {y, z} \<and> w x \<equiv> y z

*)






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.