inductive2: canonical specification syntax;
authorwenzelm
Tue Nov 14 22:16:54 2006 +0100 (2006-11-14)
changeset 213643baf57a27269
parent 21363 a12c0bcd9b2a
child 21365 4ee8e2702241
inductive2: canonical specification syntax;
src/HOL/FunDef.thy
src/HOL/Nominal/Examples/Weakening.thy
     1.1 --- a/src/HOL/FunDef.thy	Tue Nov 14 17:55:30 2006 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Tue Nov 14 22:16:54 2006 +0100
     1.3 @@ -48,8 +48,8 @@
     1.4  
     1.5  inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
     1.6    for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.7 -intros
     1.8 -    accPI: "(!!y. r y x ==> accP r y) ==> accP r x"
     1.9 +where
    1.10 +  accPI: "(!!y. r y x ==> accP r y) ==> accP r x"
    1.11  
    1.12  
    1.13  theorem accP_induct:
     2.1 --- a/src/HOL/Nominal/Examples/Weakening.thy	Tue Nov 14 17:55:30 2006 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/Weakening.thy	Tue Nov 14 22:16:54 2006 +0100
     2.3 @@ -28,9 +28,9 @@
     2.4  text {* valid contexts *}
     2.5  inductive2
     2.6    valid :: "(name\<times>ty) list \<Rightarrow> bool"
     2.7 -intros
     2.8 -v1[intro]: "valid []"
     2.9 -v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
    2.10 +where
    2.11 +    v1[intro]: "valid []"
    2.12 +  | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
    2.13  
    2.14  lemma eqvt_valid:
    2.15    fixes   pi:: "name prm"
    2.16 @@ -43,10 +43,10 @@
    2.17  text{* typing judgements *}
    2.18  inductive2
    2.19    typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
    2.20 -intros
    2.21 -t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
    2.22 -t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
    2.23 -t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
    2.24 +where
    2.25 +    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
    2.26 +  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
    2.27 +  | t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
    2.28  
    2.29  lemma eqvt_typing: 
    2.30    fixes pi:: "name prm"