Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/Terms2.thy
changeset 1183 cb3da5b540f2
parent 1182 3c32f91fa771
equal deleted inserted replaced
1182:3c32f91fa771 1183:cb3da5b540f2 
    23 primrec 
    23 primrec 
    24   bv1
 
    24   bv1
 
    25 where
 
    25 where
 
    26   "bv1 (BUnit) = {}"
 
    26   "bv1 (BUnit) = {}"
 
    27 | "bv1 (BVr x) = {atom x}"
 
    27 | "bv1 (BVr x) = {atom x}"
 
    28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
 
    28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
    29 
    29 
    30 local_setup {* define_raw_fv "Terms.rtrm1"
 
    30 local_setup {* define_raw_fv "Terms.rtrm1"
 
    31   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
 
    31   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
 
    32    [[], [[]], [[], []]]] *}
 
    32    [[], [[]], [[], []]]] *}
 
    33 print_theorems
 
    33 print_theorems
 
    56 
    56 
    57 (* Shouyld we derive it? But bv is given by the user? *)
 
    57 (* Shouyld we derive it? But bv is given by the user? *)
 
    58 lemma bv1_eqvt[eqvt]:
 
    58 lemma bv1_eqvt[eqvt]:
 
    59   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
 
    59   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
 
    60   apply (induct x)
 
    60   apply (induct x)
 
    61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
 
    61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts)
 
    62 done
 
    62 done
 
    63 
    63 
    64 lemma fv_rtrm1_eqvt[eqvt]:
 
    64 lemma fv_rtrm1_eqvt[eqvt]:
 
    65     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
 
    65     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
 
    66     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
 
    66     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
 
   223 apply(rule supports_finite)
 
   223 apply(rule supports_finite)
 
   224 apply(rule lt1_supp_pre)
 
   224 apply(rule lt1_supp_pre)
 
   225 apply(simp add: supp_Pair supp_atom bp_supp)
 
   225 apply(simp add: supp_Pair supp_atom bp_supp)
 
   226 done
 
   226 done
 
   227 
   227 
       
   228 lemma fv_eq_bv: "fv_bp bp = bv1 bp"
 
       
   229 apply(induct bp rule: trm1_bp_inducts(2))
 
       
   230 apply(simp_all)
 
       
   231 done
 
       
   232 
   228 lemma supp_fv:
 
   233 lemma supp_fv:
 
   229   shows "supp t = fv_trm1 t"
 
   234   shows "supp t = fv_trm1 t"
 
   230 apply(induct t rule: trm1_bp_inducts(1))
 
   235 apply(induct t rule: trm1_bp_inducts(1))
 
   231 apply(simp_all)
 
   236 apply(simp_all)
 
   232 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   237 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   238 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 
   243 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 
   239 apply(simp add: alpha1_INJ)
 
   244 apply(simp add: alpha1_INJ)
 
   240 apply(simp add: Abs_eq_iff)
 
   245 apply(simp add: Abs_eq_iff)
 
   241 apply(simp add: alpha_gen.simps)
 
   246 apply(simp add: alpha_gen.simps)
 
   242 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 
   247 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 
   243 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
 
   248 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
 
   244 apply(simp add: supp_Abs fv_trm1)
 
   249 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
 
   245 apply(simp (no_asm) add: supp_def)
 
   250 apply(simp (no_asm) add: supp_def)
 
   246 apply(simp add: alpha1_INJ)
 
   251 apply(simp add: alpha1_INJ)
 
   247 apply(simp add: Abs_eq_iff)
 
   252 apply(simp add: Abs_eq_iff)
 
   248 apply(simp add: alpha_gen)
 
   253 apply(simp add: alpha_gen)
 
   249 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
 
   254 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
 
   250 apply(simp add: Collect_imp_eq Collect_neg_eq)
 
   255 apply(simp add: Collect_imp_eq Collect_neg_eq)
 
   251 done*)
 
   256 done
 
   252 sorry
 
       
   253 
   257 
   254 lemma trm1_supp:
 
   258 lemma trm1_supp:
 
   255   "supp (Vr1 x) = {atom x}"
 
   259   "supp (Vr1 x) = {atom x}"
 
   256   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
 
   260   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
 
   257   "supp (Lm1 x t) = (supp t) - {atom x}"
 
   261   "supp (Lm1 x t) = (supp t) - {atom x}"
 
   258   "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
 
   262   "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
 
   259 sorry (*  by (simp_all only: supp_fv fv_trm1)
 
   263 by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
 
   260 
   264 
   261 lemma trm1_induct_strong:
 
   265 lemma trm1_induct_strong:
 
   262   assumes "\<And>name b. P b (Vr1 name)"
 
   266   assumes "\<And>name b. P b (Vr1 name)"
 
   263   and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
 
   267   and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
 
   264   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
 
   268   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
 
   265   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
 
   269   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
 
   266   shows   "P a rtrma"
 
   270   shows   "P a rtrma"
 
   267 sorry *)
 
   271 sorry
 
   268 
   272 
   269 section {*** lets with single assignments ***}
 
   273 section {*** lets with single assignments ***}
 
   270 
   274 
   271 datatype rtrm2 =
 
   275 datatype rtrm2 =
 
   272   rVr2 "name"
 
   276   rVr2 "name"
 
   889 where
 
   893 where
 
   890   a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
 
   894   a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
 
   891 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
 
   895 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
 
   892 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
 
   896 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
 
   893 
   897 
   894 lemma bvfv7: "rbv7 x = fv_rtrm7 x"
 
       
   895   apply induct
 
       
   896   apply simp_all
 
       
   897 sorry (*done*)
 
       
   898 
       
   899 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
 
   898 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
 
   900   apply simp
 
   899   apply simp
 
   901   apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
 
   900   apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
 
   902   apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
 
   901   apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
 
   903   apply simp
 
   902   apply simp
 
   958 
   957 
   959 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
 
   958 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
 
   960   apply simp apply clarify
 
   959   apply simp apply clarify
 
   961   apply (erule alpha8f_alpha8b.inducts(1))
 
   960   apply (erule alpha8f_alpha8b.inducts(1))
 
   962   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
 
   961   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
 
   963 sorry (*done*)
 
   962   apply clarify
 
       
   963   apply (erule alpha8f_alpha8b.inducts(2))
 
       
   964   apply (simp_all)
 
       
   965 done
 
   964 
   966 
   965 
   967 
   966 
   968 
   967 
   969 
   968 
   970
nominal2