added more infrastructure for the recursion combinator
authorurbanc
Sun Jul 02 17:27:10 2006 +0200 (2006-07-02)
changeset 1997289c5afe4139a
parent 19971 ddf69abaffa8
child 19973 07cf246f76a3
added more infrastructure for the recursion combinator
src/HOL/Nominal/Examples/Fsub.thy
src/HOL/Nominal/Examples/Iteration.thy
src/HOL/Nominal/Examples/SN.thy
src/HOL/Nominal/Examples/Weakening.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Fri Jun 30 18:26:36 2006 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Sun Jul 02 17:27:10 2006 +0200
     1.3 @@ -178,7 +178,7 @@
     1.4    have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by fact
     1.5    moreover
     1.6    have "X\<sharp>(domain \<Gamma>)" by fact
     1.7 -  hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_eqvt domain_eqvt[symmetric])
     1.8 +  hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_bij domain_eqvt[symmetric])
     1.9    moreover
    1.10    have "T closed_in \<Gamma>" by fact
    1.11    hence "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_eqvt)
    1.12 @@ -341,7 +341,7 @@
    1.13              dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
    1.14              simp add: domain_eqvt)
    1.15  apply(force)
    1.16 -apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt)
    1.17 +apply(force intro!: S_Forall simp add: fresh_prod fresh_bij)
    1.18  done
    1.19  
    1.20  text {* The most painful part of the subtyping definition is the strengthening of the
     2.1 --- a/src/HOL/Nominal/Examples/Iteration.thy	Fri Jun 30 18:26:36 2006 +0200
     2.2 +++ b/src/HOL/Nominal/Examples/Iteration.thy	Sun Jul 02 17:27:10 2006 +0200
     2.3 @@ -104,15 +104,11 @@
     2.4        done
     2.5      have fs1: "a1\<sharp>f3 a1 r1" using b f1
     2.6        apply(auto)
     2.7 -      apply(case_tac "a=a1")
     2.8 -      apply(simp)
     2.9        apply(rule_tac pi="[(a1,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
    2.10        apply(perm_simp add: calc_atm fresh_prod)
    2.11        done      
    2.12      have fs2: "a2\<sharp>f3 a2 r2" using b f2
    2.13        apply(auto)
    2.14 -      apply(case_tac "a=a2")
    2.15 -      apply(simp)
    2.16        apply(rule_tac pi="[(a2,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
    2.17        apply(perm_simp add: calc_atm fresh_prod)
    2.18        done      
    2.19 @@ -155,7 +151,7 @@
    2.20    have fs_pi: "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" 
    2.21    proof -
    2.22      from c obtain a where fs1: "a\<sharp>f3" and fs2: "\<forall>(r::'a::pt_name). a\<sharp>f3 a r" by force
    2.23 -    have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_eqvt)
    2.24 +    have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_bij)
    2.25      moreover
    2.26      have "\<forall>(r::'a::pt_name). (pi\<bullet>a)\<sharp>((pi\<bullet>f3) (pi\<bullet>a) r)" using fs2 by (perm_simp add: fresh_right)
    2.27      ultimately show "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" by blast
     3.1 --- a/src/HOL/Nominal/Examples/SN.thy	Fri Jun 30 18:26:36 2006 +0200
     3.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sun Jul 02 17:27:10 2006 +0200
     3.3 @@ -217,7 +217,7 @@
     3.4    shows   "valid (pi\<bullet>\<Gamma>)"
     3.5  using a
     3.6  apply(induct)
     3.7 -apply(auto simp add: fresh_eqvt)
     3.8 +apply(auto simp add: fresh_bij)
     3.9  done
    3.10  
    3.11  (* typing judgements *)
    3.12 @@ -281,7 +281,7 @@
    3.13      using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
    3.14  next 
    3.15    case (t3 \<Gamma> \<sigma> \<tau> a t)
    3.16 -  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
    3.17 +  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
    3.18    ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
    3.19  qed (auto)
    3.20  
     4.1 --- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Jun 30 18:26:36 2006 +0200
     4.2 +++ b/src/HOL/Nominal/Examples/Weakening.thy	Sun Jul 02 17:27:10 2006 +0200
     4.3 @@ -42,7 +42,7 @@
     4.4    shows   "valid (pi\<bullet>\<Gamma>)"
     4.5  using a
     4.6  apply(induct)
     4.7 -apply(auto simp add: fresh_eqvt)
     4.8 +apply(auto simp add: fresh_bij)
     4.9  done
    4.10  
    4.11  (* typing judgements *)
    4.12 @@ -76,7 +76,7 @@
    4.13      using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
    4.14  next 
    4.15    case (t3 \<Gamma> \<sigma> \<tau> a t)
    4.16 -  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
    4.17 +  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
    4.18    ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
    4.19  qed (auto)
    4.20  
     5.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Jun 30 18:26:36 2006 +0200
     5.2 +++ b/src/HOL/Nominal/Nominal.thy	Sun Jul 02 17:27:10 2006 +0200
     5.3 @@ -87,6 +87,16 @@
     5.4    shows "pi\<bullet>(b::bool) = b"
     5.5    by (cases b) auto
     5.6  
     5.7 +lemma perm_boolI:
     5.8 +  assumes a: "P"
     5.9 +  shows "pi\<bullet>P"
    5.10 +  using a by (simp add: perm_bool)
    5.11 +
    5.12 +lemma perm_boolE:
    5.13 +  assumes a: "pi\<bullet>P"
    5.14 +  shows "P"
    5.15 +  using a by (simp add: perm_bool)
    5.16 +
    5.17  (* permutation on options *)
    5.18  primrec (unchecked perm_option)
    5.19    perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
    5.20 @@ -865,6 +875,13 @@
    5.21  apply(simp add: supp_def dj_perm_forget[OF dj])
    5.22  done
    5.23  
    5.24 +lemma at_fresh_ineq:
    5.25 +  fixes a :: "'x"
    5.26 +  and   b :: "'y"
    5.27 +  assumes dj: "disjoint TYPE('y) TYPE('x)"
    5.28 +  shows "a\<sharp>b" 
    5.29 +  by (simp add: fresh_def dj_supp[OF dj])
    5.30 +
    5.31  section {* permutation type instances *}
    5.32  (* ===================================*)
    5.33  
    5.34 @@ -1406,6 +1423,15 @@
    5.35    shows  "a\<sharp>x"
    5.36  using a by (simp add: pt_fresh_bij[OF pt, OF at])
    5.37  
    5.38 +lemma pt_fresh_eqvt:
    5.39 +  fixes  pi :: "'x prm"
    5.40 +  and     x :: "'a"
    5.41 +  and     a :: "'x"
    5.42 +  assumes pt: "pt TYPE('a) TYPE('x)"
    5.43 +  and     at: "at TYPE('x)"
    5.44 +  shows "pi\<bullet>(a\<sharp>x) = (pi\<bullet>a)\<sharp>(pi\<bullet>x)"
    5.45 +  by (simp add: perm_bool pt_fresh_bij[OF pt, OF at])
    5.46 +
    5.47  lemma pt_perm_fresh1:
    5.48    fixes a :: "'x"
    5.49    and   b :: "'x"
    5.50 @@ -1556,6 +1582,29 @@
    5.51    thus ?thesis by (simp add: pt2[OF pt])
    5.52  qed
    5.53  
    5.54 +section {* equivaraince for some connectives *}
    5.55 +
    5.56 +lemma pt_all_eqvt:
    5.57 +  fixes  pi :: "'x prm"
    5.58 +  and     x :: "'a"
    5.59 +  assumes pt: "pt TYPE('a) TYPE('x)"
    5.60 +  and     at: "at TYPE('x)"
    5.61 +  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). (pi\<bullet>P) x)"
    5.62 +apply(auto simp add: perm_bool perm_fun_def)
    5.63 +apply(drule_tac x="pi\<bullet>x" in spec)
    5.64 +apply(simp add: pt_rev_pi[OF pt, OF at])
    5.65 +done
    5.66 +
    5.67 +lemma imp_eqvt:
    5.68 +  fixes pi::"'x prm"
    5.69 +  shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
    5.70 +  by (simp add: perm_bool)
    5.71 +
    5.72 +lemma conj_eqvt:
    5.73 +  fixes pi::"'x prm"
    5.74 +  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
    5.75 +  by (simp add: perm_bool)
    5.76 +
    5.77  section {* facts about supports *}
    5.78  (*==============================*)
    5.79  
     6.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Jun 30 18:26:36 2006 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Jul 02 17:27:10 2006 +0200
     6.3 @@ -668,6 +668,7 @@
     6.4         val pt_perm_compose'    = thm "Nominal.pt_perm_compose'";
     6.5         val perm_app            = thm "Nominal.pt_fun_app_eq";
     6.6         val at_fresh            = thm "Nominal.at_fresh";
     6.7 +       val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
     6.8         val at_calc             = thms "Nominal.at_calc";
     6.9         val at_supp             = thm "Nominal.at_supp";
    6.10         val dj_supp             = thm "Nominal.dj_supp";
    6.11 @@ -679,8 +680,11 @@
    6.12         val fresh_bij           = thm "Nominal.pt_fresh_bij";
    6.13         val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
    6.14         val fresh_aux           = thm "Nominal.pt_fresh_aux";
    6.15 +       val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
    6.16 +       val all_eqvt            = thm "Nominal.pt_all_eqvt";
    6.17         val pt_pi_rev           = thm "Nominal.pt_pi_rev";
    6.18         val pt_rev_pi           = thm "Nominal.pt_rev_pi";
    6.19 +       val at_exists_fresh     = thm "Nominal.at_exists_fresh";
    6.20    
    6.21  
    6.22         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    6.23 @@ -761,7 +765,12 @@
    6.24              ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
    6.25              ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
    6.26              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    6.27 -            ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
    6.28 +            ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
    6.29 +            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])]
    6.30 +            ||>> PureThy.add_thmss 
    6.31 +	      let val thms1 = inst_at [at_fresh]
    6.32 +		  val thms2 = inst_dj [at_fresh_ineq]
    6.33 +	      in [(("fresh_atm", thms1 @ thms2),[])] end
    6.34              ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
    6.35              ||>> PureThy.add_thmss
    6.36  	      let val thms1 = inst_pt_at [abs_fun_pi]
    6.37 @@ -792,7 +801,10 @@
    6.38              ||>> PureThy.add_thmss
    6.39  	      let val thms1 = inst_pt_at [fresh_bij]
    6.40  		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
    6.41 -	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
    6.42 +	      in [(("fresh_bij", thms1 @ thms2),[])] end
    6.43 +            ||>> PureThy.add_thmss
    6.44 +	      let val thms1 = inst_pt_at [fresh_eqvt]
    6.45 +	      in [(("fresh_eqvt", thms1),[])] end
    6.46              ||>> PureThy.add_thmss
    6.47  	      let val thms1 = inst_pt_at [fresh_aux]
    6.48  		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]