Nominal/Ex/Lambda_F_T.thy
changeset 2817 2f5ce0ecbf31
parent 2815 812cfadeb8b7
child 2823 e92ce4d110f4
equal deleted inserted replaced
2816:84c3929d2684 2817:2f5ce0ecbf31
    42   and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
    42   and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
    43   shows "a \<sharp> f x y z w"
    43   shows "a \<sharp> f x y z w"
    44   using fresh_fun_eqvt_app[OF a b(1)] a b
    44   using fresh_fun_eqvt_app[OF a b(1)] a b
    45   by (metis fresh_fun_app)
    45   by (metis fresh_fun_app)
    46 
    46 
       
    47 lemma the_default_pty:
       
    48   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
       
    49   and unique: "\<exists>!y. G x y"
       
    50   and pty: "\<And>x y. G x y \<Longrightarrow> P x y"
       
    51   shows "P x (f x)"
       
    52   apply(subst f_def)
       
    53   apply (rule ex1E[OF unique])
       
    54   apply (subst THE_default1_equality[OF unique])
       
    55   apply assumption
       
    56   apply (rule pty)
       
    57   apply assumption
       
    58   done
       
    59 
       
    60 locale test =
       
    61   fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)"
       
    62     and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
       
    63     and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
       
    64   assumes fs: "finite (supp (f1, f2, f3))"
       
    65     and eq: "eqvt f1" "eqvt f2" "eqvt f3"
       
    66     and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l"
       
    67     and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l"
       
    68     and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
       
    69 begin
       
    70 
    47 nominal_primrec
    71 nominal_primrec
    48   f
    72   f
    49 where
    73 where
    50   "f f1 f2 f3 (Var x) l = f1 x l"
    74   "f (Var x) l = f1 x l"
    51 | "f f1 f2 f3 (App t1 t2) l = f2 t1 t2 (f f1 f2 f3 t1 l) (f f1 f2 f3 t2 l) l"
    75 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l"
    52 | "(\<And>t l r. atom x \<sharp> r \<Longrightarrow> atom x \<sharp> f3 x t r l) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3,l) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t) l) = f3 x t (f f1 f2 f3 t (x # l)) l"
    76 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l"
    53   apply (simp add: eqvt_def f_graph_def)
    77   apply (simp add: eqvt_def f_graph_def)
    54   apply (rule, perm_simp, rule)
    78   apply (rule, perm_simp)
       
    79   apply (simp only: eq[unfolded eqvt_def])
    55   apply(case_tac x)
    80   apply(case_tac x)
    56   apply(rule_tac y="d" and c="z" in lam.strong_exhaust)
    81   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
    57   apply(auto simp add: fresh_star_def)
    82   apply(auto simp add: fresh_star_def)
    58   apply(blast)
       
    59   apply blast
       
    60   defer
       
    61   apply(simp add: fresh_Pair_elim)
       
    62   apply(erule Abs1_eq_fdest)
    83   apply(erule Abs1_eq_fdest)
    63   defer
    84   defer
    64   apply simp_all
    85   apply simp_all
    65   apply (rule_tac f="f3a" in fresh_fun_eqvt_app4)
    86   apply (rule fresh_fun_eqvt_app4[OF eq(3)])
    66   apply assumption
       
    67   apply (simp add: fresh_at_base)
    87   apply (simp add: fresh_at_base)
    68   apply assumption
    88   apply assumption
    69   apply (erule fresh_eqvt_at)
    89   apply (erule fresh_eqvt_at)
    70   apply (simp add: supp_Pair supp_fun_eqvt finite_supp)
    90   apply (simp add: finite_supp)
    71   apply (simp add: fresh_Pair)
    91   apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
    72   apply (simp add: fresh_Cons)
    92   apply assumption
    73   apply (simp add: fresh_Cons fresh_at_base)
    93   apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
    74   apply (assumption)
       
    75   apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3a x y r l) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
       
    76   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
    94   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
    77   apply (simp add: eqvt_at_def eqvt_def)
    95   apply (simp add: eqvt_at_def)
    78   apply (simp add: swap_fresh_fresh)
    96   apply (simp add: swap_fresh_fresh)
    79   apply (simp add: permute_fun_app_eq)
    97   apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
    80   apply (simp add: eqvt_def)
    98   apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
    81   prefer 2
    99   apply (simp add: fresh_star_def)
    82   apply (subgoal_tac "atom x \<sharp> f_sumC (f1a, f2a, f3a, t, x # la)")
   100   apply (rule fcb3)
    83   apply simp
   101   apply (rule_tac x="x # la" in meta_spec)
    84 --"I believe this holds by induction on the graph..."
   102   apply (thin_tac "eqvt_at f_sumC (t, x # la)")
    85   unfolding f_sumC_def
   103   apply (thin_tac "atom x \<sharp> la")
    86   apply (rule_tac y="t" in lam.exhaust)
   104   apply (thin_tac "atom xa \<sharp> la")
    87   apply (subgoal_tac "THE_default undefined (f_graph (f1a, f2a, f3a, t, x # la)) = f1a name (x # la)")
   105   apply (thin_tac "x \<noteq> xa")
    88   apply simp
   106   apply (thin_tac "atom xa \<sharp> t")
    89   defer
   107   apply (subgoal_tac "atom ` set (snd (t, xb)) \<sharp>* f_sumC (t, xb)")
    90   apply (rule THE_default1_equality)
   108   apply simp
    91   apply simp
   109   apply (rule_tac x="(t, xb)" in meta_spec)
    92   defer
   110   apply (simp only: triv_forall_equality)
    93   apply simp
   111 --"We start induction on the graph. We need the 2nd subgoal in the first one"
    94   apply (rule_tac ?f1.0="f1a" in f_graph.intros(1))
   112   apply (subgoal_tac "\<And>x y. f_graph x y \<Longrightarrow> atom ` set (snd x) \<sharp>* y")
    95   sorry (*this could be defined? *)
   113   apply (rule the_default_pty[OF f_sumC_def])
       
   114   prefer 2
       
   115   apply blast
       
   116   prefer 2
       
   117   apply (erule f_graph.induct)
       
   118   apply (simp add: fcb1)
       
   119   apply (simp add: fcb2 fresh_star_Pair)
       
   120   apply (simp only: snd_conv)
       
   121   apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
       
   122   apply (simp add: fresh_star_def)
       
   123   apply (rule fcb3)
       
   124   apply assumption
       
   125 --"We'd like to do the proof with this property"
       
   126   apply (case_tac xc)
       
   127   apply simp
       
   128   apply (rule_tac lam="a" and c="b" in lam.strong_induct)
       
   129   apply (rule_tac a="f1 name c" in ex1I)
       
   130   apply (rule f_graph.intros)
       
   131   apply (erule f_graph.cases)
       
   132   apply simp_all[3]
       
   133   apply (drule_tac x="c" in meta_spec)+
       
   134   apply (erule ex1E)+
       
   135   apply (subgoal_tac "f_graph (lam1, c) (f_sumC (lam1, c))")
       
   136   apply (subgoal_tac "f_graph (lam2, c) (f_sumC (lam2, c))")
       
   137   apply (rule_tac a="f2 lam1 lam2 (f_sumC (lam1, c)) (f_sumC (lam2, c)) c" in ex1I)
       
   138   apply (rule_tac f_graph.intros(2))
       
   139   apply assumption+
       
   140   apply (rotate_tac 8)
       
   141   apply (erule f_graph.cases)
       
   142   apply simp
       
   143   apply auto[1]
       
   144   apply metis
       
   145   apply simp
       
   146   apply (simp add: f_sumC_def)
       
   147   apply (rule THE_defaultI')
       
   148   apply metis
       
   149   apply (simp add: f_sumC_def)
       
   150   apply (rule THE_defaultI')
       
   151   apply metis
       
   152 --"Only the Lambda case left"
       
   153   apply (subgoal_tac "f_graph (lam, (name # c)) (f_sumC (lam, (name # c)))")
       
   154   prefer 2
       
   155   apply (simp add: f_sumC_def)
       
   156   apply (rule THE_defaultI')
       
   157   apply assumption
       
   158   apply (rule_tac a="f3 name lam (f_sumC (lam, name # c)) c" in ex1I)
       
   159   apply (rule f_graph.intros(3))
       
   160   apply (simp add: fresh_star_def)
       
   161   apply assumption
       
   162   apply (rotate_tac -1)
       
   163   apply (erule f_graph.cases)
       
   164   apply simp_all[2]
       
   165   apply simp
       
   166   apply auto[1]
       
   167   apply (subgoal_tac "f_sumC (lam, name # l) = f_sum (lam, name # l)")
       
   168   apply simp
       
   169   apply (rule sym)
       
   170   apply (erule Abs1_eq_fdest)
       
   171   apply (subgoal_tac "atom ` set (name # l) \<sharp>* f3 name lam (f_sum (lam, name # l)) l")
       
   172   apply (simp add: fresh_star_def)
       
   173   apply (rule fcb3)
       
   174   apply metis
       
   175   apply (rule fresh_fun_eqvt_app4[OF eq(3)])
       
   176   apply (simp add: fresh_at_base)
       
   177   apply assumption
       
   178 defer --"eqvt_at f_sumC"
       
   179   apply assumption
       
   180   apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 name y r l) = f3 (p \<bullet> name) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
       
   181   apply (subgoal_tac "(atom name \<rightleftharpoons> atom xa) \<bullet> l = l")
       
   182   apply (simp add: eq[unfolded eqvt_def])
       
   183 defer --"eqvt_at f_sumC"
       
   184   apply (metis fresh_star_insert swap_fresh_fresh)
       
   185   apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
       
   186   apply simp
       
   187   sorry
    96 
   188 
    97 termination
   189 termination
    98   by (relation "measure (\<lambda>(_,_,_,x,_). size x)") (auto simp add: lam.size)
   190   by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)
       
   191 
       
   192 end
    99 
   193 
   100 section {* Locally Nameless Terms *}
   194 section {* Locally Nameless Terms *}
   101 
   195 
   102 nominal_datatype ln = 
   196 nominal_datatype ln = 
   103   LNBnd nat
   197   LNBnd nat
   109   lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" 
   203   lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" 
   110 where
   204 where
   111   "lookup [] n x = LNVar x"
   205   "lookup [] n x = LNVar x"
   112 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
   206 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
   113 
   207 
   114 lemma [eqvt]:
   208 lemma lookup_eqvt[eqvt]:
   115   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   209   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   116   by (induct xs arbitrary: n) (simp_all add: permute_pure)
   210   by (induct xs arbitrary: n) (simp_all add: permute_pure)
   117 
   211 
   118 definition
   212 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
   119   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
   213   unfolding fresh_def supp_set[symmetric]
   120 where
   214   apply (induct xs)
   121   "trans t l = f (%x l. lookup l 0 x) (%t1 t2 r1 r2 l. LNApp r1 r2) (%n t r l. LNLam r) t l"
   215   apply (simp add: supp_set_empty)
   122 
   216   apply simp
   123 lemma
   217   apply auto
   124  "trans (Var x) xs = lookup xs 0 x"
   218   apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
   125   "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
   219   done
   126   "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
   220 
   127 apply (simp_all add: trans_def)
   221 interpretation trans: test
   128 apply (subst f.simps)
   222   "%x l. lookup l 0 x"
   129 apply (simp add: ln.fresh)
   223   "%t1 t2 r1 r2 l. LNApp r1 r2"
   130 apply (simp add: eqvt_def)
   224   "%n t r l. LNLam r"
   131 apply auto
   225   apply default
   132 apply (perm_simp, rule)
   226   apply (auto simp add: pure_fresh supp_Pair)
   133 apply (perm_simp, rule)
   227   apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3]
   134 apply (perm_simp, rule)
   228   apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt)
   135 apply (auto simp add: fresh_Pair)[1]
   229   apply (simp add: fresh_star_def)
   136 apply (simp_all add: fresh_def supp_def permute_fun_def)[3]
   230   apply (rule_tac x="0 :: nat" in spec)
   137 apply (simp add: eqvts permute_pure)
   231   apply (induct_tac l)
   138 done
   232   apply (simp add: ln.fresh pure_fresh)
       
   233   apply (auto simp add: ln.fresh pure_fresh)[1]
       
   234   apply (case_tac "a \<in> set list")
       
   235   apply simp
       
   236   apply (rule_tac f="lookup" in fresh_fun_eqvt_app3)
       
   237   unfolding eqvt_def
       
   238   apply rule
       
   239   using eqvts_raw(35)
       
   240   apply auto[1]
       
   241   apply (simp add: fresh_at_list)
       
   242   apply (simp add: pure_fresh)
       
   243   apply (simp add: fresh_at_base)
       
   244   apply (simp add: fresh_star_Pair fresh_star_def ln.fresh)
       
   245   apply (simp add: fresh_star_def ln.fresh)
       
   246   done
       
   247 
       
   248 thm trans.f.simps
   139 
   249 
   140 lemma lam_strong_exhaust2:
   250 lemma lam_strong_exhaust2:
   141   "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
   251   "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
   142     \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
   252     \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
   143     \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
   253     \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
   152 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"
   262 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"
   153 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"
   263 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"
   154 | "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
   264 | "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
   155   apply (simp add: eqvt_def g_graph_def)
   265   apply (simp add: eqvt_def g_graph_def)
   156   apply (rule, perm_simp, rule)
   266   apply (rule, perm_simp, rule)
       
   267   apply simp_all
   157   apply (case_tac x)
   268   apply (case_tac x)
   158   apply (case_tac "finite (supp (a, b, c))")
   269   apply (case_tac "finite (supp (a, b, c))")
   159   prefer 2
   270   prefer 2
   160   apply simp
   271   apply simp
   161   apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
   272   apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
   162   apply simp_all
   273   apply auto
       
   274   apply blast
       
   275   apply (simp add: Abs1_eq_iff fresh_star_def)
       
   276   sorry
       
   277 
       
   278 termination
       
   279   by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size)
       
   280 
       
   281 end