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.
QuotMain.thy
changeset 87 9220c51e5155
parent 86 133af7260a12
child 88 19d3856abb81
child 89 072f2f8dc694
equal deleted inserted replaced
86:133af7260a12 87:9220c51e5155 
   325 *}
 
   325 *}
 
   326 
   326 
   327 definition
 
   327 definition
 
   328   "(x : p) \<Longrightarrow> (Babs p m x = m x)"
 
   328   "(x : p) \<Longrightarrow> (Babs p m x = m x)"
 
   329 
   329 
   330 print_theorems
 
   330 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where
 
   331 
   331   "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*)
 
   332 thm Ball_def
 
   332 
   333 
       
   334 definition
 
       
   335   "BAll A P \<equiv> (\<And>x. x \<in> A \<Longrightarrow> P x)"
 
       
   336 thm BAll_def
 
       
   337 
   333 
   338 ML {*
 
   334 ML {*
 
   339 (* trm \<Rightarrow> new_trm *)
 
   335 (* trm \<Rightarrow> new_trm *)
 
   340 fun regularise trm rty rel lthy =
 
   336 fun regularise trm rty rel lthy =
 
   341   case trm of
 
   337   case trm of
 
   383         val t' = subst_bound (v, t);
 
   379         val t' = subst_bound (v, t);
 
   384         val rec_term = regularise t' rty rel lthy2;
 
   380         val rec_term = regularise t' rty rel lthy2;
 
   385       in
 
   381       in
 
   386         Term.lambda_name (x, v) rec_term
 
   382         Term.lambda_name (x, v) rec_term
 
   387       end
 
   383       end
 
       
   384   | ((Const (@{const_name "Ex"}, _)) $ (Abs (x, T, t))) =>
 
       
   385       if T = rty then let
 
       
   386         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
 
       
   387         val v = Free (x', rty);
 
       
   388         val t' = subst_bound (v, t);
 
       
   389         val rec_term = regularise t' rty rel lthy2;
 
       
   390         val lam_term = Term.lambda_name (x, v) rec_term;
 
       
   391         val sub_res_term = tyRel T rty rel lthy;
 
       
   392         val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
 
       
   393         val res_term = respects $ sub_res_term;
 
       
   394         val ty = fastype_of lam_term;
 
       
   395         val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
 
       
   396         val rall_term = (rall $ res_term) $ lam_term;
 
       
   397       in
 
       
   398         rall_term
 
       
   399       end else let
 
       
   400         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
 
       
   401         val v = Free (x', rty);
 
       
   402         val t' = subst_bound (v, t);
 
       
   403         val rec_term = regularise t' rty rel lthy2;
 
       
   404       in
 
       
   405         Term.lambda_name (x, v) rec_term
 
       
   406       end
 
   388   | _ => trm
 
   407   | _ => trm
 
   389 
   408 
   390 *}
 
   409 *}
 
   391 term "Ball"
 
       
   392 term "Ball (Respects (RR)) (\<lambda>x :: trm. true)"
 
       
   393 
   410 
   394 ML {*
 
   411 ML {*
 
   395   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
 
   412   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
 
   396   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. true"} @{typ "trm"} @{term "RR"} @{context})
 
   413   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   397 *}
 
   414   cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context})
 
       
   415 *}
 
       
   416 
       
   417 
       
   418 term Respects
 
       
   419 
       
   420 ML {*
 
       
   421 fun atomize_thm t =
 
       
   422   MetaSimplifier.rewrite_rule [ObjectLogic.atomize (cterm_of @{theory} (prop_of t))] t
 
       
   423 *}
 
       
   424 
       
   425 ML {*
 
       
   426 fun meta_quantify t =
 
       
   427   let
 
       
   428     val vars = Term.add_vars (prop_of t) [];
 
       
   429     val cvars = map (fn x => cterm_of @{theory} (Var x)) vars
 
       
   430   in
 
       
   431     fold forall_intr cvars t
 
       
   432   end
 
       
   433 *}
 
       
   434 
       
   435 ML {* atomize_thm (meta_quantify @{thm list.induct}) *}
 
   398 
   436 
   399 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
 
   437 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
 
   400   trm == new_trm
 
   438   trm == new_trm
 
   401 *)
 
   439 *)
 
   402 
   440 
   403 thm list.induct
 
       
   404 
   441 
   405 text {* produces the definition for a lifted constant *}
 
   442 text {* produces the definition for a lifted constant *}
 
   406 
   443 
   407 ML {*
 
   444 ML {*
 
   408 fun get_const_def nconst oconst rty qty lthy =
 
   445 fun get_const_def nconst oconst rty qty lthy =
 
  1077   apply (tactic {* foo_tac' @{context} 1 *})
 
  1114   apply (tactic {* foo_tac' @{context} 1 *})
 
  1078   done
 
  1115   done
 
  1079 
  1116 
  1080 thm list.induct
 
  1117 thm list.induct
 
  1081 
  1118 
       
  1119 ML {* val li = atomize_thm (meta_quantify @{thm list.induct}) *}
 
       
  1120 
       
  1121 ML {* (* Doesn't recognize that 'a list = '?a list *)
 
       
  1122   cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
 
       
  1123 *}
 
       
  1124 
       
  1125 
       
  1126 
  1082 ML {*
 
  1127 ML {*
 
  1083   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 
  1128   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 
  1084 *}
 
  1129 *}
 
  1085 
  1130 
  1086 ML {*
 
  1131 ML {*
nominal2