*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] A constant become a free variable*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Wed, 04 Dec 2013 10:09:45 +0100*Organization*: Ada @ Home*User-agent*: Opera Mail/12.16 (Linux)

-----%<---------->%----- theory Sample imports Main begin typedecl atom; typedecl variable; datatype "term" = Any ("ε") | Atom atom ("α") | Variable variable ("υ") | Compound "term list" ("ω") ; locale unification = fixes unifies :: "[term, term] ⇒ bool" (infix "≅" 500) and "interpretation" :: "variable ⇒ term" ("⊢") assumes self: "t ≅ t" and comm: "t1 ≅ t2 ⟷ t2 ≅ t1" and inter: "(υ v) ≅ t ⟷ (⊢ v) ≅ t" and rec: "(ω (t1 # r1)) ≅ (ω (t2 # r2)) ⟷ t1 ≅ t2 ∧ (ω r1) ≅ (ω r2)" ; lemma (in unification) l1: "t1 = t2 ⟹ t1 ≅ t2" proof - assume 1: "t1 = t2" have 2: "t1 = t2 ⟹ t1 ≡ t2" by (fact HOL.eq_reflection[of t1 t2]) have 3: "t1 ≡ t2" by (fact 2[OF 1]) have 4: "t1 ≅ t1" by (fact self[of t1]) from 4 show "t1 ≅ t2" by (simp add: 3) qed ; end -----%<---------->%----- -- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Attachment:
Sample.thy**

**Follow-Ups**:**Re: [isabelle] A constant become a free variable***From:*Makarius

- Previous by Date: [isabelle] F-IDE 2014: Call for Papers
- Next by Date: Re: [isabelle] Isabelle2013-2-RC3 available for testing
- Previous by Thread: [isabelle] F-IDE 2014: Call for Papers
- Next by Thread: Re: [isabelle] A constant become a free variable
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list